|
1 (* Title: HOL/WF.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind |
|
4 Copyright 1996 TU Munich |
|
5 |
|
6 For WF1.thy. |
|
7 *) |
|
8 |
|
9 open WF1; |
|
10 |
|
11 (* TFL variants *) |
|
12 goal WF.thy |
|
13 "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))"; |
|
14 by (strip_tac 1); |
|
15 by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); |
|
16 by (assume_tac 1); |
|
17 by (fast_tac HOL_cs 1); |
|
18 qed"tfl_wf_induct"; |
|
19 |
|
20 goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)"; |
|
21 by (strip_tac 1); |
|
22 by (rtac cut_apply 1); |
|
23 by (assume_tac 1); |
|
24 qed"tfl_cut_apply"; |
|
25 |
|
26 goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)"; |
|
27 by (strip_tac 1); |
|
28 by (res_inst_tac [("r","R"), ("H","M"), |
|
29 ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1); |
|
30 by (assume_tac 1); |
|
31 by (assume_tac 1); |
|
32 qed "tfl_wfrec"; |
|
33 |
|
34 (*---------------------------------------------------------------------------- |
|
35 * Proof that the inverse image into a wellfounded relation is wellfounded. |
|
36 * The proof is relatively sloppy - I map to another version of |
|
37 * wellfoundedness (every n.e. set has an R-minimal element) and transport |
|
38 * the proof for that formulation over. I also didn't remember the existence |
|
39 * of "set_cs" so no doubt the proof can be dramatically shortened! |
|
40 *---------------------------------------------------------------------------*) |
|
41 goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))"; |
|
42 by (fast_tac HOL_cs 1); |
|
43 val th1 = result(); |
|
44 |
|
45 goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))"; |
|
46 by (fast_tac HOL_cs 1); |
|
47 val th2 = result(); |
|
48 |
|
49 goal HOL.thy "(~(x-->y)) = (x & (~ y))"; |
|
50 by (fast_tac HOL_cs 1); |
|
51 val th3 = result(); |
|
52 |
|
53 goal HOL.thy "((~ x) | y) = (x --> y)"; |
|
54 by (fast_tac HOL_cs 1); |
|
55 val th4 = result(); |
|
56 |
|
57 goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))"; |
|
58 by (fast_tac HOL_cs 1); |
|
59 val th5 = result(); |
|
60 |
|
61 goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))"; |
|
62 by (fast_tac HOL_cs 1); |
|
63 val th6 = result(); |
|
64 |
|
65 goal HOL.thy "(~(~x)) = x"; |
|
66 by (fast_tac HOL_cs 1); |
|
67 val th7 = result(); |
|
68 |
|
69 (* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *) |
|
70 val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7]; |
|
71 |
|
72 (* The name "contrapos" is already taken. *) |
|
73 goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))"; |
|
74 by (fast_tac HOL_cs 1); |
|
75 val ol_contrapos = result(); |
|
76 |
|
77 (* Maps to another version of wellfoundedness *) |
|
78 val [p1] = goalw WF.thy [wf_def] |
|
79 "wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))"; |
|
80 by (rtac allI 1); |
|
81 by (rtac (ol_contrapos RS ssubst) 1); |
|
82 by (rewrite_tac NNF_rews); |
|
83 by (rtac impI 1); |
|
84 by (rtac ((p1 RS spec) RS mp) 1); |
|
85 by (fast_tac HOL_cs 1); |
|
86 val wf_minimal = result(); |
|
87 |
|
88 goalw WF.thy [wf_def] |
|
89 "(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R"; |
|
90 by (rtac impI 1); |
|
91 by (rtac allI 1); |
|
92 by (rtac (ol_contrapos RS ssubst) 1); |
|
93 by (rewrite_tac NNF_rews); |
|
94 by (rtac impI 1); |
|
95 by (etac allE 1); |
|
96 by (dtac mp 1); |
|
97 by (assume_tac 1); |
|
98 by (fast_tac HOL_cs 1); |
|
99 val minimal_wf = result(); |
|
100 |
|
101 val wf_eq_minimal = |
|
102 standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym); |
|
103 |
|
104 goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection] |
|
105 "wf(R) --> wf(inv_image R (f::'a=>'b))"; |
|
106 by (strip_tac 1); |
|
107 by (etac exE 1); |
|
108 by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1); |
|
109 by (rtac exI 2); |
|
110 by (rtac exI 2); |
|
111 by (rtac conjI 2); |
|
112 by (assume_tac 2); |
|
113 by (rtac refl 2); |
|
114 |
|
115 by (etac allE 1); |
|
116 by (dtac mp 1); |
|
117 by (assume_tac 1); |
|
118 by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \ |
|
119 \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1); |
|
120 by (etac thin_rl 1); |
|
121 by (etac thin_rl 1); |
|
122 by (rewrite_tac NNF_rews); |
|
123 by (rtac impI 1); |
|
124 by (etac exE 1); |
|
125 by (etac conjE 1); |
|
126 by (etac exE 1); |
|
127 by (rtac exI 1); |
|
128 by (etac conjE 1); |
|
129 by (rtac conjI 1); |
|
130 by (assume_tac 1); |
|
131 by (hyp_subst_tac 1); |
|
132 by (rtac allI 1); |
|
133 by (rtac impI 1); |
|
134 by (etac CollectE 1); |
|
135 by (etac allE 1); |
|
136 by (dtac mp 1); |
|
137 by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]); |
|
138 by (assume_tac 1); |
|
139 by (fast_tac HOL_cs 1); |
|
140 val wf_inv_image = result() RS mp; |
|
141 |
|
142 (* from Nat.ML *) |
|
143 goalw WF1.thy [wf_def] "wf(pred_nat)"; |
|
144 by (strip_tac 1); |
|
145 by (nat_ind_tac "x" 1); |
|
146 by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, |
|
147 make_elim Suc_inject]) 2); |
|
148 by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1); |
|
149 val wf_pred_nat = result(); |
|
150 |
|
151 goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)"; |
|
152 by (strip_tac 1); |
|
153 by (List.list.induct_tac "x" 1); |
|
154 by (etac allE 1); |
|
155 by (etac impE 1); |
|
156 by (assume_tac 2); |
|
157 by (strip_tac 1); |
|
158 by (etac CollectE 1); |
|
159 by (asm_full_simp_tac (!simpset) 1); |
|
160 |
|
161 by (etac allE 1); |
|
162 by (etac impE 1); |
|
163 by (assume_tac 2); |
|
164 by (strip_tac 1); |
|
165 by (etac CollectE 1); |
|
166 by (etac exE 1); |
|
167 by (asm_full_simp_tac (!simpset) 1); |
|
168 by (etac conjE 1); |
|
169 by (hyp_subst_tac 1); |
|
170 by (assume_tac 1); |
|
171 qed "wf_pred_list"; |
|
172 |
|
173 (*---------------------------------------------------------------------------- |
|
174 * All measures are wellfounded. |
|
175 *---------------------------------------------------------------------------*) |
|
176 |
|
177 goalw WF1.thy [measure_def] "wf (measure f)"; |
|
178 by (rtac wf_inv_image 1); |
|
179 by (rtac wf_trancl 1); |
|
180 by (rtac wf_pred_nat 1); |
|
181 qed "wf_measure"; |
|
182 |
|
183 (*---------------------------------------------------------------------------- |
|
184 * Wellfoundedness of lexicographic combinations |
|
185 *---------------------------------------------------------------------------*) |
|
186 |
|
187 val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)"; |
|
188 by (cut_facts_tac prems 1); |
|
189 by (rtac allI 1); |
|
190 by (rtac (surjective_pairing RS ssubst) 1); |
|
191 by (fast_tac HOL_cs 1); |
|
192 qed "split_all_pair"; |
|
193 |
|
194 val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def] |
|
195 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; |
|
196 by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
197 by (rtac (wfa RS spec RS mp) 1); |
|
198 by (EVERY1 [rtac allI,rtac impI]); |
|
199 by (rtac (wfb RS spec RS mp) 1); |
|
200 by (fast_tac (set_cs addSEs [Pair_inject]) 1); |
|
201 qed "wf_lex_prod"; |
|
202 |
|
203 (*---------------------------------------------------------------------------- |
|
204 * Wellfoundedness of relational product |
|
205 *---------------------------------------------------------------------------*) |
|
206 val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def] |
|
207 "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)"; |
|
208 by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); |
|
209 by (rtac (wfa RS spec RS mp) 1); |
|
210 by (EVERY1 [rtac allI,rtac impI]); |
|
211 by (rtac (wfb RS spec RS mp) 1); |
|
212 by (fast_tac (set_cs addSEs [Pair_inject]) 1); |
|
213 qed "wf_rel_prod"; |
|
214 |
|
215 |
|
216 (*--------------------------------------------------------------------------- |
|
217 * Wellfoundedness of subsets |
|
218 *---------------------------------------------------------------------------*) |
|
219 |
|
220 goalw WF1.thy [wf_eq_minimal RS eq_reflection] |
|
221 "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)"; |
|
222 by (fast_tac set_cs 1); |
|
223 qed "wf_subset"; |
|
224 |
|
225 (*--------------------------------------------------------------------------- |
|
226 * Wellfoundedness of the empty relation. |
|
227 *---------------------------------------------------------------------------*) |
|
228 |
|
229 goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def] |
|
230 "wf(emptyr)"; |
|
231 by (fast_tac set_cs 1); |
|
232 qed "wf_emptyr"; |