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