A new "wf_recp" theory is created as a child of "wf_relp".

The main part of this is the proof that functionals which are well-founded with respect to some well-founded relation have fixed points. This done, the operator "fix" is defined, which yields such a fixed point.

In this section I will create a decent proof context for recursive definitions, eventually.

I have already proved a recursion theorem fairly closely following the formulation and proof devised by Tobias Nipkow for Isabelle-HOL. There are two reasons for my wanting a different version of this result. The Nipkow derived version works with relations rather than functions, and in my version the relations are ProofPower sets of pairs (I think in the original they were probably properties of pairs). This is probably all easily modded into one which works directly with functions but I though it should be possible also to do a neater proof (the "proof" of the recursion theorem in Kunen is just a couple of lines).

The end result certainly looks nicer, we'll have to see whether it works out well in practice. In particular the fixpoint operator simply takes a functional as an argument and delivers the fixed point as a result. The functional which you give it as an argument, in the simple cases, is just what you get by abstracting the right hand side of a recursive definition on the name of the function (more complicated of course if a pattern matching definition is used). The relation with respect to which the recursion is well-founded need only be mentioned when attempting to prove that this does yield a fixed point.

Another minor improvement is that I do not require the relation to be transitive.

The proof is shorter than (my version of) the original, but by less than 20 percent. I'm sure there's lots of scope for improvement. (The isabelle version is much shorter than either.)

The new theory is first created, together with a proof context which we will build up as we develop the theory.

xl-sml open_theory "wf_relp"; force_new_theory "wf_recp"; force_new_pc "wf_recp"; merge_pcs ["xl_cs_∃_conv"] "wf_recp"; set_merge_pcs ["hol", "wf_relp", "wf_recp"];

xl-sml declare_infix (240, "respects");

xl-holconst $respects: (('a → 'b) → ('a → 'b)) → ('a → 'a → BOOL) → BOOL

∀ f r • f respects r ⇔ ∀g h x• (∀y• (tc r) y x ⇒ g y = h y) ⇒ f g x = f h x

xl-holconst fixed_below: (('a → 'b) → ('a → 'b)) → ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL

∀f r g x• fixed_below f r g x ⇔ ∀y• tc r y x ⇒ f g y = g y

xl-holconst fixed_at: (('a → 'b) → ('a → 'b)) → ('a → 'a → BOOL) → ('a → 'b) → 'a → BOOL

∀f r g x• fixed_at f r g x ⇔ fixed_below f r g x ∧ f g x = g x

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x g y• fixed_below f r g x ∧ tc r y x ⇒ fixed_below f r g y⌝); a (rewrite_tac [get_spec ⌜fixed_below⌝, get_spec ⌜$respects⌝]); a (REPEAT strip_tac); a (all_asm_fc_tac [tran_tc_thm2]); a (all_asm_fc_tac []); val fixed_below_lemma1 = save_pop_thm "fixed_below_lemma1";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x g• fixed_below f r g x ⇒ fixed_at f r (f g) x⌝); a (rewrite_tac [get_spec ⌜fixed_below⌝, get_spec ⌜fixed_at⌝, get_spec ⌜$respects⌝]); a (REPEAT strip_tac); (* *** Goal "1" *** *) a (list_spec_nth_asm_tac 3 [⌜f g⌝, ⌜g⌝]); a (spec_nth_asm_tac 1 ⌜y⌝); a (all_asm_fc_tac [tran_tc_thm2]); a (all_asm_fc_tac []); (* *** Goal "2" *** *) a (list_spec_nth_asm_tac 2 [⌜f g⌝, ⌜g⌝]); a (all_asm_fc_tac []); val fixed_at_lemma1 = save_pop_thm "fixed_at_lemma1";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x g• fixed_below f r g x ⇒ ∀y• tc r y x ⇒ fixed_at f r g y⌝); a (rewrite_tac [get_spec ⌜fixed_below⌝, get_spec ⌜fixed_at⌝, get_spec ⌜$respects⌝]); a (REPEAT strip_tac); (* *** Goal "1" *** *) a (all_asm_fc_tac [tran_tc_thm2]); a (all_asm_fc_tac []); (* *** Goal "2" *** *) a (all_asm_fc_tac []); val fixed_at_lemma2 = save_pop_thm "fixed_at_lemma2";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x g• (∀y• tc r y x ⇒ fixed_at f r g y) ⇒ fixed_below f r g x⌝); a (REPEAT_N 4 strip_tac); a (rewrite_tac [get_spec ⌜fixed_at⌝, get_spec ⌜fixed_below⌝]); a (REPEAT strip_tac); a (all_asm_fc_tac []); val fixed_at_lemma3 = save_pop_thm "fixed_at_lemma3";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x g h• fixed_below f r g x ∧ fixed_below f r h x ⇒ ∀z• tc r z x ⇒ h z = g z⌝); a (REPEAT_N 4 strip_tac); a (wf_induction_tac (asm_rule ⌜well_founded r⌝) ⌜x⌝); a (REPEAT strip_tac); a (spec_nth_asm_tac 4 ⌜z⌝); a (all_asm_fc_tac [fixed_below_lemma1]); a (list_spec_nth_asm_tac 3 [⌜g⌝, ⌜h⌝]); a (all_asm_fc_tac [fixed_at_lemma2]); a (all_asm_fc_tac [get_spec ⌜fixed_at⌝]); a (all_asm_fc_tac [fixed_at_lemma1]); a (all_asm_fc_tac [get_spec ⌜$respects⌝]); a (GET_ASM_T ⌜f h z = h z⌝ (rewrite_thm_tac o eq_sym_rule)); a (GET_ASM_T ⌜f h z = f g z⌝ rewrite_thm_tac); a strip_tac; val fixed_below_lemma2 = save_pop_thm "fixed_below_lemma2";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀g x• fixed_at f r g x ⇒ ∀y• tc r y x ⇒ fixed_at f r g y⌝); a (REPEAT strip_tac); a (all_fc_tac [get_spec ⌜fixed_at⌝]); a (all_fc_tac[fixed_at_lemma2]); val fixed_at_lemma4 = save_pop_thm "fixed_at_lemma4";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀g h x• fixed_at f r g x ∧ fixed_at f r h x ⇒ g x = h x⌝); a (REPEAT strip_tac); a (fc_tac[get_spec ⌜$respects⌝]); a (all_fc_tac[get_spec ⌜fixed_at⌝]); a (all_asm_fc_tac[get_spec ⌜$respects⌝]); a (fc_tac[get_spec ⌜fixed_below⌝]); a (fc_tac[fixed_below_lemma2]); a (asm_fc_tac[]); a (asm_fc_tac[]); a (asm_fc_tac[]); a (asm_fc_tac[]); a (POP_ASM_T discard_tac); a (eq_sym_nth_asm_tac 16); a (eq_sym_nth_asm_tac 15); a (asm_rewrite_tac[]); val fixed_at_lemma5 = save_pop_thm "fixed_at_lemma5";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x• (∀y• tc r y x ⇒ ∃g• fixed_at f r g y) ⇒ ∃g• fixed_below f r g x⌝); a (REPEAT strip_tac); a (∃_tac ⌜λz• (εh• fixed_at f r h z) z⌝); a (rewrite_tac [get_spec ⌜fixed_below⌝] THEN REPEAT strip_tac); a (GET_ASM_T ⌜f respects r⌝ ante_tac THEN rewrite_tac [list_∀_elim [⌜f⌝, ⌜r⌝] (get_spec ⌜$respects⌝)] THEN strip_tac); a (list_spec_nth_asm_tac 1 [⌜λ z• (ε h• fixed_at f r h z) z⌝, ⌜ε h• fixed_at f r h y⌝]); a (spec_nth_asm_tac 1 ⌜y⌝); (* *** Goal "1" *** *) a (swap_nth_asm_concl_tac 1 THEN rewrite_tac[]); a (asm_fc_tac[fixed_at_lemma4]); a (list_spec_nth_asm_tac 2 [⌜f⌝, ⌜g⌝, ⌜y⌝, ⌜y'⌝]); a (asm_fc_tac[]); a (all_ε_tac); (* *** Goal "1.1" *** *) a (∃_tac ⌜g⌝ THEN asm_rewrite_tac[]); (* *** Goal "1.2" *** *) a (∃_tac ⌜g⌝ THEN asm_rewrite_tac[]); (* *** Goal "1.3" *** *) a (∃_tac ⌜g⌝ THEN asm_rewrite_tac[]); (* *** Goal "1.4" *** *) a (asm_tac fixed_at_lemma4); a (list_spec_nth_asm_tac 1 [⌜f⌝, ⌜r⌝]); a (list_spec_nth_asm_tac 1 [⌜ε h• fixed_at f r h y⌝, ⌜y⌝]); a (list_spec_nth_asm_tac 1 [⌜y'⌝]); a (all_asm_fc_tac[fixed_at_lemma5]); (* *** Goal "2" *** *) a (asm_rewrite_tac[]); a (all_asm_fc_tac[]); a (all_ε_tac); (* *** Goal "2.1" *** *) a (∃_tac ⌜g⌝ THEN asm_rewrite_tac[]); (* *** Goal "2.2" *** *) a (all_fc_tac[get_spec ⌜fixed_at⌝]); val fixed_below_lemma3 = save_pop_thm "fixed_below_lemma3";

xl-sml set_goal ([],⌜∀r f• well_founded r ∧ f respects r ⇒ ∀x• ∃g• fixed_below f r g x ⌝); a (REPEAT_N 4 strip_tac); a (wf_induction_tac (asm_rule ⌜well_founded r⌝) ⌜x⌝); a (lemma_tac ⌜∀ u• tc r u t ⇒ (∃ g• fixed_at f r g u)⌝ THEN1 (REPEAT strip_tac THEN all_asm_fc_tac[] THEN all_fc_tac[fixed_at_lemma1] THEN ∃_tac ⌜f g⌝ THEN asm_rewrite_tac[])); a (all_fc_tac[fixed_below_lemma3]); a (∃_tac ⌜g⌝ THEN strip_tac); val fixed_below_lemma4 = save_pop_thm "fixed_below_lemma4";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x• ∃g• fixed_at f r g x ⌝); a (REPEAT_N 4 strip_tac); a (all_fc_tac[fixed_below_lemma4]); a (spec_nth_asm_tac 1 ⌜x⌝); a (∃_tac ⌜f g⌝); a (all_fc_tac[fixed_at_lemma1]); val fixed_at_lemma6 = save_pop_thm "fixed_at_lemma6";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∀x• fixed_at f r (λ x• (ε h• fixed_at f r h x) x) x⌝); a (REPEAT strip_tac); a (lemma_tac ⌜∃g• (λ x• (ε h• fixed_at f r h x) x) = g⌝ THEN1 prove_∃_tac); a (asm_rewrite_tac[]); a (wf_induction_tac (asm_rule ⌜well_founded r⌝) ⌜x⌝); a (rewrite_tac[get_spec ⌜fixed_at⌝] THEN strip_tac); (* *** Goal "1" *** *) a (asm_fc_tac [list_∀_elim [⌜f⌝, ⌜r⌝] fixed_at_lemma3]); a (asm_fc_tac []); a (list_spec_nth_asm_tac 1 [⌜t⌝, ⌜g⌝]); a (asm_fc_tac []); (* *** Goal "2" *** *) a (fc_tac [list_∀_elim [⌜f⌝, ⌜r⌝] fixed_at_lemma6]); a (list_spec_nth_asm_tac 1 [⌜f⌝, ⌜t⌝]); a (fc_tac [get_spec ⌜fixed_at⌝]); a (lemma_tac ⌜g t = g' t⌝ THEN1 (GET_NTH_ASM_T 6 (rewrite_thm_tac o eq_sym_rule))); (* *** Goal "2.1" *** *) a (ε_tac ⌜ε h• fixed_at f r h t⌝); (* *** Goal "2.1.1" *** *) a (∃_tac ⌜g'⌝ THEN asm_rewrite_tac[]); (* *** Goal "2.1.2" *** *) a (fc_tac [get_spec ⌜fixed_at⌝]); a (fc_tac [fixed_at_lemma5]); a (list_spec_nth_asm_tac 1 [⌜f⌝, ⌜ε h• fixed_at f r h t⌝, ⌜t⌝, ⌜g'⌝]); (* *** Goal "2.2" *** *) a (fc_tac [get_spec ⌜$respects⌝]); a (list_spec_nth_asm_tac 1 [⌜t⌝, ⌜g⌝, ⌜g'⌝]); (* *** Goal "2.2.1" *** *) a (asm_fc_tac []); a (asm_fc_tac [fixed_at_lemma4]); a (list_spec_nth_asm_tac 1 [⌜f⌝, ⌜g'⌝, ⌜t⌝, ⌜y⌝]); a (asm_fc_tac [fixed_at_lemma5]); a (REPEAT (asm_fc_tac[])); (* *** Goal "2.2.2" *** *) a (asm_rewrite_tac[]); val fixed_lemma1 = save_pop_thm "fixed_lemma1";

xl-sml set_goal ([],⌜∀f r• well_founded r ∧ f respects r ⇒ ∃g• f g = g⌝); a (REPEAT strip_tac); a (∃_tac ⌜λx• (εh• fixed_at f r h x) x⌝ THEN rewrite_tac [ext_thm] THEN REPEAT strip_tac); a (all_fc_tac [list_∀_elim [⌜f⌝, ⌜r⌝] fixed_lemma1]); a (spec_nth_asm_tac 1 ⌜x⌝); a (all_fc_tac [get_spec ⌜fixed_at⌝]); a (asm_rewrite_tac[]); val fixp_thm1 = save_pop_thm "fixp_thm1";

xl-sml set_goal ([],⌜∃fix• ∀f r•well_founded r ∧ f respects r ⇒ f (fix f) = (fix f)⌝); a (∃_tac ⌜λf• εg• f g = g⌝); a (REPEAT strip_tac THEN rewrite_tac[]); a (all_ε_tac); a (all_fc_tac [fixp_thm1]); a (∃_tac ⌜g⌝ THEN strip_tac); val _ = xl_set_cs_∃_thm (pop_thm ());

xl-holconst fix: (('a → 'b) → ('a → 'b)) → 'a → 'b

∀f r• well_founded r ∧ f respects r ⇒ f (fix f) = fix f

My first applications of the recursion theorem are in set theory, typically involving recursion which respects membership or its transitive closure.

The following function takes a relation and a function and returns a function which maps each element in the domain of the relation to the relation which holds between a predecessor of that element and its value under the function. i.e. it maps the function over the predecessors of the element and returns the result as a relation. It may therefore be used to rephrase primitive recursive definitions, and so the result which follows may be used to establish the existence of functions defined by primitive recursion.

xl-holconst relmap : ('a → 'a → BOOL) → ('a → 'b) → ('a → ('a → 'b → BOOL))

∀r f• relmap r f = λx y z• r y x ∧ z = f y

xl-sml set_goal ([],⌜∀r g• (λf• g o (relmap r f)) respects r⌝); a (rewrite_tac[get_spec ⌜$respects⌝, get_spec ⌜relmap⌝, get_spec ⌜$o⌝] THEN REPEAT strip_tac); a (lemma_tac ⌜(λ y z• r y x ∧ z = g' y) = (λ y z• r y x ∧ z = h y)⌝ THEN1 rewrite_tac[ext_thm]); (* *** Goal "1" *** *) a (REPEAT strip_tac); (* *** Goal "1.2" *** *) a (asm_fc_tac[tc_incr_thm]); a (asm_fc_tac[]); a (asm_rewrite_tac []); (* *** Goal "1.2" *** *) a (asm_fc_tac[tc_incr_thm]); a (asm_fc_tac[]); a (asm_rewrite_tac []); (* *** Goal "2" *** *) a (asm_rewrite_tac []); val relmap_respect_thm = save_pop_thm "relmap_respect_thm";

xl-sml (* commit_pc "wf_relp"; *)