A new "wf_rec" theory is created as a child of "wf_rel". Probably

In this section is proved the theorem which justifies well-founded recursive definitions.

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

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"];

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 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-holconst is_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}) }

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";

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_specis_recfun, bin_rel_ext_clauses, _in_clauses]); a (fc_tac [get_specis_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_spectwf,get_specTransitive]); 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_spectwf,get_specTransitive]); 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_spectwf,get_specTransitive]); 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_spectwf]); a (strip_asm_tac (_elim R (get_specwf)) 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_specis_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-holconst the_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-holconst wftrecfun: (('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-holconst wftrec: (('a 'a)SET 'a (('a ('a 'a)SET) 'a)) 'a

r a H wftrec (r,a,H) = H(a,the_recfun(r,a,H))

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