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