author | wenzelm |
Wed, 30 Dec 2015 21:57:52 +0100 | |
changeset 62002 | f1599e98c4d0 |
parent 60770 | 240563fbf41d |
child 62020 | 5d208fd2507d |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/Type.thy |
0 | 2 |
Author: Martin Coen |
3 |
Copyright 1993 University of Cambridge |
|
4 |
*) |
|
5 |
||
60770 | 6 |
section \<open>Types in CCL are defined as sets of terms\<close> |
17456 | 7 |
|
8 |
theory Type |
|
9 |
imports Term |
|
10 |
begin |
|
0 | 11 |
|
12 |
consts |
|
13 |
||
58977 | 14 |
Subtype :: "['a set, 'a \<Rightarrow> o] \<Rightarrow> 'a set" |
0 | 15 |
Bool :: "i set" |
16 |
Unit :: "i set" |
|
58977 | 17 |
Plus :: "[i set, i set] \<Rightarrow> i set" (infixr "+" 55) |
18 |
Pi :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set" |
|
19 |
Sigma :: "[i set, i \<Rightarrow> i set] \<Rightarrow> i set" |
|
0 | 20 |
Nat :: "i set" |
58977 | 21 |
List :: "i set \<Rightarrow> i set" |
22 |
Lists :: "i set \<Rightarrow> i set" |
|
23 |
ILists :: "i set \<Rightarrow> i set" |
|
24 |
TAll :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TALL " 55) |
|
25 |
TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder "TEX " 55) |
|
26 |
Lift :: "i set \<Rightarrow> i set" ("(3[_])") |
|
0 | 27 |
|
58977 | 28 |
SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set" |
0 | 29 |
|
14765 | 30 |
syntax |
58977 | 31 |
"_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3PROD _:_./ _)" |
1474 | 32 |
[0,0,60] 60) |
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset
|
33 |
|
58977 | 34 |
"_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" ("(3SUM _:_./ _)" |
1474 | 35 |
[0,0,60] 60) |
17456 | 36 |
|
58977 | 37 |
"_arrow" :: "[i set, i set] \<Rightarrow> i set" ("(_ ->/ _)" [54, 53] 53) |
38 |
"_star" :: "[i set, i set] \<Rightarrow> i set" ("(_ */ _)" [56, 55] 55) |
|
39 |
"_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" ("(1{_: _ ./ _})") |
|
0 | 40 |
|
41 |
translations |
|
58977 | 42 |
"PROD x:A. B" => "CONST Pi(A, \<lambda>x. B)" |
43 |
"A -> B" => "CONST Pi(A, \<lambda>_. B)" |
|
44 |
"SUM x:A. B" => "CONST Sigma(A, \<lambda>x. B)" |
|
45 |
"A * B" => "CONST Sigma(A, \<lambda>_. B)" |
|
46 |
"{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)" |
|
0 | 47 |
|
60770 | 48 |
print_translation \<open> |
42284 | 49 |
[(@{const_syntax Pi}, |
52143 | 50 |
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
42284 | 51 |
(@{const_syntax Sigma}, |
52143 | 52 |
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
60770 | 53 |
\<close> |
0 | 54 |
|
42156 | 55 |
defs |
58977 | 56 |
Subtype_def: "{x:A. P(x)} == {x. x:A \<and> P(x)}" |
17456 | 57 |
Unit_def: "Unit == {x. x=one}" |
58 |
Bool_def: "Bool == {x. x=true | x=false}" |
|
59 |
Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
|
58977 | 60 |
Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) \<and> (ALL x:A. b(x):B(x))}" |
17456 | 61 |
Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" |
58977 | 62 |
Nat_def: "Nat == lfp(\<lambda>X. Unit + X)" |
63 |
List_def: "List(A) == lfp(\<lambda>X. Unit + A*X)" |
|
0 | 64 |
|
58977 | 65 |
Lists_def: "Lists(A) == gfp(\<lambda>X. Unit + A*X)" |
66 |
ILists_def: "ILists(A) == gfp(\<lambda>X.{} + A*X)" |
|
0 | 67 |
|
17456 | 68 |
Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" |
69 |
Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" |
|
70 |
Lift_def: "[A] == A Un {bot}" |
|
0 | 71 |
|
58977 | 72 |
SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> \<and> A=B(x,y)})" |
17456 | 73 |
|
20140 | 74 |
|
75 |
lemmas simp_type_defs = |
|
76 |
Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def |
|
77 |
and ind_type_defs = Nat_def List_def |
|
78 |
and simp_data_defs = one_def inl_def inr_def |
|
79 |
and ind_data_defs = zero_def succ_def nil_def cons_def |
|
80 |
||
58977 | 81 |
lemma subsetXH: "A <= B \<longleftrightarrow> (ALL x. x:A \<longrightarrow> x:B)" |
20140 | 82 |
by blast |
83 |
||
84 |
||
60770 | 85 |
subsection \<open>Exhaustion Rules\<close> |
20140 | 86 |
|
58977 | 87 |
lemma EmptyXH: "\<And>a. a : {} \<longleftrightarrow> False" |
88 |
and SubtypeXH: "\<And>a A P. a : {x:A. P(x)} \<longleftrightarrow> (a:A \<and> P(a))" |
|
89 |
and UnitXH: "\<And>a. a : Unit \<longleftrightarrow> a=one" |
|
90 |
and BoolXH: "\<And>a. a : Bool \<longleftrightarrow> a=true | a=false" |
|
91 |
and PlusXH: "\<And>a A B. a : A+B \<longleftrightarrow> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))" |
|
92 |
and PiXH: "\<And>a A B. a : PROD x:A. B(x) \<longleftrightarrow> (EX b. a=lam x. b(x) \<and> (ALL x:A. b(x):B(x)))" |
|
93 |
and SgXH: "\<And>a A B. a : SUM x:A. B(x) \<longleftrightarrow> (EX x:A. EX y:B(x).a=<x,y>)" |
|
20140 | 94 |
unfolding simp_type_defs by blast+ |
95 |
||
96 |
lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH |
|
97 |
||
58977 | 98 |
lemma LiftXH: "a : [A] \<longleftrightarrow> (a=bot | a:A)" |
99 |
and TallXH: "a : TALL X. B(X) \<longleftrightarrow> (ALL X. a:B(X))" |
|
100 |
and TexXH: "a : TEX X. B(X) \<longleftrightarrow> (EX X. a:B(X))" |
|
20140 | 101 |
unfolding simp_type_defs by blast+ |
102 |
||
60770 | 103 |
ML \<open>ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs})\<close> |
20140 | 104 |
|
105 |
||
60770 | 106 |
subsection \<open>Canonical Type Rules\<close> |
20140 | 107 |
|
108 |
lemma oneT: "one : Unit" |
|
109 |
and trueT: "true : Bool" |
|
110 |
and falseT: "false : Bool" |
|
58977 | 111 |
and lamT: "\<And>b B. (\<And>x. x:A \<Longrightarrow> b(x):B(x)) \<Longrightarrow> lam x. b(x) : Pi(A,B)" |
112 |
and pairT: "\<And>b B. \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> <a,b>:Sigma(A,B)" |
|
113 |
and inlT: "a:A \<Longrightarrow> inl(a) : A+B" |
|
114 |
and inrT: "b:B \<Longrightarrow> inr(b) : A+B" |
|
20140 | 115 |
by (blast intro: XHs [THEN iffD2])+ |
116 |
||
117 |
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT |
|
118 |
||
119 |
||
60770 | 120 |
subsection \<open>Non-Canonical Type Rules\<close> |
20140 | 121 |
|
58977 | 122 |
lemma lem: "\<lbrakk>a:B(u); u = v\<rbrakk> \<Longrightarrow> a : B(v)" |
20140 | 123 |
by blast |
124 |
||
125 |
||
60770 | 126 |
ML \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
127 |
fun mk_ncanT_tac top_crls crls = |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
128 |
SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
129 |
resolve_tac ctxt ([major] RL top_crls) 1 THEN |
59499 | 130 |
REPEAT_SOME (eresolve_tac ctxt (crls @ @{thms exE bexE conjE disjE})) THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset
|
131 |
ALLGOALS (asm_simp_tac ctxt) THEN |
59499 | 132 |
ALLGOALS (assume_tac ctxt ORELSE' resolve_tac ctxt (prems RL [@{thm lem}]) |
133 |
ORELSE' eresolve_tac ctxt @{thms bspec}) THEN |
|
42793 | 134 |
safe_tac (ctxt addSIs prems)) |
60770 | 135 |
\<close> |
20140 | 136 |
|
60770 | 137 |
method_setup ncanT = \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
138 |
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) |
60770 | 139 |
\<close> |
20140 | 140 |
|
58977 | 141 |
lemma ifT: "\<lbrakk>b:Bool; b=true \<Longrightarrow> t:A(true); b=false \<Longrightarrow> u:A(false)\<rbrakk> \<Longrightarrow> if b then t else u : A(b)" |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
142 |
by ncanT |
20140 | 143 |
|
58977 | 144 |
lemma applyT: "\<lbrakk>f : Pi(A,B); a:A\<rbrakk> \<Longrightarrow> f ` a : B(a)" |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
145 |
by ncanT |
20140 | 146 |
|
58977 | 147 |
lemma splitT: "\<lbrakk>p:Sigma(A,B); \<And>x y. \<lbrakk>x:A; y:B(x); p=<x,y>\<rbrakk> \<Longrightarrow> c(x,y):C(<x,y>)\<rbrakk> \<Longrightarrow> split(p,c):C(p)" |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
148 |
by ncanT |
20140 | 149 |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
150 |
lemma whenT: |
58977 | 151 |
"\<lbrakk>p:A+B; |
152 |
\<And>x. \<lbrakk>x:A; p=inl(x)\<rbrakk> \<Longrightarrow> a(x):C(inl(x)); |
|
153 |
\<And>y. \<lbrakk>y:B; p=inr(y)\<rbrakk> \<Longrightarrow> b(y):C(inr(y))\<rbrakk> \<Longrightarrow> when(p,a,b) : C(p)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
154 |
by ncanT |
20140 | 155 |
|
156 |
lemmas ncanTs = ifT applyT splitT whenT |
|
157 |
||
158 |
||
60770 | 159 |
subsection \<open>Subtypes\<close> |
20140 | 160 |
|
58977 | 161 |
lemma SubtypeD1: "a : Subtype(A, P) \<Longrightarrow> a : A" |
162 |
and SubtypeD2: "a : Subtype(A, P) \<Longrightarrow> P(a)" |
|
20140 | 163 |
by (simp_all add: SubtypeXH) |
164 |
||
58977 | 165 |
lemma SubtypeI: "\<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> a : {x:A. P(x)}" |
20140 | 166 |
by (simp add: SubtypeXH) |
167 |
||
58977 | 168 |
lemma SubtypeE: "\<lbrakk>a : {x:A. P(x)}; \<lbrakk>a:A; P(a)\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
20140 | 169 |
by (simp add: SubtypeXH) |
170 |
||
171 |
||
60770 | 172 |
subsection \<open>Monotonicity\<close> |
20140 | 173 |
|
58977 | 174 |
lemma idM: "mono (\<lambda>X. X)" |
20140 | 175 |
apply (rule monoI) |
176 |
apply assumption |
|
177 |
done |
|
178 |
||
58977 | 179 |
lemma constM: "mono(\<lambda>X. A)" |
20140 | 180 |
apply (rule monoI) |
181 |
apply (rule subset_refl) |
|
182 |
done |
|
183 |
||
58977 | 184 |
lemma "mono(\<lambda>X. A(X)) \<Longrightarrow> mono(\<lambda>X.[A(X)])" |
20140 | 185 |
apply (rule subsetI [THEN monoI]) |
186 |
apply (drule LiftXH [THEN iffD1]) |
|
187 |
apply (erule disjE) |
|
188 |
apply (erule disjI1 [THEN LiftXH [THEN iffD2]]) |
|
189 |
apply (rule disjI2 [THEN LiftXH [THEN iffD2]]) |
|
190 |
apply (drule (1) monoD) |
|
191 |
apply blast |
|
192 |
done |
|
193 |
||
194 |
lemma SgM: |
|
58977 | 195 |
"\<lbrakk>mono(\<lambda>X. A(X)); \<And>x X. x:A(X) \<Longrightarrow> mono(\<lambda>X. B(X,x))\<rbrakk> \<Longrightarrow> |
196 |
mono(\<lambda>X. Sigma(A(X),B(X)))" |
|
20140 | 197 |
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
198 |
dest!: monoD [THEN subsetD]) |
|
199 |
||
58977 | 200 |
lemma PiM: "(\<And>x. x:A \<Longrightarrow> mono(\<lambda>X. B(X,x))) \<Longrightarrow> mono(\<lambda>X. Pi(A,B(X)))" |
20140 | 201 |
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
202 |
dest!: monoD [THEN subsetD]) |
|
203 |
||
58977 | 204 |
lemma PlusM: "\<lbrakk>mono(\<lambda>X. A(X)); mono(\<lambda>X. B(X))\<rbrakk> \<Longrightarrow> mono(\<lambda>X. A(X)+B(X))" |
20140 | 205 |
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls |
206 |
dest!: monoD [THEN subsetD]) |
|
207 |
||
208 |
||
60770 | 209 |
subsection \<open>Recursive types\<close> |
20140 | 210 |
|
60770 | 211 |
subsubsection \<open>Conversion Rules for Fixed Points via monotonicity and Tarski\<close> |
20140 | 212 |
|
58977 | 213 |
lemma NatM: "mono(\<lambda>X. Unit+X)" |
20140 | 214 |
apply (rule PlusM constM idM)+ |
215 |
done |
|
216 |
||
217 |
lemma def_NatB: "Nat = Unit + Nat" |
|
218 |
apply (rule def_lfp_Tarski [OF Nat_def]) |
|
219 |
apply (rule NatM) |
|
220 |
done |
|
221 |
||
58977 | 222 |
lemma ListM: "mono(\<lambda>X.(Unit+Sigma(A,\<lambda>y. X)))" |
20140 | 223 |
apply (rule PlusM SgM constM idM)+ |
224 |
done |
|
225 |
||
226 |
lemma def_ListB: "List(A) = Unit + A * List(A)" |
|
227 |
apply (rule def_lfp_Tarski [OF List_def]) |
|
228 |
apply (rule ListM) |
|
229 |
done |
|
230 |
||
231 |
lemma def_ListsB: "Lists(A) = Unit + A * Lists(A)" |
|
232 |
apply (rule def_gfp_Tarski [OF Lists_def]) |
|
233 |
apply (rule ListM) |
|
234 |
done |
|
235 |
||
58977 | 236 |
lemma IListsM: "mono(\<lambda>X.({} + Sigma(A,\<lambda>y. X)))" |
20140 | 237 |
apply (rule PlusM SgM constM idM)+ |
238 |
done |
|
239 |
||
240 |
lemma def_IListsB: "ILists(A) = {} + A * ILists(A)" |
|
241 |
apply (rule def_gfp_Tarski [OF ILists_def]) |
|
242 |
apply (rule IListsM) |
|
243 |
done |
|
244 |
||
245 |
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB |
|
246 |
||
247 |
||
60770 | 248 |
subsection \<open>Exhaustion Rules\<close> |
20140 | 249 |
|
58977 | 250 |
lemma NatXH: "a : Nat \<longleftrightarrow> (a=zero | (EX x:Nat. a=succ(x)))" |
251 |
and ListXH: "a : List(A) \<longleftrightarrow> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))" |
|
252 |
and ListsXH: "a : Lists(A) \<longleftrightarrow> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))" |
|
253 |
and IListsXH: "a : ILists(A) \<longleftrightarrow> (EX x:A. EX xs:ILists(A).a=x$xs)" |
|
20140 | 254 |
unfolding ind_data_defs |
255 |
by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ |
|
256 |
||
257 |
lemmas iXHs = NatXH ListXH |
|
258 |
||
60770 | 259 |
ML \<open>ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs})\<close> |
20140 | 260 |
|
261 |
||
60770 | 262 |
subsection \<open>Type Rules\<close> |
20140 | 263 |
|
264 |
lemma zeroT: "zero : Nat" |
|
58977 | 265 |
and succT: "n:Nat \<Longrightarrow> succ(n) : Nat" |
20140 | 266 |
and nilT: "[] : List(A)" |
58977 | 267 |
and consT: "\<lbrakk>h:A; t:List(A)\<rbrakk> \<Longrightarrow> h$t : List(A)" |
20140 | 268 |
by (blast intro: iXHs [THEN iffD2])+ |
269 |
||
270 |
lemmas icanTs = zeroT succT nilT consT |
|
271 |
||
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
272 |
|
60770 | 273 |
method_setup incanT = \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
274 |
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) |
60770 | 275 |
\<close> |
20140 | 276 |
|
58977 | 277 |
lemma ncaseT: "\<lbrakk>n:Nat; n=zero \<Longrightarrow> b:C(zero); \<And>x. \<lbrakk>x:Nat; n=succ(x)\<rbrakk> \<Longrightarrow> c(x):C(succ(x))\<rbrakk> |
278 |
\<Longrightarrow> ncase(n,b,c) : C(n)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
279 |
by incanT |
20140 | 280 |
|
58977 | 281 |
lemma lcaseT: "\<lbrakk>l:List(A); l = [] \<Longrightarrow> b:C([]); \<And>h t. \<lbrakk>h:A; t:List(A); l=h$t\<rbrakk> \<Longrightarrow> c(h,t):C(h$t)\<rbrakk> |
282 |
\<Longrightarrow> lcase(l,b,c) : C(l)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
283 |
by incanT |
20140 | 284 |
|
285 |
lemmas incanTs = ncaseT lcaseT |
|
286 |
||
287 |
||
60770 | 288 |
subsection \<open>Induction Rules\<close> |
20140 | 289 |
|
290 |
lemmas ind_Ms = NatM ListM |
|
291 |
||
58977 | 292 |
lemma Nat_ind: "\<lbrakk>n:Nat; P(zero); \<And>x. \<lbrakk>x:Nat; P(x)\<rbrakk> \<Longrightarrow> P(succ(x))\<rbrakk> \<Longrightarrow> P(n)" |
20140 | 293 |
apply (unfold ind_data_defs) |
294 |
apply (erule def_induct [OF Nat_def _ NatM]) |
|
295 |
apply (blast intro: canTs elim!: case_rls) |
|
296 |
done |
|
297 |
||
58977 | 298 |
lemma List_ind: "\<lbrakk>l:List(A); P([]); \<And>x xs. \<lbrakk>x:A; xs:List(A); P(xs)\<rbrakk> \<Longrightarrow> P(x$xs)\<rbrakk> \<Longrightarrow> P(l)" |
20140 | 299 |
apply (unfold ind_data_defs) |
300 |
apply (erule def_induct [OF List_def _ ListM]) |
|
301 |
apply (blast intro: canTs elim!: case_rls) |
|
302 |
done |
|
303 |
||
304 |
lemmas inds = Nat_ind List_ind |
|
305 |
||
306 |
||
60770 | 307 |
subsection \<open>Primitive Recursive Rules\<close> |
20140 | 308 |
|
58977 | 309 |
lemma nrecT: "\<lbrakk>n:Nat; b:C(zero); \<And>x g. \<lbrakk>x:Nat; g:C(x)\<rbrakk> \<Longrightarrow> c(x,g):C(succ(x))\<rbrakk> |
310 |
\<Longrightarrow> nrec(n,b,c) : C(n)" |
|
20140 | 311 |
by (erule Nat_ind) auto |
312 |
||
58977 | 313 |
lemma lrecT: "\<lbrakk>l:List(A); b:C([]); \<And>x xs g. \<lbrakk>x:A; xs:List(A); g:C(xs)\<rbrakk> \<Longrightarrow> c(x,xs,g):C(x$xs) \<rbrakk> |
314 |
\<Longrightarrow> lrec(l,b,c) : C(l)" |
|
20140 | 315 |
by (erule List_ind) auto |
316 |
||
317 |
lemmas precTs = nrecT lrecT |
|
318 |
||
319 |
||
60770 | 320 |
subsection \<open>Theorem proving\<close> |
20140 | 321 |
|
58977 | 322 |
lemma SgE2: "\<lbrakk><a,b> : Sigma(A,B); \<lbrakk>a:A; b:B(a)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
20140 | 323 |
unfolding SgXH by blast |
324 |
||
325 |
(* General theorem proving ignores non-canonical term-formers, *) |
|
326 |
(* - intro rules are type rules for canonical terms *) |
|
327 |
(* - elim rules are case rules (no non-canonical terms appear) *) |
|
328 |
||
60770 | 329 |
ML \<open>ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs})\<close> |
20140 | 330 |
|
331 |
lemmas [intro!] = SubtypeI canTs icanTs |
|
332 |
and [elim!] = SubtypeE XHEs |
|
333 |
||
334 |
||
60770 | 335 |
subsection \<open>Infinite Data Types\<close> |
20140 | 336 |
|
58977 | 337 |
lemma lfp_subset_gfp: "mono(f) \<Longrightarrow> lfp(f) <= gfp(f)" |
20140 | 338 |
apply (rule lfp_lowerbound [THEN subset_trans]) |
339 |
apply (erule gfp_lemma3) |
|
340 |
apply (rule subset_refl) |
|
341 |
done |
|
342 |
||
343 |
lemma gfpI: |
|
344 |
assumes "a:A" |
|
58977 | 345 |
and "\<And>x X. \<lbrakk>x:A; ALL y:A. t(y):X\<rbrakk> \<Longrightarrow> t(x) : B(X)" |
20140 | 346 |
shows "t(a) : gfp(B)" |
347 |
apply (rule coinduct) |
|
58977 | 348 |
apply (rule_tac P = "\<lambda>x. EX y:A. x=t (y)" in CollectI) |
41526 | 349 |
apply (blast intro!: assms)+ |
20140 | 350 |
done |
351 |
||
58977 | 352 |
lemma def_gfpI: "\<lbrakk>C == gfp(B); a:A; \<And>x X. \<lbrakk>x:A; ALL y:A. t(y):X\<rbrakk> \<Longrightarrow> t(x) : B(X)\<rbrakk> \<Longrightarrow> t(a) : C" |
20140 | 353 |
apply unfold |
354 |
apply (erule gfpI) |
|
355 |
apply blast |
|
356 |
done |
|
357 |
||
358 |
(* EG *) |
|
359 |
lemma "letrec g x be zero$g(x) in g(bot) : Lists(Nat)" |
|
360 |
apply (rule refl [THEN UnitXH [THEN iffD2], THEN Lists_def [THEN def_gfpI]]) |
|
361 |
apply (subst letrecB) |
|
362 |
apply (unfold cons_def) |
|
363 |
apply blast |
|
364 |
done |
|
365 |
||
366 |
||
60770 | 367 |
subsection \<open>Lemmas and tactics for using the rule @{text |
368 |
"coinduct3"} on @{text "[="} and @{text "="}\<close> |
|
20140 | 369 |
|
58977 | 370 |
lemma lfpI: "\<lbrakk>mono(f); a : f(lfp(f))\<rbrakk> \<Longrightarrow> a : lfp(f)" |
20140 | 371 |
apply (erule lfp_Tarski [THEN ssubst]) |
372 |
apply assumption |
|
373 |
done |
|
374 |
||
58977 | 375 |
lemma ssubst_single: "\<lbrakk>a = a'; a' : A\<rbrakk> \<Longrightarrow> a : A" |
20140 | 376 |
by simp |
377 |
||
58977 | 378 |
lemma ssubst_pair: "\<lbrakk>a = a'; b = b'; <a',b'> : A\<rbrakk> \<Longrightarrow> <a,b> : A" |
20140 | 379 |
by simp |
380 |
||
381 |
||
60770 | 382 |
ML \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
383 |
val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} => |
42793 | 384 |
fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1); |
60770 | 385 |
\<close> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
386 |
|
60770 | 387 |
method_setup coinduct3 = \<open>Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)\<close> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
388 |
|
58977 | 389 |
lemma ci3_RI: "\<lbrakk>mono(Agen); a : R\<rbrakk> \<Longrightarrow> a : lfp(\<lambda>x. Agen(x) Un R Un A)" |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
390 |
by coinduct3 |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
391 |
|
58977 | 392 |
lemma ci3_AgenI: "\<lbrakk>mono(Agen); a : Agen(lfp(\<lambda>x. Agen(x) Un R Un A))\<rbrakk> \<Longrightarrow> |
393 |
a : lfp(\<lambda>x. Agen(x) Un R Un A)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
394 |
by coinduct3 |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
395 |
|
58977 | 396 |
lemma ci3_AI: "\<lbrakk>mono(Agen); a : A\<rbrakk> \<Longrightarrow> a : lfp(\<lambda>x. Agen(x) Un R Un A)" |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
397 |
by coinduct3 |
20140 | 398 |
|
60770 | 399 |
ML \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
400 |
fun genIs_tac ctxt genXH gen_mono = |
60754 | 401 |
resolve_tac ctxt [genXH RS @{thm iffD2}] THEN' |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset
|
402 |
simp_tac ctxt THEN' |
42793 | 403 |
TRY o fast_tac |
404 |
(ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}]) |
|
60770 | 405 |
\<close> |
20140 | 406 |
|
60770 | 407 |
method_setup genIs = \<open> |
42814 | 408 |
Attrib.thm -- Attrib.thm >> |
409 |
(fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono)) |
|
60770 | 410 |
\<close> |
20140 | 411 |
|
412 |
||
60770 | 413 |
subsection \<open>POgen\<close> |
20140 | 414 |
|
415 |
lemma PO_refl: "<a,a> : PO" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
416 |
by (rule po_refl [THEN PO_iff [THEN iffD1]]) |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
417 |
|
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
418 |
lemma POgenIs: |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
419 |
"<true,true> : POgen(R)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
420 |
"<false,false> : POgen(R)" |
58977 | 421 |
"\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : POgen(R)" |
422 |
"\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : POgen(R)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
423 |
"<one,one> : POgen(R)" |
58977 | 424 |
"<a,a'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
425 |
<inl(a),inl(a')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
426 |
"<b,b'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
|
427 |
<inr(b),inr(b')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
428 |
"<zero,zero> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
429 |
"<n,n'> : lfp(\<lambda>x. POgen(x) Un R Un PO) \<Longrightarrow> |
|
430 |
<succ(n),succ(n')> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
431 |
"<[],[]> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
432 |
"\<lbrakk><h,h'> : lfp(\<lambda>x. POgen(x) Un R Un PO); <t,t'> : lfp(\<lambda>x. POgen(x) Un R Un PO)\<rbrakk> |
|
433 |
\<Longrightarrow> <h$t,h'$t'> : POgen(lfp(\<lambda>x. POgen(x) Un R Un PO))" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
434 |
unfolding data_defs by (genIs POgenXH POgen_mono)+ |
20140 | 435 |
|
60770 | 436 |
ML \<open> |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
437 |
fun POgen_tac ctxt (rla, rlb) i = |
42793 | 438 |
SELECT_GOAL (safe_tac ctxt) i THEN |
60754 | 439 |
resolve_tac ctxt [rlb RS (rla RS @{thm ssubst_pair})] i THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
440 |
(REPEAT (resolve_tac ctxt |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
441 |
(@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
442 |
(@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
443 |
[@{thm POgen_mono} RS @{thm ci3_RI}]) i)) |
60770 | 444 |
\<close> |
20140 | 445 |
|
446 |
||
60770 | 447 |
subsection \<open>EQgen\<close> |
20140 | 448 |
|
449 |
lemma EQ_refl: "<a,a> : EQ" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
450 |
by (rule refl [THEN EQ_iff [THEN iffD1]]) |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
451 |
|
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
452 |
lemma EQgenIs: |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
453 |
"<true,true> : EQgen(R)" |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
454 |
"<false,false> : EQgen(R)" |
58977 | 455 |
"\<lbrakk><a,a'> : R; <b,b'> : R\<rbrakk> \<Longrightarrow> <<a,b>,<a',b'>> : EQgen(R)" |
456 |
"\<And>b b'. (\<And>x. <b(x),b'(x)> : R) \<Longrightarrow> <lam x. b(x),lam x. b'(x)> : EQgen(R)" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
457 |
"<one,one> : EQgen(R)" |
58977 | 458 |
"<a,a'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
459 |
<inl(a),inl(a')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
460 |
"<b,b'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
|
461 |
<inr(b),inr(b')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
462 |
"<zero,zero> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
463 |
"<n,n'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ) \<Longrightarrow> |
|
464 |
<succ(n),succ(n')> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
465 |
"<[],[]> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
466 |
"\<lbrakk><h,h'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ); <t,t'> : lfp(\<lambda>x. EQgen(x) Un R Un EQ)\<rbrakk> |
|
467 |
\<Longrightarrow> <h$t,h'$t'> : EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))" |
|
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
468 |
unfolding data_defs by (genIs EQgenXH EQgen_mono)+ |
20140 | 469 |
|
60770 | 470 |
ML \<open> |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
471 |
fun EQgen_raw_tac ctxt i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
472 |
(REPEAT (resolve_tac ctxt (@{thms EQgenIs} @ |
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
473 |
[@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
474 |
(@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @ |
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset
|
475 |
[@{thm EQgen_mono} RS @{thm ci3_RI}]) i)) |
20140 | 476 |
|
477 |
(* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *) |
|
478 |
(* then reduce this to a goal <a',b'> : R (hopefully?) *) |
|
479 |
(* rews are rewrite rules that would cause looping in the simpifier *) |
|
480 |
||
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset
|
481 |
fun EQgen_tac ctxt rews i = |
20140 | 482 |
SELECT_GOAL |
42793 | 483 |
(TRY (safe_tac ctxt) THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
484 |
resolve_tac ctxt ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset
|
485 |
ALLGOALS (simp_tac ctxt) THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
486 |
ALLGOALS (EQgen_raw_tac ctxt)) i |
60770 | 487 |
\<close> |
0 | 488 |
|
60770 | 489 |
method_setup EQgen = \<open> |
58971 | 490 |
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (EQgen_tac ctxt ths)) |
60770 | 491 |
\<close> |
58971 | 492 |
|
0 | 493 |
end |