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