Well-Founded Recursion
Overview
 This is a proof of the recursion theorem for well-founded recursive definitions. It is modelled on Tobias Nipkow's proof for Isabelle HOL and uses relations modelled with ProofPower HOL's SET type constructor.
 Introduction A new "wf_rec" theory is created as a child of "wf_rel". Probably Well-Founded Recursion In this section is proved the theorem which justifies well-founded recursive definitions. Recursive Definition
 Proof Context In this section I will create a decent proof context for recursive definitions, eventually. Listing of Theory wf_rec
Introduction
 A new "wf_rec" theory is created as a child of "wf_rel". Probably
The Theory wf_rec
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_rel"; force_new_theory "wf_rec"; force_new_pc "wf_rec"; merge_pcs ["xl_cs_∃_conv"] "wf_rec"; set_merge_pcs ["hol", "'bin_rel", "wf_rec"];

Well-Founded Recursion
 In this section is proved the theorem which justifies well-founded recursive definitions.
Introduction

The idea here is that a recursive equation is represented by a functional, which is obtained by abstracting the right hand side of the equation on the name of the function. We need to demonstrate that definitions using such a functional have unique solutions.

Is RecFun
is_recfun is the set of 4-tuples <r,a,H,f> such that f solves the recursion equations represented by H for values which are in the left image of a under R. (following Tobias Nipkow)
 xl-holconstis_recfun: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a) × ('a × 'a)SET)SET ∀ r a H f • (r,a,H,f) ∈ is_recfun ≡ f = {(x,y)| (x,a) ∈ r ∧ y = H(x, {(v,w)| (v,w) ∈ f ∧ (v,x) ∈ r}) }
Restriction Intersection
The following lemma states that two restriced recursive functions agree over their intersection.
 xl-sml set_goal([],⌜∀r H a f b g• r ∈ twf ∧ (r,a,H,f) ∈ is_recfun ∧ (r,b,H,g) ∈ is_recfun ⇒ ∀x• (x,a)∈r ∧ (x,b)∈r ⇒ ∀y•(x,y)∈f ≡ (x,y)∈g⌝); a (rewrite_tac(map get_spec [⌜twf⌝, ⌜wf⌝, ⌜is_recfun⌝])); a (REPEAT_N 7 strip_tac); a (spec_nth_asm_tac 4 ⌜{x | (x, a) ∈ r ∧ (x, b) ∈ r ⇒ ∀y•(x,y)∈f ≡ (x,y)∈g}⌝); (* *** Goal "1" *** *) a (SWAP_NTH_ASM_CONCL_T 1 discard_tac); a (all_asm_ante_tac THEN REPEAT_N 5 strip_tac); a (once_asm_rewrite_tac[]); a (rewrite_tac[] THEN REPEAT strip_tac); a (DROP_NTH_ASM_T 1 rewrite_thm_tac); a (LEMMA_T ⌜{(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ g ∧ (v, x) ∈ r}⌝ rewrite_thm_tac); a (rewrite_tac[bin_rel_ext_clauses]); a (REPEAT strip_tac); a (spec_nth_asm_tac 5 ⌜x'⌝ THEN all_asm_fc_tac[]); a (spec_nth_asm_tac 5 ⌜x'⌝ THEN all_asm_fc_tac[]); a (spec_nth_asm_tac 3 ⌜y⌝); (* *** Goal "2" *** *) a (SWAP_NTH_ASM_CONCL_T 1 discard_tac); a (all_asm_ante_tac THEN REPEAT_N 5 strip_tac); a (once_asm_rewrite_tac[]); a (rewrite_tac[] THEN REPEAT strip_tac); a (DROP_NTH_ASM_T 1 rewrite_thm_tac); a (LEMMA_T ⌜{(v, w)|(v, w) ∈ g ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝ rewrite_thm_tac); a (rewrite_tac[bin_rel_ext_clauses]); a (REPEAT strip_tac); a (spec_nth_asm_tac 5 ⌜x'⌝ THEN all_asm_fc_tac[]); a (spec_nth_asm_tac 3 ⌜y⌝); a (spec_nth_asm_tac 5 ⌜x'⌝ THEN all_asm_fc_tac[]); (* *** Goal "3" *** *) a (strip_tac THEN strip_tac); a (spec_nth_asm_tac 3 ⌜x⌝); val ri_lemma = save_pop_thm "ri_lemma";

Restrict Unique
An immediate corrolory is that there is only one restricted recursive function at any point. First, however we prove a lemma about the domain of a restricted recursive function.
 xl-sml set_goal([],⌜∀r a H f• (r,a,H,f) ∈ is_recfun ⇒ Dom f = {x | (x,a) ∈ r}⌝); a (REPEAT strip_tac); a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜a⌝,⌜H⌝,⌜f⌝] (get_spec ⌜is_recfun⌝))); a (once_asm_rewrite_tac[] THEN rewrite_tac[sets_ext_clauses, ∈_in_clauses]); a (once_asm_rewrite_tac[]); a (prove_tac[sets_ext_clauses, ∈_in_clauses]); val recfun_Dom_thm = save_pop_thm "recfun_Dom_thm";

 xl-sml set_goal([],⌜∀r H a f g• r ∈ twf ∧ (r,a,H,f) ∈ is_recfun ∧ (r,a,H,g) ∈ is_recfun ⇒ f = g⌝); a (REPEAT strip_tac); a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜H⌝,⌜a⌝,⌜f⌝,⌜a⌝,⌜g⌝] ri_lemma)); a (pure_rewrite_tac [rel_ext_Dom_thm]); a (FC_T rewrite_tac [recfun_Dom_thm]); a (asm_prove_tac[]); val recfun_unique_thm = save_pop_thm "recfun_unique_thm";

 xl-sml set_goal([],⌜∀r H a f b g• r ∈ twf ∧ (r,a,H,f) ∈ is_recfun ∧ (r,b,H,g) ∈ is_recfun ∧ (a,b) ∈ r ⇒ f = (Dom f) ⊲ g⌝); a (REPEAT strip_tac); a (strip_asm_tac (list_∀_elim [⌜r⌝,⌜H⌝,⌜a⌝,⌜f⌝,⌜b⌝,⌜g⌝] ri_lemma)); a (fc_tac [recfun_Dom_thm, get_spec ⌜twf⌝]); a (pure_asm_rewrite_tac [rel_ext_Dom_thm, Dom_rest_thm]); a (rewrite_tac [rel_ext_Dom_thm, sets_ext_clauses, ∈_in_clauses]); a (REPEAT strip_tac THEN_TRY all_asm_fc_tac[]); a (spec_asm_tac ⌜∀ x• (x, a) ∈ r ∧ (x, b) ∈ r ⇒ (∀ y• (x, y) ∈ f ≡ (x, y) ∈ g)⌝ ⌜x⌝); a (asm_rewrite_tac[]); val recfun_restr_lemma = save_pop_thm "recfun_restr_lemma";

 xl-sml set_goal([],⌜∀r H a f b• r ∈ twf ∧ (r,a,H,f) ∈ is_recfun ∧ (b,a) ∈ r ⇒ (r,b,H,{(v,w) | (v,w) ∈ f ∧ (v,b) ∈ r}) ∈ is_recfun⌝); a (REPEAT strip_tac); a (rewrite_tac [get_spec⌜is_recfun⌝, bin_rel_ext_clauses, ∈_in_clauses]); a (fc_tac [get_spec⌜is_recfun⌝]); a (REPEAT_N 4 strip_tac); (* *** Goal "1" *** *) a (GET_NTH_ASM_T 1 (fn asm=>STRIP_T (fn x => strip_asm_tac(once_rewrite_rule[asm]x)))); a (REPEAT strip_tac); a (lemma_tac ⌜{(v, w)|((v, w) ∈ f ∧ (v, b) ∈ r) ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝ THEN1 (rewrite_tac [bin_rel_ext_clauses,∈_in_clauses])); (* *** Goal "1.1" *** *) a (REPEAT strip_tac); a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]); a (all_asm_fc_tac[]); (* *** Goal "1.2" *** *) a (pure_once_asm_rewrite_tac[]); a (rewrite_tac[]); (* *** Goal "2" *** *) a (REPEAT strip_tac); a (once_asm_rewrite_tac[]); a (rewrite_tac[]); a (REPEAT strip_tac); (* *** Goal "2.1" *** *) a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]); a (all_asm_fc_tac[]); (* *** Goal "2.2" *** *) a (lemma_tac ⌜{(v, w)|((v, w) ∈ f ∧ (v, b) ∈ r) ∧ (v, x) ∈ r} = {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r}⌝ THEN1 (rewrite_tac [bin_rel_ext_clauses,∈_in_clauses])); (* *** Goal "2.2.1" *** *) a (REPEAT strip_tac); a (fc_tac [get_spec⌜twf⌝,get_spec⌜Transitive⌝]); a (all_asm_fc_tac[]); (* *** Goal "2.2.2" *** *) a (GET_NTH_ASM_T 1 (fn x=> pure_once_rewrite_tac[x])); a (rewrite_tac[]); val restr_is_recfun_lemma = save_pop_thm "restr_is_recfun_lemma";

Now the big one:
 xl-sml set_goal([],⌜∀H R a• R ∈ twf ⇒ ∃f• (R, a, H, f) ∈ is_recfun⌝); a (REPEAT strip_tac); a (fc_tac[get_spec⌜twf⌝]); a (strip_asm_tac (∀_elim ⌜R⌝ (get_spec⌜wf⌝)) THEN1 REPEAT (all_asm_fc_tac[])); a (spec_nth_asm_tac 1 ⌜{z|∃ f• (R, z, H, f) ∈ is_recfun}⌝); (* *** Goal "1" *** *) a (SWAP_NTH_ASM_CONCL_T 1 discard_tac THEN strip_tac); a (lemma_tac ⌜∃g• g = { (v,w) | (v,x) ∈ R ∧ ∃h• (R,v,H,h) ∈ is_recfun ∧ w = H(v,h)}⌝ THEN1 prove_∃_tac); a (∃_tac ⌜g⌝); a (rewrite_tac[get_spec ⌜is_recfun⌝, bin_rel_ext_clauses, ∈_in_clauses]); a (REPEAT strip_tac); (* *** Goal "1.1" *** *) a (asm_ante_tac ⌜(x', y) ∈ g⌝); a (asm_rewrite_tac[] THEN REPEAT strip_tac); (* *** Goal "1.2" *** *) a (swap_asm_concl_tac ⌜(x', y) ∈ g⌝); a (asm_rewrite_tac[] THEN swap_nth_asm_concl_tac 1); a (spec_nth_asm_tac 5 ⌜x'⌝); a (lemma_tac ⌜h={(v, w)|(v, w) ∈ g ∧ (v, x') ∈ R}⌝); (* *** Goal "1.2.1" *** *) a (asm_rewrite_tac[bin_rel_ext_clauses, ∈_in_clauses]); a (strip_tac THEN strip_tac THEN asm_rewrite_tac[]); a (FC_T once_rewrite_tac [get_spec⌜is_recfun⌝]); a (rewrite_tac[]); a (REPEAT strip_tac); (* *** Goal "1.2.1.1" *** *) a (all_asm_fc_tac[]); (* *** Goal "1.2.1.2" *** *) a (∃_tac ⌜{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}⌝ THEN asm_rewrite_tac[]); a (strip_asm_tac (list_∀_elim [⌜R⌝,⌜H⌝,⌜x'⌝,⌜h⌝,⌜x''⌝] restr_is_recfun_lemma)); (* *** Goal "1.2.1.3" *** *) a (lemma_tac ⌜(R,x'',H,{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}) ∈ is_recfun⌝ THEN1 (strip_asm_tac (list_∀_elim [⌜R⌝,⌜H⌝,⌜x'⌝,⌜h⌝,⌜x''⌝] restr_is_recfun_lemma))); a (strip_asm_tac (list_∀_elim [⌜R⌝,⌜H⌝,⌜x''⌝,⌜{(v, w)|(v, w) ∈ h ∧ (v, x'') ∈ R}⌝,⌜h'⌝] recfun_unique_thm)); a (asm_rewrite_tac[]); (* *** Goal "1.2.2" *** *) a (asm_ante_tac ⌜y = H (x', h)⌝); a (GET_ASM_T ⌜h = {(v, w)|(v, w) ∈ g ∧ (v, x') ∈ R}⌝ rewrite_thm_tac); (* *** Goal "1.3" *** *) a (asm_rewrite_tac[]); a (spec_asm_tac ⌜∀ y• (y, x) ∈ R ⇒ y ∈ {z|∃ f• (R, z, H, f) ∈ is_recfun}⌝ ⌜x'⌝); a (∃_tac ⌜f⌝ THEN asm_rewrite_tac[]); a (lemma_tac ⌜{(v, w) |((v, x) ∈ R ∧ (∃ h• (R, v, H, h) ∈ is_recfun ∧ w = H (v, h))) ∧ (v, x') ∈ R} = f⌝); (* *** Goal "1.3.1" *** *) a (rewrite_tac[bin_rel_ext_clauses]); a (REPEAT strip_tac); (* *** Goal "1.3.1.1" *** *) a (all_fc_tac [recfun_restr_lemma]); a (all_fc_tac [recfun_Dom_thm]); a (all_fc_tac [get_spec ⌜is_recfun⌝]); a (once_asm_rewrite_tac[]); a (rewrite_tac[∈_in_clauses]); (*a (once_asm_rewrite_tac[]);*) a (lemma_tac ⌜{(v, w)|(v, w) ∈ f ∧ (v, x'') ∈ R} = h⌝); a ((POP_ASM_T discard_tac) THEN (POP_ASM_T discard_tac) THEN once_asm_rewrite_tac[]); a (GET_ASM_T ⌜Dom h = {x|(x, x'') ∈ R}⌝ pure_rewrite_thm_tac); a (prove_tac[bin_rel_ext_clauses]); a (POP_ASM_T rewrite_thm_tac THEN strip_tac); (* *** Goal "1.3.1.2" *** *) a (POP_ASM_T ante_tac); a (ALL_FC_T (MAP_EVERY ante_tac) [recfun_Dom_thm]); a (rewrite_tac[sets_ext_clauses]); a (REPEAT strip_tac); a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝ ⌜x''⌝); (* *** Goal "1.3.1.2.1" *** *) a (REPEAT (asm_fc_tac[])); a (REPEAT (asm_fc_tac[])); a (REPEAT (asm_fc_tac[])); (* *** Goal "1.3.1.3" *** *) a (∃_tac ⌜{(x,y)| (x,y) ∈ f ∧ (x,x'') ∈ R}⌝ THEN REPEAT strip_tac); (* *** Goal "1.3.1.3.1" *** *) a (ALL_FC_T (MAP_EVERY(asm_tac o (rewrite_rule[sets_ext_clauses]))) [recfun_Dom_thm]); a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝ ⌜x''⌝); a (asm_fc_tac[]); a (asm_fc_tac[]); a (all_fc_tac [restr_is_recfun_lemma]); (* *** Goal "1.3.1.3.2" *** *) a (ALL_FC_T (MAP_EVERY ante_tac) [get_spec ⌜is_recfun⌝]); a (POP_ASM_T (fn a=> STRIP_T (fn h=> ante_tac (once_rewrite_rule[h]a)))); a (rewrite_tac [∈_in_clauses]); a (strip_tac); (* *** Goal "1.3.1.4" *** *) a (ALL_FC_T (MAP_EVERY(asm_tac o (rewrite_rule[sets_ext_clauses]))) [recfun_Dom_thm]); a (spec_asm_tac ⌜∀ x• (∃ y• (x, y) ∈ f) ≡ (x, x') ∈ R⌝ ⌜x''⌝); a (asm_fc_tac[]); a (asm_fc_tac[]); (* *** Goal "1.3.2" *** *) a (asm_rewrite_tac[]); (* *** Goal "2" *** *) a (spec_asm_tac ⌜∀ x• x ∈ {z|∃ f• (R, z, H, f) ∈ is_recfun}⌝ ⌜a⌝); a (∃_tac ⌜f⌝ THEN strip_tac); val exists_recfun_thm = save_pop_thm "exists_recfun_thm";

 xl-sml set_goal([],⌜∃ the_recfun • ∀ r a H• r ∈ twf ⇒ (r, a, H, the_recfun (r, a, H)) ∈ is_recfun⌝); a (PC_T "hol" prove_∃_tac THEN strip_tac); a (∃_tac ⌜εrecfun• Fst x ∈ twf ⇒ (Fst x, Fst (Snd x), Snd (Snd x), recfun) ∈ is_recfun⌝); a strip_tac; a (fc_tac[list_∀_elim [⌜Snd(Snd x)⌝,⌜Fst x⌝,⌜Fst (Snd x)⌝] exists_recfun_thm]); a (all_ε_tac); a (∃_tac ⌜f⌝ THEN asm_rewrite_tac[]); val recfun_consistent = top_thm(); xl_set_cs_∃_thm (pop_thm());

 xl-holconstthe_recfun: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a)) → ('a × 'a)SET ∀ r a H• r ∈ twf ⇒ (r,a,H,the_recfun(r,a,H)) ∈ is_recfun
We now define the function wftrec which delivers a solution to a recursion functional.
 xl-holconstwftrecfun: (('a × 'a)SET × (('a × ('a × 'a)SET) → 'a)) → ('a × 'a)SET ∀ r H• wftrecfun (r,H) = {(a,v) | v = H(a,the_recfun(r,a,H))}
The following theorem shows that this is indeed a fixed-point.
 xl-holconstwftrec: (('a × 'a)SET × 'a × (('a × ('a × 'a)SET) → 'a)) → 'a ∀ r a H• wftrec (r,a,H) = H(a,the_recfun(r,a,H))
Recursion Theorem
Proof Context
 In this section I will create a decent proof context for recursive definitions, eventually.
Proof Context

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