|
1 (* Title: CCL/wf |
|
2 ID: $Id$ |
|
3 |
|
4 For wf.thy. |
|
5 |
|
6 Based on |
|
7 Titles: ZF/wf.ML and HOL/ex/lex-prod |
|
8 Authors: Lawrence C Paulson and Tobias Nipkow |
|
9 Copyright 1992 University of Cambridge |
|
10 |
|
11 *) |
|
12 |
|
13 open Wfd; |
|
14 |
|
15 (***********) |
|
16 |
|
17 val wfd_congs = mk_congs Wfd.thy ["Wfd","wf","op **","wmap","ListPR"]; |
|
18 |
|
19 (***********) |
|
20 |
|
21 val [major,prem] = goalw Wfd.thy [Wfd_def] |
|
22 "[| Wfd(R); \ |
|
23 \ !!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x) |] ==> \ |
|
24 \ P(a)"; |
|
25 by (rtac (major RS spec RS mp RS spec RS CollectD) 1); |
|
26 by (fast_tac (set_cs addSIs [prem RS CollectI]) 1); |
|
27 val wfd_induct = result(); |
|
28 |
|
29 val [p1,p2,p3] = goal Wfd.thy |
|
30 "[| !!x y.<x,y> : R ==> Q(x); \ |
|
31 \ ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \ |
|
32 \ !!x.Q(x) ==> x:P |] ==> a:P"; |
|
33 br (p2 RS spec RS mp) 1; |
|
34 by (fast_tac (set_cs addSIs [p1 RS p3]) 1); |
|
35 val wfd_strengthen_lemma = result(); |
|
36 |
|
37 fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN |
|
38 assume_tac (i+1); |
|
39 |
|
40 val wfd::prems = goal Wfd.thy "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"; |
|
41 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1); |
|
42 by (fast_tac (FOL_cs addIs prems) 1); |
|
43 br (wfd RS wfd_induct) 1; |
|
44 by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); |
|
45 val wf_anti_sym = result(); |
|
46 |
|
47 val prems = goal Wfd.thy "[| Wfd(r); <a,a>: r |] ==> P"; |
|
48 by (rtac wf_anti_sym 1); |
|
49 by (REPEAT (resolve_tac prems 1)); |
|
50 val wf_anti_refl = result(); |
|
51 |
|
52 (*** Irreflexive transitive closure ***) |
|
53 |
|
54 val [prem] = goal Wfd.thy "Wfd(R) ==> Wfd(R^+)"; |
|
55 by (rewtac Wfd_def); |
|
56 by (REPEAT (ares_tac [allI,ballI,impI] 1)); |
|
57 (*must retain the universal formula for later use!*) |
|
58 by (rtac allE 1 THEN assume_tac 1); |
|
59 by (etac mp 1); |
|
60 br (prem RS wfd_induct) 1; |
|
61 by (rtac (impI RS allI) 1); |
|
62 by (etac tranclE 1); |
|
63 by (fast_tac ccl_cs 1); |
|
64 be (spec RS mp RS spec RS mp) 1; |
|
65 by (REPEAT (atac 1)); |
|
66 val trancl_wf = result(); |
|
67 |
|
68 (*** Lexicographic Ordering ***) |
|
69 |
|
70 goalw Wfd.thy [lex_def] |
|
71 "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))"; |
|
72 by (fast_tac ccl_cs 1); |
|
73 val lexXH = result(); |
|
74 |
|
75 val prems = goal Wfd.thy |
|
76 "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb"; |
|
77 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); |
|
78 val lexI1 = result(); |
|
79 |
|
80 val prems = goal Wfd.thy |
|
81 "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb"; |
|
82 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); |
|
83 val lexI2 = result(); |
|
84 |
|
85 val major::prems = goal Wfd.thy |
|
86 "[| p : ra**rb; \ |
|
87 \ !!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R; \ |
|
88 \ !!a b b'.[| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> R |] ==> \ |
|
89 \ R"; |
|
90 br (major RS (lexXH RS iffD1) RS exE) 1; |
|
91 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); |
|
92 by (ALLGOALS (fast_tac ccl_cs)); |
|
93 val lexE = result(); |
|
94 |
|
95 val [major,minor] = goal Wfd.thy |
|
96 "[| p : r**s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P"; |
|
97 br (major RS lexE) 1; |
|
98 by (ALLGOALS (fast_tac (set_cs addSEs [minor]))); |
|
99 val lex_pair = result(); |
|
100 |
|
101 val [wfa,wfb] = goal Wfd.thy |
|
102 "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)"; |
|
103 bw Wfd_def; |
|
104 by (safe_tac ccl_cs); |
|
105 by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1); |
|
106 by (fast_tac (term_cs addSEs [lex_pair]) 1); |
|
107 by (subgoal_tac "ALL a b.<a,b>:P" 1); |
|
108 by (fast_tac ccl_cs 1); |
|
109 br (wfa RS wfd_induct RS allI) 1; |
|
110 br (wfb RS wfd_induct RS allI) 1;back(); |
|
111 by (fast_tac (type_cs addSEs [lexE]) 1); |
|
112 val lex_wf = result(); |
|
113 |
|
114 (*** Mapping ***) |
|
115 |
|
116 goalw Wfd.thy [wmap_def] |
|
117 "p : wmap(f,r) <-> (EX x y. p=<x,y> & <f(x),f(y)> : r)"; |
|
118 by (fast_tac ccl_cs 1); |
|
119 val wmapXH = result(); |
|
120 |
|
121 val prems = goal Wfd.thy |
|
122 "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)"; |
|
123 by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1); |
|
124 val wmapI = result(); |
|
125 |
|
126 val major::prems = goal Wfd.thy |
|
127 "[| p : wmap(f,r); !!a b.[| <f(a),f(b)> : r; p=<a,b> |] ==> R |] ==> R"; |
|
128 br (major RS (wmapXH RS iffD1) RS exE) 1; |
|
129 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); |
|
130 by (ALLGOALS (fast_tac ccl_cs)); |
|
131 val wmapE = result(); |
|
132 |
|
133 val [wf] = goal Wfd.thy |
|
134 "Wfd(r) ==> Wfd(wmap(f,r))"; |
|
135 bw Wfd_def; |
|
136 by (safe_tac ccl_cs); |
|
137 by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1); |
|
138 by (fast_tac ccl_cs 1); |
|
139 br (wf RS wfd_induct RS allI) 1; |
|
140 by (safe_tac ccl_cs); |
|
141 be (spec RS mp) 1; |
|
142 by (safe_tac (ccl_cs addSEs [wmapE])); |
|
143 be (spec RS mp RS spec RS mp) 1; |
|
144 ba 1; |
|
145 br refl 1; |
|
146 val wmap_wf = result(); |
|
147 |
|
148 (* Projections *) |
|
149 |
|
150 val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)"; |
|
151 br wmapI 1; |
|
152 by (SIMP_TAC (term_ss addrews prems) 1); |
|
153 val wfstI = result(); |
|
154 |
|
155 val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)"; |
|
156 br wmapI 1; |
|
157 by (SIMP_TAC (term_ss addrews prems) 1); |
|
158 val wsndI = result(); |
|
159 |
|
160 val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)"; |
|
161 br wmapI 1; |
|
162 by (SIMP_TAC (term_ss addrews prems) 1); |
|
163 val wthdI = result(); |
|
164 |
|
165 (*** Ground well-founded relations ***) |
|
166 |
|
167 val prems = goalw Wfd.thy [wf_def] |
|
168 "[| Wfd(r); a : r |] ==> a : wf(r)"; |
|
169 by (fast_tac (set_cs addSIs prems) 1); |
|
170 val wfI = result(); |
|
171 |
|
172 val prems = goalw Wfd.thy [Wfd_def] "Wfd({})"; |
|
173 by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1); |
|
174 val Empty_wf = result(); |
|
175 |
|
176 val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))"; |
|
177 by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1); |
|
178 by (ALLGOALS (ASM_SIMP_TAC (CCL_ss addcongs wfd_congs))); |
|
179 br Empty_wf 1; |
|
180 val wf_wf = result(); |
|
181 |
|
182 goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)"; |
|
183 by (fast_tac set_cs 1); |
|
184 val NatPRXH = result(); |
|
185 |
|
186 goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h.t>)"; |
|
187 by (fast_tac set_cs 1); |
|
188 val ListPRXH = result(); |
|
189 |
|
190 val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2)); |
|
191 val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2))); |
|
192 |
|
193 goalw Wfd.thy [Wfd_def] "Wfd(NatPR)"; |
|
194 by (safe_tac set_cs); |
|
195 by (wfd_strengthen_tac "%x.x:Nat" 1); |
|
196 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1); |
|
197 be Nat_ind 1; |
|
198 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH]))); |
|
199 val NatPR_wf = result(); |
|
200 |
|
201 goalw Wfd.thy [Wfd_def] "Wfd(ListPR(A))"; |
|
202 by (safe_tac set_cs); |
|
203 by (wfd_strengthen_tac "%x.x:List(A)" 1); |
|
204 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1); |
|
205 be List_ind 1; |
|
206 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH]))); |
|
207 val ListPR_wf = result(); |
|
208 |