|
1 (* Title: HOL/wf.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For wf.thy. Well-founded Recursion |
|
7 *) |
|
8 |
|
9 open WF; |
|
10 |
|
11 val H_cong = read_instantiate [("f","H::[?'a, ?'a=>?'b]=>?'b")] |
|
12 (standard(refl RS cong RS cong)); |
|
13 val H_cong1 = refl RS H_cong; |
|
14 |
|
15 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
|
16 val [prem1,prem2] = goalw WF.thy [wf_def] |
|
17 "[| r <= Sigma A (%u.A); \ |
|
18 \ !!x P. [| ! x. (! y. <y,x> : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
|
19 \ ==> wf(r)"; |
|
20 by (strip_tac 1); |
|
21 by (rtac allE 1); |
|
22 by (assume_tac 1); |
|
23 by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); |
|
24 qed "wfI"; |
|
25 |
|
26 val major::prems = goalw WF.thy [wf_def] |
|
27 "[| wf(r); \ |
|
28 \ !!x.[| ! y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
29 \ |] ==> P(a)"; |
|
30 by (rtac (major RS spec RS mp RS spec) 1); |
|
31 by (fast_tac (HOL_cs addEs prems) 1); |
|
32 qed "wf_induct"; |
|
33 |
|
34 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
35 fun wf_ind_tac a prems i = |
|
36 EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
37 rename_last_tac a ["1"] (i+1), |
|
38 ares_tac prems i]; |
|
39 |
|
40 val prems = goal WF.thy "[| wf(r); <a,x>:r; <x,a>:r |] ==> P"; |
|
41 by (subgoal_tac "! x. <a,x>:r --> <x,a>:r --> P" 1); |
|
42 by (fast_tac (HOL_cs addIs prems) 1); |
|
43 by (wf_ind_tac "a" prems 1); |
|
44 by (fast_tac set_cs 1); |
|
45 qed "wf_asym"; |
|
46 |
|
47 val prems = goal WF.thy "[| wf(r); <a,a>: r |] ==> P"; |
|
48 by (rtac wf_asym 1); |
|
49 by (REPEAT (resolve_tac prems 1)); |
|
50 qed "wf_anti_refl"; |
|
51 |
|
52 (*transitive closure of a WF relation is WF!*) |
|
53 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
|
54 by (rewtac wf_def); |
|
55 by (strip_tac 1); |
|
56 (*must retain the universal formula for later use!*) |
|
57 by (rtac allE 1 THEN assume_tac 1); |
|
58 by (etac mp 1); |
|
59 by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); |
|
60 by (rtac (impI RS allI) 1); |
|
61 by (etac tranclE 1); |
|
62 by (fast_tac HOL_cs 1); |
|
63 by (fast_tac HOL_cs 1); |
|
64 qed "wf_trancl"; |
|
65 |
|
66 |
|
67 (** cut **) |
|
68 |
|
69 (*This rewrite rule works upon formulae; thus it requires explicit use of |
|
70 H_cong to expose the equality*) |
|
71 goalw WF.thy [cut_def] |
|
72 "(cut f r x = cut g r x) = (!y. <y,x>:r --> f(y)=g(y))"; |
|
73 by(simp_tac (HOL_ss addsimps [expand_fun_eq] |
|
74 setloop (split_tac [expand_if])) 1); |
|
75 qed "cut_cut_eq"; |
|
76 |
|
77 goalw WF.thy [cut_def] "!!x. <x,a>:r ==> (cut f r a)(x) = f(x)"; |
|
78 by(asm_simp_tac HOL_ss 1); |
|
79 qed "cut_apply"; |
|
80 |
|
81 |
|
82 (*** is_recfun ***) |
|
83 |
|
84 goalw WF.thy [is_recfun_def,cut_def] |
|
85 "!!f. [| is_recfun r a H f; ~<b,a>:r |] ==> f(b) = (@z.True)"; |
|
86 by (etac ssubst 1); |
|
87 by(asm_simp_tac HOL_ss 1); |
|
88 qed "is_recfun_undef"; |
|
89 |
|
90 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE |
|
91 mp amd allE instantiate induction hypotheses*) |
|
92 fun indhyp_tac hyps = |
|
93 ares_tac (TrueI::hyps) ORELSE' |
|
94 (cut_facts_tac hyps THEN' |
|
95 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
|
96 eresolve_tac [transD, mp, allE])); |
|
97 |
|
98 (*** NOTE! some simplifications need a different finish_tac!! ***) |
|
99 fun indhyp_tac hyps = |
|
100 resolve_tac (TrueI::refl::hyps) ORELSE' |
|
101 (cut_facts_tac hyps THEN' |
|
102 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
|
103 eresolve_tac [transD, mp, allE])); |
|
104 val wf_super_ss = HOL_ss setsolver indhyp_tac; |
|
105 |
|
106 val prems = goalw WF.thy [is_recfun_def,cut_def] |
|
107 "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \ |
|
108 \ <x,a>:r --> <x,b>:r --> f(x)=g(x)"; |
|
109 by (cut_facts_tac prems 1); |
|
110 by (etac wf_induct 1); |
|
111 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
112 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); |
|
113 qed "is_recfun_equal_lemma"; |
|
114 bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp)); |
|
115 |
|
116 |
|
117 val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] |
|
118 "[| wf(r); trans(r); \ |
|
119 \ is_recfun r a H f; is_recfun r b H g; <b,a>:r |] ==> \ |
|
120 \ cut f r b = g"; |
|
121 val gundef = recgb RS is_recfun_undef |
|
122 and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); |
|
123 by (cut_facts_tac prems 1); |
|
124 by (rtac ext 1); |
|
125 by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg] |
|
126 setloop (split_tac [expand_if])) 1); |
|
127 qed "is_recfun_cut"; |
|
128 |
|
129 (*** Main Existence Lemma -- Basic Properties of the_recfun ***) |
|
130 |
|
131 val prems = goalw WF.thy [the_recfun_def] |
|
132 "is_recfun r a H f ==> is_recfun r a H (the_recfun r a H)"; |
|
133 by (res_inst_tac [("P", "is_recfun r a H")] selectI 1); |
|
134 by (resolve_tac prems 1); |
|
135 qed "is_the_recfun"; |
|
136 |
|
137 val prems = goal WF.thy |
|
138 "[| wf(r); trans(r) |] ==> is_recfun r a H (the_recfun r a H)"; |
|
139 by (cut_facts_tac prems 1); |
|
140 by (wf_ind_tac "a" prems 1); |
|
141 by (res_inst_tac [("f", "cut (%y. wftrec r y H) r a1")] is_the_recfun 1); |
|
142 by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
143 by (rtac (cut_cut_eq RS ssubst) 1); |
|
144 (*Applying the substitution: must keep the quantified assumption!!*) |
|
145 by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac, |
|
146 etac (mp RS ssubst), atac]); |
|
147 by (fold_tac [is_recfun_def]); |
|
148 by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1); |
|
149 qed "unfold_the_recfun"; |
|
150 |
|
151 |
|
152 (*Beware incompleteness of unification!*) |
|
153 val prems = goal WF.thy |
|
154 "[| wf(r); trans(r); <c,a>:r; <c,b>:r |] \ |
|
155 \ ==> the_recfun r a H c = the_recfun r b H c"; |
|
156 by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1)); |
|
157 qed "the_recfun_equal"; |
|
158 |
|
159 val prems = goal WF.thy |
|
160 "[| wf(r); trans(r); <b,a>:r |] \ |
|
161 \ ==> cut (the_recfun r a H) r b = the_recfun r b H"; |
|
162 by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1)); |
|
163 qed "the_recfun_cut"; |
|
164 |
|
165 (*** Unfolding wftrec ***) |
|
166 |
|
167 goalw WF.thy [wftrec_def] |
|
168 "!!r. [| wf(r); trans(r) |] ==> \ |
|
169 \ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; |
|
170 by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), |
|
171 REPEAT o atac, rtac H_cong1]); |
|
172 by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1); |
|
173 qed "wftrec"; |
|
174 |
|
175 (*Unused but perhaps interesting*) |
|
176 val prems = goal WF.thy |
|
177 "[| wf(r); trans(r); !!f x. H x (cut f r x) = H x f |] ==> \ |
|
178 \ wftrec r a H = H a (%x.wftrec r x H)"; |
|
179 by (rtac (wftrec RS trans) 1); |
|
180 by (REPEAT (resolve_tac prems 1)); |
|
181 qed "wftrec2"; |
|
182 |
|
183 (** Removal of the premise trans(r) **) |
|
184 |
|
185 goalw WF.thy [wfrec_def] |
|
186 "!!r. wf(r) ==> wfrec r a H = H a (cut (%x.wfrec r x H) r a)"; |
|
187 by (etac (wf_trancl RS wftrec RS ssubst) 1); |
|
188 by (rtac trans_trancl 1); |
|
189 by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) |
|
190 by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1); |
|
191 qed "wfrec"; |
|
192 |
|
193 (*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
194 val rew::prems = goal WF.thy |
|
195 "[| !!x. f(x)==wfrec r x H; wf(r) |] ==> f(a) = H a (cut (%x.f(x)) r a)"; |
|
196 by (rewtac rew); |
|
197 by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
198 qed "def_wfrec"; |