1 theory QuotMain

     2 imports QuotScript QuotList Prove

     3 uses ("quotient_info.ML") 

     4      ("quotient.ML")

     5      ("quotient_def.ML")

     6 begin

     7 

     8 locale QUOT_TYPE =

     9   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    10   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"

    11   and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"

    12   assumes equiv: "EQUIV R"

    13   and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"

    14   and     rep_inverse: "\<And>x. Abs (Rep x) = x"

    15   and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"

    16   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"

    17 begin

    18 

    19 definition

    20   ABS::"'a \<Rightarrow> 'b"

    21 where

    22   "ABS x \<equiv> Abs (R x)"

    23 

    24 definition

    25   REP::"'b \<Rightarrow> 'a"

    26 where

    27   "REP a = Eps (Rep a)"

    28 

    29 lemma lem9:

    30   shows "R (Eps (R x)) = R x"

    31 proof -

    32   have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)

    33   then have "R x (Eps (R x))" by (rule someI)

    34   then show "R (Eps (R x)) = R x"

    35     using equiv unfolding EQUIV_def by simp

    36 qed

    37 

    38 theorem thm10:

    39   shows "ABS (REP a) \<equiv> a"

    40   apply  (rule eq_reflection)

    41   unfolding ABS_def REP_def

    42 proof -

    43   from rep_prop

    44   obtain x where eq: "Rep a = R x" by auto

    45   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp

    46   also have "\<dots> = Abs (R x)" using lem9 by simp

    47   also have "\<dots> = Abs (Rep a)" using eq by simp

    48   also have "\<dots> = a" using rep_inverse by simp

    49   finally

    50   show "Abs (R (Eps (Rep a))) = a" by simp

    51 qed

    52 

    53 lemma REP_refl:

    54   shows "R (REP a) (REP a)"

    55 unfolding REP_def

    56 by (simp add: equiv[simplified EQUIV_def])

    57 

    58 lemma lem7:

    59   shows "(R x = R y) = (Abs (R x) = Abs (R y))"

    60 apply(rule iffI)

    61 apply(simp)

    62 apply(drule rep_inject[THEN iffD2])

    63 apply(simp add: abs_inverse)

    64 done

    65 

    66 theorem thm11:

    67   shows "R r r' = (ABS r = ABS r')"

    68 unfolding ABS_def

    69 by (simp only: equiv[simplified EQUIV_def] lem7)

    70 

    71 

    72 lemma REP_ABS_rsp:

    73   shows "R f (REP (ABS g)) = R f g"

    74   and   "R (REP (ABS g)) f = R g f"

    75 by (simp_all add: thm10 thm11)

    76 

    77 lemma QUOTIENT:

    78   "QUOTIENT R ABS REP"

    79 apply(unfold QUOTIENT_def)

    80 apply(simp add: thm10)

    81 apply(simp add: REP_refl)

    82 apply(subst thm11[symmetric])

    83 apply(simp add: equiv[simplified EQUIV_def])

    84 done

    85 

    86 lemma R_trans:

    87   assumes ab: "R a b"

    88   and     bc: "R b c"

    89   shows "R a c"

    90 proof -

    91   have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

    92   moreover have ab: "R a b" by fact

    93   moreover have bc: "R b c" by fact

    94   ultimately show "R a c" unfolding TRANS_def by blast

    95 qed

    96 

    97 lemma R_sym:

    98   assumes ab: "R a b"

    99   shows "R b a"

   100 proof -

   101   have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

   102   then show "R b a" using ab unfolding SYM_def by blast

   103 qed

   104 

   105 lemma R_trans2:

   106   assumes ac: "R a c"

   107   and     bd: "R b d"

   108   shows "R a b = R c d"

   109 using ac bd

   110 by (blast intro: R_trans R_sym)

   111 

   112 lemma REPS_same:

   113   shows "R (REP a) (REP b) \<equiv> (a = b)"

   114 proof -

   115   have "R (REP a) (REP b) = (a = b)"

   116   proof

   117     assume as: "R (REP a) (REP b)"

   118     from rep_prop

   119     obtain x y

   120       where eqs: "Rep a = R x" "Rep b = R y" by blast

   121     from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp

   122     then have "R x (Eps (R y))" using lem9 by simp

   123     then have "R (Eps (R y)) x" using R_sym by blast

   124     then have "R y x" using lem9 by simp

   125     then have "R x y" using R_sym by blast

   126     then have "ABS x = ABS y" using thm11 by simp

   127     then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp

   128     then show "a = b" using rep_inverse by simp

   129   next

   130     assume ab: "a = b"

   131     have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp

   132     then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto

   133   qed

   134   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   135 qed

   136 

   137 end

   138 

   139 lemma equiv_trans2:

   140   assumes e: "EQUIV R"

   141   and     ac: "R a c"

   142   and     bd: "R b d"

   143   shows "R a b = R c d"

   144 using ac bd e

   145 unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def

   146 by (blast)

   147 

   148 section {* type definition for the quotient type *}

   149 

   150 (* the auxiliary data for the quotient types *)

   151 use "quotient_info.ML"

   152 

   153 declare [[map list = (map, LIST_REL)]]

   154 declare [[map * = (prod_fun, prod_rel)]]

   155 declare [[map "fun" = (fun_map, FUN_REL)]]

   156 

   157 ML {* maps_lookup @{theory} "List.list" *}

   158 ML {* maps_lookup @{theory} "*" *}

   159 ML {* maps_lookup @{theory} "fun" *}

   160 

   161 

   162 (* definition of the quotient types *)

   163 (* FIXME: should be called quotient_typ.ML *)

   164 use "quotient.ML"

   165 

   166 

   167 (* lifting of constants *)

   168 use "quotient_def.ML"

   169 

   170 (* TODO: Consider defining it with an "if"; sth like:

   171    Babs p m = \<lambda>x. if x \<in> p then m x else undefined

   172 *)

   173 definition

   174   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"

   175 where

   176   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"

   177 

   178 section {* ATOMIZE *}

   179 

   180 lemma atomize_eqv[atomize]:

   181   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"

   182 proof

   183   assume "A \<equiv> B"

   184   then show "Trueprop A \<equiv> Trueprop B" by unfold

   185 next

   186   assume *: "Trueprop A \<equiv> Trueprop B"

   187   have "A = B"

   188   proof (cases A)

   189     case True

   190     have "A" by fact

   191     then show "A = B" using * by simp

   192   next

   193     case False

   194     have "\<not>A" by fact

   195     then show "A = B" using * by auto

   196   qed

   197   then show "A \<equiv> B" by (rule eq_reflection)

   198 qed

   199 

   200 ML {*

   201 fun atomize_thm thm =

   202 let

   203   val thm' = Thm.freezeT (forall_intr_vars thm)

   204   val thm'' = ObjectLogic.atomize (cprop_of thm')

   205 in

   206   @{thm equal_elim_rule1} OF [thm'', thm']

   207 end

   208 *}

   209 

   210 section {* infrastructure about id *}

   211 

   212 lemma prod_fun_id: "prod_fun id id \<equiv> id"

   213   by (rule eq_reflection) (simp add: prod_fun_def)

   214 

   215 lemma map_id: "map id \<equiv> id"

   216   apply (rule eq_reflection)

   217   apply (rule ext)

   218   apply (rule_tac list="x" in list.induct)

   219   apply (simp_all)

   220   done

   221 

   222 lemmas id_simps =

   223   FUN_MAP_I[THEN eq_reflection]

   224   id_apply[THEN eq_reflection]

   225   id_def[THEN eq_reflection,symmetric]

   226   prod_fun_id map_id

   227 

   228 ML {*

   229 fun simp_ids thm =

   230   MetaSimplifier.rewrite_rule @{thms id_simps} thm

   231 *}

   232 

   233 section {* Debugging infrastructure for testing tactics *}

   234 

   235 ML {*

   236 fun my_print_tac ctxt s i thm =

   237 let

   238   val prem_str = nth (prems_of thm) (i - 1)

   239                  |> Syntax.string_of_term ctxt

   240                  handle Subscript => "no subgoal"

   241   val _ = tracing (s ^ "\n" ^ prem_str)

   242 in

   243   Seq.single thm

   244 end *}

   245 

   246 

   247 ML {*

   248 fun DT ctxt s tac i thm =

   249 let

   250   val before_goal = nth (prems_of thm) (i - 1)

   251                     |> Syntax.string_of_term ctxt

   252   val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]

   253                    |> cat_lines

   254 in 

   255   EVERY [tac i, my_print_tac ctxt before_msg i] thm

   256 end

   257 

   258 fun NDT ctxt s tac thm = tac thm  

   259 *}

   260 

   261 

   262 section {*  Infrastructure about definitions *}

   263 

   264 (* Does the same as 'subst' in a given theorem *)

   265 ML {*

   266 fun eqsubst_thm ctxt thms thm =

   267   let

   268     val goalstate = Goal.init (Thm.cprop_of thm)

   269     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of

   270       NONE => error "eqsubst_thm"

   271     | SOME th => cprem_of th 1

   272     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1

   273     val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');

   274     val cgoal = cterm_of (ProofContext.theory_of ctxt) goal

   275     val rt = Goal.prove_internal [] cgoal (fn _ => tac);

   276   in

   277     @{thm equal_elim_rule1} OF [rt, thm]

   278   end

   279 *}

   280 

   281 (* expects atomized definitions *)

   282 ML {*

   283 fun add_lower_defs_aux lthy thm =

   284   let

   285     val e1 = @{thm fun_cong} OF [thm];

   286     val f = eqsubst_thm lthy @{thms fun_map.simps} e1;

   287     val g = simp_ids f

   288   in

   289     (simp_ids thm) :: (add_lower_defs_aux lthy g)

   290   end

   291   handle _ => [simp_ids thm]

   292 *}

   293 

   294 ML {*

   295 fun add_lower_defs lthy def =

   296   let

   297     val def_pre_sym = symmetric def

   298     val def_atom = atomize_thm def_pre_sym

   299     val defs_all = add_lower_defs_aux lthy def_atom

   300   in

   301     map Thm.varifyT defs_all

   302   end

   303 *}

   304 

   305 section {* Infrastructure for collecting theorems for starting the lifting *}

   306 

   307 ML {*

   308 fun lookup_quot_data lthy qty =

   309   let

   310     val qty_name = fst (dest_Type qty)

   311     val SOME quotdata = quotdata_lookup lthy qty_name

   312                   (* cu: Changed the lookup\<dots>not sure whether this works *)

   313     (* TODO: Should no longer be needed *)

   314     val rty = Logic.unvarifyT (#rtyp quotdata)

   315     val rel = #rel quotdata

   316     val rel_eqv = #equiv_thm quotdata

   317     val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]

   318   in

   319     (rty, rel, rel_refl, rel_eqv)

   320   end

   321 *}

   322 

   323 ML {*

   324 fun lookup_quot_thms lthy qty_name =

   325   let

   326     val thy = ProofContext.theory_of lthy;

   327     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")

   328     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")

   329     val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")

   330     val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)

   331   in

   332     (trans2, reps_same, absrep, quot)

   333   end

   334 *}

   335 

   336 ML {*

   337 fun lookup_quot_consts defs =

   338   let

   339     fun dest_term (a $ b) = (a, b);

   340     val def_terms = map (snd o Logic.dest_equals o concl_of) defs;

   341   in

   342     map (fst o dest_Const o snd o dest_term) def_terms

   343   end

   344 *}

   345 

   346 section {* Infrastructure for special quotient identity *}

   347 

   348 definition

   349   "qid TYPE('a) TYPE('b) x \<equiv> x"

   350 

   351 ML {*

   352 fun get_typ_aux (Type ("itself", [T])) = T 

   353 fun get_typ (Const ("TYPE", T)) = get_typ_aux T

   354 fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =

   355   (get_typ ty1, get_typ ty2)

   356 

   357 fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true

   358   | is_qid _ = false

   359 

   360 

   361 fun mk_itself ty = Type ("itself", [ty])

   362 fun mk_TYPE ty = Const ("TYPE", mk_itself ty)

   363 fun mk_qid (rty, qty, trm) = 

   364   Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) 

   365     $ mk_TYPE rty $ mk_TYPE qty $ trm

   366 *}

   367 

   368 ML {*

   369 fun insertion_aux rtrm qtrm =

   370   case (rtrm, qtrm) of

   371     (Abs (x, ty, t), Abs (x', ty', t')) =>

   372        let

   373          val (y, s) = Term.dest_abs (x, ty, t)

   374          val (_, s') = Term.dest_abs (x', ty', t')

   375          val yvar = Free (y, ty)

   376          val result = Term.lambda_name (y, yvar) (insertion_aux s s')

   377        in     

   378          if ty = ty'

   379          then result

   380          else mk_qid (ty, ty', result)

   381        end

   382   | (t1 $ t2, t1' $ t2') =>

   383        let 

   384          val rty = fastype_of rtrm

   385          val qty = fastype_of qtrm 

   386          val subtrm1 = insertion_aux t1 t1' 

   387          val subtrm2 = insertion_aux t2 t2'

   388        in

   389          if rty = qty

   390          then subtrm1 $ subtrm2

   391          else mk_qid (rty, qty, subtrm1 $ subtrm2)

   392        end

   393   | (Free (_, ty), Free (_, ty')) =>

   394        if ty = ty'

   395        then rtrm 

   396        else mk_qid (ty, ty', rtrm)

   397   | (Const (s, ty), Const (s', ty')) =>

   398        if s = s' andalso ty = ty'

   399        then rtrm

   400        else mk_qid (ty, ty', rtrm) 

   401   | (_, _) => raise (LIFT_MATCH "insertion")

   402 *}

   403 

   404 section {* Regularization *} 

   405 

   406 (*

   407 Regularizing an rtrm means:

   408  - quantifiers over a type that needs lifting are replaced by

   409    bounded quantifiers, for example:

   410       \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P

   411 

   412    the relation R is given by the rty and qty;

   413  

   414  - abstractions over a type that needs lifting are replaced

   415    by bounded abstractions:

   416       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)

   417 

   418  - equalities over the type being lifted are replaced by

   419    corresponding relations:

   420       A = B     \<Longrightarrow>     A \<approx> B

   421 

   422    example with more complicated types of A, B:

   423       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B

   424 *)

   425 

   426 ML {*

   427 (* builds the relation that is the argument of respects *)

   428 fun mk_resp_arg lthy (rty, qty) =

   429 let

   430   val thy = ProofContext.theory_of lthy

   431 in  

   432   if rty = qty

   433   then HOLogic.eq_const rty

   434   else

   435     case (rty, qty) of

   436       (Type (s, tys), Type (s', tys')) =>

   437        if s = s' 

   438        then let

   439               val SOME map_info = maps_lookup thy s

   440               val args = map (mk_resp_arg lthy) (tys ~~ tys')

   441             in

   442               list_comb (Const (#relfun map_info, dummyT), args) 

   443             end  

   444        else let  

   445               val SOME qinfo = quotdata_lookup_thy thy s'

   446               (* FIXME: check in this case that the rty and qty *)

   447               (* FIXME: correspond to each other *)

   448               val (s, _) = dest_Const (#rel qinfo)

   449               (* FIXME: the relation should only be the string        *)

   450               (* FIXME: and the type needs to be calculated as below; *)

   451               (* FIXME: maybe one should actually have a term         *)

   452               (* FIXME: and one needs to force it to have this type   *)

   453             in

   454               Const (s, rty --> rty --> @{typ bool})

   455             end

   456       | _ => HOLogic.eq_const dummyT 

   457              (* FIXME: check that the types correspond to each other? *)

   458 end

   459 *}

   460 

   461 ML {*

   462 val mk_babs = Const (@{const_name "Babs"}, dummyT)

   463 val mk_ball = Const (@{const_name "Ball"}, dummyT)

   464 val mk_bex  = Const (@{const_name "Bex"}, dummyT)

   465 val mk_resp = Const (@{const_name Respects}, dummyT)

   466 *}

   467 

   468 ML {*

   469 (* - applies f to the subterm of an abstraction,   *)

   470 (*   otherwise to the given term,                  *)

   471 (* - used by regularize, therefore abstracted      *)

   472 (*   variables do not have to be treated specially *)

   473 

   474 fun apply_subt f trm =

   475   case trm of

   476     (Abs (x, T, t)) => Abs (x, T, f t)

   477   | _ => f trm

   478 

   479 (* the major type of All and Ex quantifiers *)

   480 fun qnt_typ ty = domain_type (domain_type ty)  

   481 *}

   482 

   483 ML {*

   484 (* produces a regularized version of trm      *)

   485 (* - the result is still not completely typed *)

   486 (* - does not need any special treatment of   *)

   487 (*   bound variables                          *)

   488 

   489 fun regularize_trm lthy trm =

   490   case trm of

   491     (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>

   492        let

   493          val rty = get_typ rty'

   494          val qty = get_typ qty'

   495          val subtrm = regularize_trm lthy t

   496        in     

   497          mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)

   498        end

   499   | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => 

   500        let

   501          val subtrm = apply_subt (regularize_trm lthy) t

   502        in

   503          if ty = ty'

   504          then Const (@{const_name "All"}, ty) $ subtrm

   505          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   506        end

   507   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>

   508        let

   509          val subtrm = apply_subt (regularize_trm lthy) t t'

   510        in

   511          if ty = ty'

   512          then Const (@{const_name "Ex"}, ty) $ subtrm

   513          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   514        end

   515     (* FIXME: Should = only be replaced, when fully applied? *) 

   516     (* Then there must be a 2nd argument                     *)

   517   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>

   518        let

   519          val subtrm = regularize_trm lthy t t'

   520        in

   521          if ty = ty'

   522          then Const (@{const_name "op ="}, ty) $ subtrm

   523          else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm

   524        end 

   525   | (t1 $ t2, t1' $ t2') =>

   526        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

   527   | (Free (x, ty), Free (x', ty')) => 

   528        (* this case cannot arrise as we start with two fully atomized terms *)

   529        raise (LIFT_MATCH "regularize (frees)")

   530   | (Bound i, Bound i') =>

   531        if i = i' 

   532        then rtrm 

   533        else raise (LIFT_MATCH "regularize (bounds)")

   534   | (Const (s, ty), Const (s', ty')) =>

   535        if s = s' andalso ty = ty'

   536        then rtrm

   537        else rtrm (* FIXME: check correspondence according to definitions *) 

   538   | (rt, qt) => 

   539        raise (LIFT_MATCH "regularize (default)")

   540 *}

   541 

   542 (*

   543 FIXME / TODO: needs to be adapted

   544 

   545 To prove that the raw theorem implies the regularised one, 

   546 we try in order:

   547 

   548  - Reflexivity of the relation

   549  - Assumption

   550  - Elimnating quantifiers on both sides of toplevel implication

   551  - Simplifying implications on both sides of toplevel implication

   552  - Ball (Respects ?E) ?P = All ?P

   553  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q

   554 

   555 *)

   556 

   557 (* FIXME: they should be in in the new Isabelle *)

   558 lemma [mono]: 

   559   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"

   560 by blast

   561 

   562 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"

   563 by auto

   564 

   565 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)

   566 ML {*

   567 fun equiv_tac rel_eqvs =

   568   REPEAT_ALL_NEW (FIRST' 

   569     [resolve_tac rel_eqvs,

   570      rtac @{thm IDENTITY_EQUIV},

   571      rtac @{thm LIST_EQUIV}])

   572 *}

   573 

   574 ML {*

   575 fun ball_reg_eqv_simproc rel_eqvs ss redex =

   576   let

   577     val ctxt = Simplifier.the_context ss

   578     val thy = ProofContext.theory_of ctxt

   579   in

   580   case redex of

   581       (ogl as ((Const (@{const_name "Ball"}, _)) $

   582         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>

   583       (let

   584         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;

   585         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   586         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   587         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);

   588 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)

   589       in

   590         SOME thm

   591       end

   592       handle _ => NONE

   593       )

   594   | _ => NONE

   595   end

   596 *}

   597 

   598 ML {*

   599 fun bex_reg_eqv_simproc rel_eqvs ss redex =

   600   let

   601     val ctxt = Simplifier.the_context ss

   602     val thy = ProofContext.theory_of ctxt

   603   in

   604   case redex of

   605       (ogl as ((Const (@{const_name "Bex"}, _)) $

   606         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>

   607       (let

   608         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;

   609         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   610         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   611         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);

   612 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)

   613       in

   614         SOME thm

   615       end

   616       handle _ => NONE

   617       )

   618   | _ => NONE

   619   end

   620 *}

   621 

   622 ML {*

   623 fun prep_trm thy (x, (T, t)) =

   624   (cterm_of thy (Var (x, T)), cterm_of thy t)

   625 

   626 fun prep_ty thy (x, (S, ty)) =

   627   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)

   628 *}

   629 

   630 ML {*

   631 fun matching_prs thy pat trm =

   632 let

   633   val univ = Unify.matchers thy [(pat, trm)]

   634   val SOME (env, _) = Seq.pull univ

   635   val tenv = Vartab.dest (Envir.term_env env)

   636   val tyenv = Vartab.dest (Envir.type_env env)

   637 in

   638   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)

   639 end

   640 *}

   641 

   642 ML {*

   643 fun ball_reg_eqv_range_simproc rel_eqvs ss redex =

   644   let

   645     val ctxt = Simplifier.the_context ss

   646     val thy = ProofContext.theory_of ctxt

   647   in

   648   case redex of

   649       (ogl as ((Const (@{const_name "Ball"}, _)) $

   650         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>

   651       (let

   652         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;

   653         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   654         val _ = tracing (Syntax.string_of_term ctxt glc);

   655         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   656         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);

   657         val R1c = cterm_of thy R1;

   658         val thmi = Drule.instantiate' [] [SOME R1c] thm;

   659 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)

   660         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl

   661         val _ = tracing "AAA";

   662         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);

   663         val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));

   664       in

   665         SOME thm2

   666       end

   667       handle _ => NONE

   668 

   669       )

   670   | _ => NONE

   671   end

   672 *}

   673 

   674 ML {*

   675 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =

   676   let

   677     val ctxt = Simplifier.the_context ss

   678     val thy = ProofContext.theory_of ctxt

   679   in

   680   case redex of

   681       (ogl as ((Const (@{const_name "Bex"}, _)) $

   682         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>

   683       (let

   684         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;

   685         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   686         val _ = tracing (Syntax.string_of_term ctxt glc);

   687         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   688         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);

   689         val R1c = cterm_of thy R1;

   690         val thmi = Drule.instantiate' [] [SOME R1c] thm;

   691 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)

   692         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl

   693         val _ = tracing "AAA";

   694         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);

   695         val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));

   696       in

   697         SOME thm2

   698       end

   699       handle _ => NONE

   700 

   701       )

   702   | _ => NONE

   703   end

   704 *}

   705 

   706 lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"

   707 by (simp add: EQUIV_REFL)

   708 

   709 ML {*

   710 fun regularize_tac ctxt rel_eqvs =

   711   let

   712     val pat1 = [@{term "Ball (Respects R) P"}];

   713     val pat2 = [@{term "Bex (Respects R) P"}];

   714     val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];

   715     val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];

   716     val thy = ProofContext.theory_of ctxt

   717     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))

   718     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))

   719     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))

   720     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))

   721     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]

   722     (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)

   723     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs

   724   in

   725   ObjectLogic.full_atomize_tac THEN'

   726   simp_tac simp_ctxt THEN'

   727   REPEAT_ALL_NEW (FIRST' [

   728     rtac @{thm ball_reg_right},

   729     rtac @{thm bex_reg_left},

   730     resolve_tac (Inductive.get_monos ctxt),

   731     rtac @{thm ball_all_comm},

   732     rtac @{thm bex_ex_comm},

   733     resolve_tac eq_eqvs,

   734     simp_tac simp_ctxt

   735   ])

   736   end

   737 *}

   738 

   739 section {* Injections of REP and ABSes *}

   740 

   741 (*

   742 Injecting REPABS means:

   743 

   744   For abstractions:

   745   * If the type of the abstraction doesn't need lifting we recurse.

   746   * If it does we add RepAbs around the whole term and check if the

   747     variable needs lifting.

   748     * If it doesn't then we recurse

   749     * If it does we recurse and put 'RepAbs' around all occurences

   750       of the variable in the obtained subterm. This in combination

   751       with the RepAbs above will let us change the type of the

   752       abstraction with rewriting.

   753   For applications:

   754   * If the term is 'Respects' applied to anything we leave it unchanged

   755   * If the term needs lifting and the head is a constant that we know

   756     how to lift, we put a RepAbs and recurse

   757   * If the term needs lifting and the head is a free applied to subterms

   758     (if it is not applied we treated it in Abs branch) then we

   759     put RepAbs and recurse

   760   * Otherwise just recurse.

   761 *)

   762 

   763 ML {*

   764 fun mk_repabs lthy (T, T') trm = 

   765   Quotient_Def.get_fun repF lthy (T, T') 

   766     $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)

   767 *}

   768 

   769 ML {*

   770 (* bound variables need to be treated properly,  *)

   771 (* as the type of subterms need to be calculated *)

   772 

   773 fun inj_repabs_trm lthy (rtrm, qtrm) =

   774 let

   775   val rty = fastype_of rtrm

   776   val qty = fastype_of qtrm

   777 in

   778   case (rtrm, qtrm) of

   779     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>

   780        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   781   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>

   782        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   783   | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>

   784        Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   785   | (Abs (x, T, t), Abs (x', T', t')) =>

   786       let

   787         val (y, s) = Term.dest_abs (x, T, t)

   788         val (_, s') = Term.dest_abs (x', T', t')

   789         val yvar = Free (y, T)

   790         val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))

   791       in

   792         if rty = qty 

   793         then result

   794         else mk_repabs lthy (rty, qty) result

   795       end

   796   | _ =>

   797       (* FIXME / TODO: this is a case that needs to be looked at          *)

   798       (* - variables get a rep-abs insde and outside an application       *)

   799       (* - constants only get a rep-abs on the outside of the application *)

   800       (* - applications get a rep-abs insde and outside an application    *)

   801       let

   802         val (rhead, rargs) = strip_comb rtrm

   803         val (qhead, qargs) = strip_comb qtrm

   804         val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)

   805       in

   806         if rty = qty

   807         then

   808           case (rhead, qhead) of

   809             (Free (_, T), Free (_, T')) =>

   810               if T = T' then list_comb (rhead, rargs')

   811               else list_comb (mk_repabs lthy (T, T') rhead, rargs')

   812           | _ => list_comb (rhead, rargs')

   813         else

   814           case (rhead, qhead, length rargs') of

   815             (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead

   816           | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead

   817           | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 

   818           | (Free (x, T), Free (x', T'), _) => 

   819                mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))

   820           | (Abs _, Abs _, _ ) =>

   821                mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 

   822           | _ => raise (LIFT_MATCH "injection")

   823       end

   824 end

   825 *}

   826 

   827 section {* RepAbs Injection Tactic *}

   828 

   829 ML {*

   830 fun stripped_term_of ct =

   831   ct |> term_of |> HOLogic.dest_Trueprop

   832 *}

   833 

   834 ML {*

   835 fun instantiate_tac thm = 

   836   Subgoal.FOCUS (fn {concl, ...} =>

   837   let

   838     val pat = Drule.strip_imp_concl (cprop_of thm)

   839     val insts = Thm.match (pat, concl)

   840   in

   841     rtac (Drule.instantiate insts thm) 1

   842   end

   843   handle _ => no_tac)

   844 *}

   845 

   846 ML {*

   847 fun quotient_tac quot_thms =

   848   REPEAT_ALL_NEW (FIRST' 

   849     [rtac @{thm FUN_QUOTIENT},

   850      resolve_tac quot_thms,

   851      rtac @{thm IDENTITY_QUOTIENT},

   852      (* For functional identity quotients, (op = ---> op =) *)

   853      (* TODO: think about the other way around, if we need to shorten the relation *)

   854      CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])

   855 *}

   856 

   857 lemma FUN_REL_I:

   858   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"

   859   shows "(R1 ===> R2) f g"

   860 using a by (simp add: FUN_REL.simps)

   861 

   862 ML {*

   863 val lambda_res_tac =

   864   Subgoal.FOCUS (fn {concl, ...} =>

   865     case (stripped_term_of concl) of

   866        (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1

   867      | _ => no_tac)

   868 *}

   869 

   870 ML {*

   871 val weak_lambda_res_tac =

   872   Subgoal.FOCUS (fn {concl, ...} =>

   873     case (stripped_term_of concl) of

   874        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1

   875      | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1

   876      | _ => no_tac)

   877 *}

   878 

   879 ML {*

   880 val ball_rsp_tac = 

   881   Subgoal.FOCUS (fn {concl, ...} =>

   882      case (stripped_term_of concl) of

   883         (_ $ (Const (@{const_name Ball}, _) $ _) 

   884            $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1

   885       |_ => no_tac)

   886 *}

   887 

   888 ML {*

   889 val bex_rsp_tac = 

   890   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>

   891      case (stripped_term_of concl) of

   892         (_ $ (Const (@{const_name Bex}, _) $ _) 

   893            $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1

   894       | _ => no_tac)

   895 *}

   896 

   897 ML {* (* Legacy *)

   898 fun needs_lift (rty as Type (rty_s, _)) ty =

   899   case ty of

   900     Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys)

   901   | _ => false

   902 

   903 *}

   904 

   905 ML {*

   906 fun APPLY_RSP_TAC rty = 

   907   Subgoal.FOCUS (fn {concl, ...} =>

   908     case (stripped_term_of concl) of

   909        (_ $ (f $ _) $ (_ $ _)) =>

   910           let

   911             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});

   912             val insts = Thm.match (pat, concl)

   913           in

   914             if needs_lift rty (fastype_of f) 

   915             then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1

   916             else no_tac

   917           end

   918      | _ => no_tac)

   919 *}

   920 

   921 ML {*

   922 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)

   923 *}

   924 

   925 (*

   926 To prove that the regularised theorem implies the abs/rep injected, 

   927 we try:

   928 

   929  1) theorems 'trans2' from the appropriate QUOT_TYPE

   930  2) remove lambdas from both sides: lambda_res_tac

   931  3) remove Ball/Bex from the right hand side

   932  4) use user-supplied RSP theorems

   933  5) remove rep_abs from the right side

   934  6) reflexivity of equality

   935  7) split applications of lifted type (apply_rsp)

   936  8) split applications of non-lifted type (cong_tac)

   937  9) apply extentionality

   938  A) reflexivity of the relation

   939  B) assumption

   940     (Lambdas under respects may have left us some assumptions)

   941  C) proving obvious higher order equalities by simplifying fun_rel

   942     (not sure if it is still needed?)

   943  D) unfolding lambda on one side

   944  E) simplifying (= ===> =) for simpler respectfulness

   945 

   946 *)

   947 

   948 ML {*

   949 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =

   950   (FIRST' [

   951     (* "cong" rule of the of the relation / transitivity*)

   952     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)

   953     NDT ctxt "1" (resolve_tac trans2),

   954 

   955     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 

   956     NDT ctxt "2" (lambda_res_tac ctxt),

   957 

   958     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   959     NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),

   960 

   961     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)

   962     NDT ctxt "4" (ball_rsp_tac ctxt),

   963 

   964     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   965     NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),

   966 

   967     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)

   968     NDT ctxt "6" (bex_rsp_tac ctxt),

   969 

   970     (* respectfulness of constants *)

   971     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),

   972 

   973     (* reflexivity of operators arising from Cong_tac *)

   974     NDT ctxt "8" (rtac @{thm refl}),

   975 

   976     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)

   977     (* observe ---> *) 

   978     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 

   979                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),

   980 

   981     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)

   982     NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 

   983                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),

   984 

   985     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)

   986     (* merge with previous tactic *)

   987     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),

   988 

   989     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)

   990     NDT ctxt "C" (rtac @{thm ext}),

   991     

   992     (* reflexivity of the basic relations *)

   993     (* R \<dots> \<dots> *)

   994     NDT ctxt "D" (resolve_tac rel_refl),

   995 

   996     (* resolving with R x y assumptions *)

   997     NDT ctxt "E" (atac),

   998 

   999     (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)

  1000     

  1001     (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 

  1002     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 

  1003     (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)

  1004 

  1005     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)

  1006     (* global simplification *)

  1007     NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])

  1008 *}

  1009 

  1010 ML {*

  1011 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =

  1012   REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)

  1013 *}

  1014 

  1015 

  1016 section {* Cleaning of the theorem *}

  1017 

  1018 ML {*

  1019 fun applic_prs lthy absrep (rty, qty) =

  1020   let

  1021     fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;

  1022     fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;

  1023     val (raty, rgty) = Term.strip_type rty;

  1024     val (qaty, qgty) = Term.strip_type qty;

  1025     val vs = map (fn _ => "x") qaty;

  1026     val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;

  1027     val f = Free (fname, qaty ---> qgty);

  1028     val args = map Free (vfs ~~ qaty);

  1029     val rhs = list_comb(f, args);

  1030     val largs = map2 mk_rep (raty ~~ qaty) args;

  1031     val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));

  1032     val llhs = Syntax.check_term lthy lhs;

  1033     val eq = Logic.mk_equals (llhs, rhs);

  1034     val ceq = cterm_of (ProofContext.theory_of lthy') eq;

  1035     val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);

  1036     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)

  1037     val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;

  1038   in

  1039     singleton (ProofContext.export lthy' lthy) t_id

  1040   end

  1041 *}

  1042 

  1043 ML {*

  1044 fun find_aps_all rtm qtm =

  1045   case (rtm, qtm) of

  1046     (Abs(_, T1, s1), Abs(_, T2, s2)) =>

  1047       find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))

  1048   | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>

  1049       let

  1050         val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)

  1051       in

  1052         if T1 = T2 then sub else (T1, T2) :: sub

  1053       end

  1054   | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)

  1055   | _ => [];

  1056 

  1057 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)

  1058 *}

  1059 

  1060 ML {*

  1061 fun allex_prs_tac lthy quot =

  1062   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})

  1063   THEN' (quotient_tac quot)

  1064 *}

  1065 

  1066 (* Rewrites the term with LAMBDA_PRS thm.

  1067 

  1068 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))

  1069     with: f

  1070 

  1071 It proves the QUOTIENT assumptions by calling quotient_tac

  1072  *)

  1073 ML {*

  1074 fun make_inst lhs t =

  1075   let

  1076     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

  1077     val _ $ (Abs (_, _, g)) = t;

  1078     fun mk_abs i t =

  1079       if incr_boundvars i u aconv t then Bound i

  1080       else (case t of

  1081         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

  1082       | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')

  1083       | Bound j => if i = j then error "make_inst" else t

  1084       | _ => t);

  1085   in (f, Abs ("x", T, mk_abs 0 g)) end;

  1086 

  1087 fun lambda_prs_conv1 ctxt quot_thms ctrm =

  1088   case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>

  1089   let

  1090     val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);

  1091     val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);

  1092     val thy = ProofContext.theory_of ctxt;

  1093     val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]

  1094     val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];

  1095     val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]

  1096     val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};

  1097     val tac =

  1098       (compose_tac (false, lpi, 2)) THEN_ALL_NEW

  1099       (quotient_tac quot_thms);

  1100     val gc = Drule.strip_imp_concl (cprop_of lpi);

  1101     val t = Goal.prove_internal [] gc (fn _ => tac 1)

  1102     val te = @{thm eq_reflection} OF [t]

  1103     val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te

  1104     val tl = Thm.lhs_of ts;

  1105     val (insp, inst) = make_inst (term_of tl) (term_of ctrm);

  1106     val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;

  1107 (*    val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)

  1108   in

  1109     Conv.rewr_conv ti ctrm

  1110   end

  1111 *}

  1112 

  1113 (* quot stands for the QUOTIENT theorems: *)

  1114 (* could be potentially all of them       *)

  1115 ML {*

  1116 fun lambda_prs_conv ctxt quot ctrm =

  1117   case (term_of ctrm) of

  1118     (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>

  1119       (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)

  1120       then_conv (lambda_prs_conv1 ctxt quot)) ctrm

  1121   | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm

  1122   | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm

  1123   | _ => Conv.all_conv ctrm

  1124 *}

  1125 

  1126 ML {*

  1127 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>

  1128   CONVERSION

  1129     (Conv.params_conv ~1 (fn ctxt =>

  1130        (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv

  1131           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)

  1132 *}

  1133 

  1134 ML {*

  1135 fun clean_tac lthy quot defs aps =