0

1 
(* Title: ZF/wf.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow and Lawrence C Paulson


4 
Copyright 1992 University of Cambridge


5 


6 
For wf.thy. Wellfounded Recursion


7 


8 
Derived first for transitive relations, and finally for arbitrary WF relations


9 
via wf_trancl and trans_trancl.


10 


11 
It is difficult to derive this general case directly, using r^+ instead of


12 
r. In is_recfun, the two occurrences of the relation must have the same


13 
form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with


14 
r^+ `` {a} instead of r``{a}. This recursion rule is stronger in


15 
principle, but harder to use, especially to prove wfrec_eclose_eq in


16 
epsilon.ML. Expanding out the definition of wftrec in wfrec would yield


17 
a mess.


18 
*)


19 


20 
open WF;


21 


22 
val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")];


23 


24 
val wf_ss = ZF_ss addcongs [H_cong];


25 


26 


27 
(*** Wellfounded relations ***)


28 


29 
(*Are these two theorems at all useful??*)


30 


31 
(*If every subset of field(r) possesses an rminimal element then wf(r).


32 
Seems impossible to prove this for domain(r) or range(r) instead...


33 
Consider in particular finite wf relations!*)


34 
val [prem1,prem2] = goalw WF.thy [wf_def]


35 
"[ field(r)<=A; \


36 
\ !!Z u. [ Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r ] ==> False ] \


37 
\ ==> wf(r)";


38 
by (rtac (equals0I RS disjCI RS allI) 1);


39 
by (rtac prem2 1);


40 
by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1);


41 
by (fast_tac ZF_cs 1);


42 
by (fast_tac ZF_cs 1);


43 
val wfI = result();


44 


45 
(*If r allows wellfounded induction then wf(r)*)


46 
val [prem1,prem2] = goal WF.thy


47 
"[ field(r)<=A; \


48 
\ !!B. ALL x:A. (ALL y. <y,x>: r > y:B) > x:B ==> A<=B ] \


49 
\ ==> wf(r)";


50 
by (rtac (prem1 RS wfI) 1);


51 
by (res_inst_tac [ ("B", "AZ") ] (prem2 RS subsetCE) 1);


52 
by (fast_tac ZF_cs 3);


53 
by (fast_tac ZF_cs 2);


54 
by (fast_tac ZF_cs 1);


55 
val wfI2 = result();


56 


57 


58 
(** Wellfounded Induction **)


59 


60 
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)


61 
val major::prems = goalw WF.thy [wf_def]


62 
"[ wf(r); \


63 
\ !!x.[ ALL y. <y,x>: r > P(y) ] ==> P(x) \


64 
\ ] ==> P(a)";


65 
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1);


66 
by (etac disjE 1);


67 
by (rtac classical 1);


68 
by (etac equals0D 1);


69 
by (etac (singletonI RS UnI2 RS CollectI) 1);


70 
by (etac bexE 1);


71 
by (etac CollectE 1);


72 
by (etac swap 1);


73 
by (resolve_tac prems 1);


74 
by (fast_tac ZF_cs 1);


75 
val wf_induct = result();


76 


77 
(*Perform induction on i, then prove the wf(r) subgoal using prems. *)


78 
fun wf_ind_tac a prems i =


79 
EVERY [res_inst_tac [("a",a)] wf_induct i,


80 
rename_last_tac a ["1"] (i+1),


81 
ares_tac prems i];


82 


83 
(*The form of this rule is designed to match wfI2*)


84 
val wfr::amem::prems = goal WF.thy


85 
"[ wf(r); a:A; field(r)<=A; \


86 
\ !!x.[ x: A; ALL y. <y,x>: r > P(y) ] ==> P(x) \


87 
\ ] ==> P(a)";


88 
by (rtac (amem RS rev_mp) 1);


89 
by (wf_ind_tac "a" [wfr] 1);


90 
by (rtac impI 1);


91 
by (eresolve_tac prems 1);


92 
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);


93 
val wf_induct2 = result();


94 


95 
val prems = goal WF.thy "[ wf(r); <a,x>:r; <x,a>:r ] ==> False";


96 
by (subgoal_tac "ALL x. <a,x>:r > <x,a>:r > False" 1);


97 
by (wf_ind_tac "a" prems 2);


98 
by (fast_tac ZF_cs 2);


99 
by (fast_tac (FOL_cs addIs prems) 1);


100 
val wf_anti_sym = result();


101 


102 
(*transitive closure of a WF relation is WF!*)


103 
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";


104 
by (rtac (trancl_type RS field_rel_subset RS wfI2) 1);


105 
by (rtac subsetI 1);


106 
(*must retain the universal formula for later use!*)


107 
by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1);


108 
by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1);


109 
by (rtac subset_refl 1);


110 
by (rtac (impI RS allI) 1);


111 
by (etac tranclE 1);


112 
by (etac (bspec RS mp) 1);


113 
by (etac fieldI1 1);


114 
by (fast_tac ZF_cs 1);


115 
by (fast_tac ZF_cs 1);


116 
val wf_trancl = result();


117 


118 
(** r``{a} is the set of everything under a in r **)


119 


120 
val underI = standard (vimage_singleton_iff RS iffD2);


121 
val underD = standard (vimage_singleton_iff RS iffD1);


122 


123 
(** is_recfun **)


124 


125 
val [major] = goalw WF.thy [is_recfun_def]


126 
"is_recfun(r,a,H,f) ==> f: r``{a} > range(f)";


127 
by (rtac (major RS ssubst) 1);


128 
by (rtac (lamI RS rangeI RS lam_type) 1);


129 
by (assume_tac 1);


130 
val is_recfun_type = result();


131 


132 
val [isrec,rel] = goalw WF.thy [is_recfun_def]


133 
"[ is_recfun(r,a,H,f); <x,a>:r ] ==> f`x = H(x, restrict(f,r``{x}))";


134 
by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1);


135 
by (rtac (rel RS underI RS beta) 1);


136 
val apply_recfun = result();


137 


138 
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE


139 
spec RS mp instantiates induction hypotheses*)


140 
fun indhyp_tac hyps =


141 
ares_tac (TrueI::hyps) ORELSE'


142 
(cut_facts_tac hyps THEN'


143 
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'


144 
eresolve_tac [underD, transD, spec RS mp]));


145 


146 
(*** NOTE! some simplifications need a different auto_tac!! ***)


147 
val wf_super_ss = wf_ss setauto indhyp_tac;


148 


149 
val prems = goalw WF.thy [is_recfun_def]


150 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) ] ==> \


151 
\ <x,a>:r > <x,b>:r > f`x=g`x";


152 
by (cut_facts_tac prems 1);


153 
by (wf_ind_tac "x" prems 1);


154 
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));


155 
by (rewtac restrict_def);


156 
by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1);


157 
val is_recfun_equal_lemma = result();


158 
val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);


159 


160 
val prems as [wfr,transr,recf,recg,_] = goal WF.thy


161 
"[ wf(r); trans(r); \


162 
\ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r ] ==> \


163 
\ restrict(f, r``{b}) = g";


164 
by (cut_facts_tac prems 1);


165 
by (rtac (consI1 RS restrict_type RS fun_extension) 1);


166 
by (etac is_recfun_type 1);


167 
by (ALLGOALS


168 
(ASM_SIMP_TAC (wf_super_ss addrews


169 
[ [wfr,transr,recf,recg] MRS is_recfun_equal ])));


170 
val is_recfun_cut = result();


171 


172 
(*** Main Existence Lemma ***)


173 


174 
val prems = goal WF.thy


175 
"[ wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) ] ==> f=g";


176 
by (cut_facts_tac prems 1);


177 
by (rtac fun_extension 1);


178 
by (REPEAT (ares_tac [is_recfun_equal] 1


179 
ORELSE eresolve_tac [is_recfun_type,underD] 1));


180 
val is_recfun_functional = result();


181 


182 
(*If some f satisfies is_recfun(r,a,H,) then so does the_recfun(r,a,H) *)


183 
val prems = goalw WF.thy [the_recfun_def]


184 
"[ is_recfun(r,a,H,f); wf(r); trans(r) ] \


185 
\ ==> is_recfun(r, a, H, the_recfun(r,a,H))";


186 
by (rtac (ex1I RS theI) 1);


187 
by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1));


188 
val is_the_recfun = result();


189 


190 
val prems = goal WF.thy


191 
"[ wf(r); trans(r) ] ==> is_recfun(r, a, H, the_recfun(r,a,H))";


192 
by (cut_facts_tac prems 1);


193 
by (wf_ind_tac "a" prems 1);


194 
by (res_inst_tac [("f", "lam y: r``{a1}. wftrec(r,y,H)")] is_the_recfun 1);


195 
by (REPEAT (assume_tac 2));


196 
by (rewrite_goals_tac [is_recfun_def, wftrec_def]);


197 
(*Applying the substitution: must keep the quantified assumption!!*)


198 
by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1));


199 
by (fold_tac [is_recfun_def]);


200 
by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1);


201 
by (rtac is_recfun_type 1);


202 
by (ALLGOALS


203 
(ASM_SIMP_TAC


204 
(wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut])));


205 
val unfold_the_recfun = result();


206 


207 


208 
(*** Unfolding wftrec ***)


209 


210 
val prems = goal WF.thy


211 
"[ wf(r); trans(r); <b,a>:r ] ==> \


212 
\ restrict(the_recfun(r,a,H), r``{b}) = the_recfun(r,b,H)";


213 
by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1));


214 
val the_recfun_cut = result();


215 


216 
(*NOT SUITABLE FOR REWRITING since it is recursive!*)


217 
val prems = goalw WF.thy [wftrec_def]


218 
"[ wf(r); trans(r) ] ==> \


219 
\ wftrec(r,a,H) = H(a, lam x: r``{a}. wftrec(r,x,H))";


220 
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);


221 
by (ALLGOALS (ASM_SIMP_TAC


222 
(wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym,


223 
the_recfun_cut]))));


224 
val wftrec = result();


225 


226 
(** Removal of the premise trans(r) **)


227 


228 
(*NOT SUITABLE FOR REWRITING since it is recursive!*)


229 
val [wfr] = goalw WF.thy [wfrec_def]


230 
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r``{a}. wfrec(r,x,H))";


231 
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);


232 
by (rtac trans_trancl 1);


233 
by (rtac (refl RS H_cong) 1);


234 
by (rtac (vimage_pair_mono RS restrict_lam_eq) 1);


235 
by (etac r_into_trancl 1);


236 
by (rtac subset_refl 1);


237 
val wfrec = result();


238 


239 
(*This form avoids giant explosions in proofs. NOTE USE OF == *)


240 
val rew::prems = goal WF.thy


241 
"[ !!x. h(x)==wfrec(r,x,H); wf(r) ] ==> \


242 
\ h(a) = H(a, lam x: r``{a}. h(x))";


243 
by (rewtac rew);


244 
by (REPEAT (resolve_tac (prems@[wfrec]) 1));


245 
val def_wfrec = result();


246 


247 
val prems = goal WF.thy


248 
"[ wf(r); a:A; field(r)<=A; \


249 
\ !!x u. [ x: A; u: Pi(r``{x}, B) ] ==> H(x,u) : B(x) \


250 
\ ] ==> wfrec(r,a,H) : B(a)";


251 
by (res_inst_tac [("a","a")] wf_induct2 1);


252 
by (rtac (wfrec RS ssubst) 4);


253 
by (REPEAT (ares_tac (prems@[lam_type]) 1


254 
ORELSE eresolve_tac [spec RS mp, underD] 1));


255 
val wfrec_type = result();


256 


257 
val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def]


258 
"[ r=r'; !!x u. H(x,u)=H'(x,u); a=a' ] \


259 
\ ==> wfrec(r,a,H)=wfrec(r',a',H')";


260 
by (EVERY1 (map rtac (prems RL [subst])));


261 
by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1);


262 
val wfrec_cong = result();
