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