author | wenzelm |
Mon, 17 Feb 1997 17:23:14 +0100 | |
changeset 2652 | 024654b75919 |
parent 2637 | e9b203f854ae |
child 2935 | 998cb95fdd43 |
permissions | -rw-r--r-- |
1475 | 1 |
(* Title: HOL/wf.ML |
923 | 2 |
ID: $Id$ |
1475 | 3 |
Author: Tobias Nipkow, with minor changes by Konrad Slind |
4 |
Copyright 1992 University of Cambridge/1995 TU Munich |
|
923 | 5 |
|
1475 | 6 |
For WF.thy. Wellfoundedness, induction, and recursion |
923 | 7 |
*) |
8 |
||
9 |
open WF; |
|
10 |
||
950 | 11 |
val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
923 | 12 |
val H_cong1 = refl RS H_cong; |
13 |
||
14 |
(*Restriction to domain A. If r is well-founded over A then wf(r)*) |
|
15 |
val [prem1,prem2] = goalw WF.thy [wf_def] |
|
1642 | 16 |
"[| r <= A Times A; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
17 |
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
923 | 18 |
\ ==> wf(r)"; |
19 |
by (strip_tac 1); |
|
20 |
by (rtac allE 1); |
|
21 |
by (assume_tac 1); |
|
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1771
diff
changeset
|
22 |
by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); |
923 | 23 |
qed "wfI"; |
24 |
||
25 |
val major::prems = goalw WF.thy [wf_def] |
|
26 |
"[| wf(r); \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
27 |
\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ |
923 | 28 |
\ |] ==> P(a)"; |
29 |
by (rtac (major RS spec RS mp RS spec) 1); |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
30 |
by (fast_tac (!claset addEs prems) 1); |
923 | 31 |
qed "wf_induct"; |
32 |
||
33 |
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
34 |
fun wf_ind_tac a prems i = |
|
35 |
EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
1465 | 36 |
rename_last_tac a ["1"] (i+1), |
37 |
ares_tac prems i]; |
|
923 | 38 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
39 |
val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
40 |
by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
41 |
by (fast_tac (!claset addIs prems) 1); |
923 | 42 |
by (wf_ind_tac "a" prems 1); |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
43 |
by (Fast_tac 1); |
923 | 44 |
qed "wf_asym"; |
45 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
46 |
val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; |
923 | 47 |
by (rtac wf_asym 1); |
48 |
by (REPEAT (resolve_tac prems 1)); |
|
1618 | 49 |
qed "wf_irrefl"; |
923 | 50 |
|
1475 | 51 |
(*transitive closure of a wf relation is wf! *) |
923 | 52 |
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
53 |
by (rewtac wf_def); |
|
54 |
by (strip_tac 1); |
|
55 |
(*must retain the universal formula for later use!*) |
|
56 |
by (rtac allE 1 THEN assume_tac 1); |
|
57 |
by (etac mp 1); |
|
58 |
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); |
|
59 |
by (rtac (impI RS allI) 1); |
|
60 |
by (etac tranclE 1); |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
61 |
by (Fast_tac 1); |
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
62 |
by (Fast_tac 1); |
923 | 63 |
qed "wf_trancl"; |
64 |
||
65 |
||
66 |
(** cut **) |
|
67 |
||
68 |
(*This rewrite rule works upon formulae; thus it requires explicit use of |
|
69 |
H_cong to expose the equality*) |
|
70 |
goalw WF.thy [cut_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
71 |
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; |
1552 | 72 |
by (simp_tac (HOL_ss addsimps [expand_fun_eq] |
1475 | 73 |
setloop (split_tac [expand_if])) 1); |
74 |
qed "cuts_eq"; |
|
923 | 75 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
76 |
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; |
1552 | 77 |
by (asm_simp_tac HOL_ss 1); |
923 | 78 |
qed "cut_apply"; |
79 |
||
80 |
(*** is_recfun ***) |
|
81 |
||
82 |
goalw WF.thy [is_recfun_def,cut_def] |
|
1475 | 83 |
"!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = (@z.True)"; |
923 | 84 |
by (etac ssubst 1); |
1552 | 85 |
by (asm_simp_tac HOL_ss 1); |
923 | 86 |
qed "is_recfun_undef"; |
87 |
||
88 |
(*** NOTE! some simplifications need a different finish_tac!! ***) |
|
89 |
fun indhyp_tac hyps = |
|
90 |
(cut_facts_tac hyps THEN' |
|
91 |
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
|
1465 | 92 |
eresolve_tac [transD, mp, allE])); |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2031
diff
changeset
|
93 |
val wf_super_ss = HOL_ss addSolver indhyp_tac; |
923 | 94 |
|
95 |
val prems = goalw WF.thy [is_recfun_def,cut_def] |
|
1475 | 96 |
"[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
97 |
\ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
923 | 98 |
by (cut_facts_tac prems 1); |
99 |
by (etac wf_induct 1); |
|
100 |
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
101 |
by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset
|
102 |
qed_spec_mp "is_recfun_equal"; |
923 | 103 |
|
104 |
||
105 |
val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] |
|
106 |
"[| wf(r); trans(r); \ |
|
1475 | 107 |
\ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \ |
923 | 108 |
\ cut f r b = g"; |
109 |
val gundef = recgb RS is_recfun_undef |
|
110 |
and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); |
|
111 |
by (cut_facts_tac prems 1); |
|
112 |
by (rtac ext 1); |
|
113 |
by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg] |
|
114 |
setloop (split_tac [expand_if])) 1); |
|
115 |
qed "is_recfun_cut"; |
|
116 |
||
117 |
(*** Main Existence Lemma -- Basic Properties of the_recfun ***) |
|
118 |
||
119 |
val prems = goalw WF.thy [the_recfun_def] |
|
1475 | 120 |
"is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; |
121 |
by (res_inst_tac [("P", "is_recfun r H a")] selectI 1); |
|
923 | 122 |
by (resolve_tac prems 1); |
123 |
qed "is_the_recfun"; |
|
124 |
||
125 |
val prems = goal WF.thy |
|
1475 | 126 |
"[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; |
127 |
by (cut_facts_tac prems 1); |
|
128 |
by (wf_ind_tac "a" prems 1); |
|
129 |
by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] |
|
130 |
is_the_recfun 1); |
|
1552 | 131 |
by (rewtac is_recfun_def); |
2031 | 132 |
by (stac cuts_eq 1); |
1475 | 133 |
by (rtac allI 1); |
134 |
by (rtac impI 1); |
|
135 |
by (res_inst_tac [("f1","H"),("x","y")](arg_cong RS fun_cong) 1); |
|
136 |
by (subgoal_tac |
|
137 |
"the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); |
|
138 |
by (etac allE 2); |
|
139 |
by (dtac impE 2); |
|
140 |
by (atac 2); |
|
141 |
by (atac 3); |
|
142 |
by (atac 2); |
|
143 |
by (etac ssubst 1); |
|
144 |
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
145 |
by (rtac allI 1); |
|
146 |
by (rtac impI 1); |
|
147 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
148 |
by (res_inst_tac [("f1","H"),("x","ya")](arg_cong RS fun_cong) 1); |
|
149 |
by (fold_tac [is_recfun_def]); |
|
150 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
923 | 151 |
qed "unfold_the_recfun"; |
152 |
||
1475 | 153 |
val unwind1_the_recfun = rewrite_rule[is_recfun_def] unfold_the_recfun; |
923 | 154 |
|
1475 | 155 |
(*--------------Old proof----------------------------------------------------- |
923 | 156 |
val prems = goal WF.thy |
1475 | 157 |
"[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; |
158 |
by (cut_facts_tac prems 1); |
|
159 |
by (wf_ind_tac "a" prems 1); |
|
160 |
by (res_inst_tac [("f", "cut (%y. wftrec r H y) r a1")] is_the_recfun 1); |
|
161 |
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
2031 | 162 |
by (stac cuts_eq 1); |
1475 | 163 |
(*Applying the substitution: must keep the quantified assumption!!*) |
164 |
by (EVERY1 [strip_tac, rtac H_cong1, rtac allE, atac, |
|
165 |
etac (mp RS ssubst), atac]); |
|
166 |
by (fold_tac [is_recfun_def]); |
|
167 |
by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cuts_eq]) 1); |
|
168 |
qed "unfold_the_recfun"; |
|
169 |
---------------------------------------------------------------------------*) |
|
923 | 170 |
|
171 |
(** Removal of the premise trans(r) **) |
|
1475 | 172 |
val th = rewrite_rule[is_recfun_def] |
173 |
(trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); |
|
923 | 174 |
|
175 |
goalw WF.thy [wfrec_def] |
|
1475 | 176 |
"!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; |
177 |
by (rtac H_cong 1); |
|
178 |
by (rtac refl 2); |
|
179 |
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
180 |
by (rtac allI 1); |
|
181 |
by (rtac impI 1); |
|
182 |
by (simp_tac(HOL_ss addsimps [wfrec_def]) 1); |
|
183 |
by (res_inst_tac [("a1","a")] (th RS ssubst) 1); |
|
184 |
by (atac 1); |
|
185 |
by (forward_tac[wf_trancl] 1); |
|
186 |
by (forward_tac[r_into_trancl] 1); |
|
187 |
by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); |
|
188 |
by (rtac H_cong 1); (*expose the equality of cuts*) |
|
189 |
by (rtac refl 2); |
|
190 |
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); |
|
191 |
by (strip_tac 1); |
|
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset
|
192 |
by (res_inst_tac [("r","r^+")] is_recfun_equal 1); |
1475 | 193 |
by (atac 1); |
194 |
by (rtac trans_trancl 1); |
|
195 |
by (rtac unfold_the_recfun 1); |
|
196 |
by (atac 1); |
|
197 |
by (rtac trans_trancl 1); |
|
198 |
by (rtac unfold_the_recfun 1); |
|
199 |
by (atac 1); |
|
200 |
by (rtac trans_trancl 1); |
|
201 |
by (rtac transD 1); |
|
202 |
by (rtac trans_trancl 1); |
|
203 |
by (forw_inst_tac [("a","ya")] r_into_trancl 1); |
|
204 |
by (atac 1); |
|
205 |
by (atac 1); |
|
206 |
by (forw_inst_tac [("a","ya")] r_into_trancl 1); |
|
207 |
by (atac 1); |
|
208 |
qed "wfrec"; |
|
209 |
||
210 |
(*--------------Old proof----------------------------------------------------- |
|
211 |
goalw WF.thy [wfrec_def] |
|
212 |
"!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; |
|
923 | 213 |
by (etac (wf_trancl RS wftrec RS ssubst) 1); |
214 |
by (rtac trans_trancl 1); |
|
215 |
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*) |
|
1475 | 216 |
by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); |
923 | 217 |
qed "wfrec"; |
1475 | 218 |
---------------------------------------------------------------------------*) |
923 | 219 |
|
1475 | 220 |
(*--------------------------------------------------------------------------- |
221 |
* This form avoids giant explosions in proofs. NOTE USE OF == |
|
222 |
*---------------------------------------------------------------------------*) |
|
923 | 223 |
val rew::prems = goal WF.thy |
1475 | 224 |
"[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"; |
923 | 225 |
by (rewtac rew); |
226 |
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
227 |
qed "def_wfrec"; |
|
1475 | 228 |