1 (* Code for getting the goal *)

     2 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

     3 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}

     4 

     5 

     6 section {*  Infrastructure about definitions *}

     7 

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

     9 ML {*

    10 fun eqsubst_thm ctxt thms thm =

    11   let

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

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

    14       NONE => error "eqsubst_thm"

    15     | SOME th => cprem_of th 1

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

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

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

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

    20   in

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

    22   end

    23 *}

    24 

    25 (* expects atomized definitions *)

    26 ML {*

    27 fun add_lower_defs_aux lthy thm =

    28   let

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

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

    31     val g = simp_ids f

    32   in

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

    34   end

    35   handle _ => [simp_ids thm]

    36 *}

    37 

    38 ML {*

    39 fun add_lower_defs lthy def =

    40   let

    41     val def_pre_sym = symmetric def

    42     val def_atom = atomize_thm def_pre_sym

    43     val defs_all = add_lower_defs_aux lthy def_atom

    44   in

    45     map Thm.varifyT defs_all

    46   end

    47 *}

    48 

    49 

    50 

    51 ML {*

    52 fun repeat_eqsubst_thm ctxt thms thm =

    53   repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)

    54   handle _ => thm

    55 *}

    56 

    57 

    58 ML {*

    59 fun eqsubst_prop ctxt thms t =

    60   let

    61     val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)

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

    63       NONE => error "eqsubst_prop"

    64     | SOME th => cprem_of th 1

    65   in term_of a' end

    66 *}

    67 

    68 ML {*

    69   fun repeat_eqsubst_prop ctxt thms t =

    70     repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)

    71     handle _ => t

    72 *}

    73 

    74 

    75 text {* tyRel takes a type and builds a relation that a quantifier over this

    76   type needs to respect. *}

    77 ML {*

    78 fun tyRel ty rty rel lthy =

    79   if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)

    80   then rel

    81   else (case ty of

    82           Type (s, tys) =>

    83             let

    84               val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;

    85               val ty_out = ty --> ty --> @{typ bool};

    86               val tys_out = tys_rel ---> ty_out;

    87             in

    88             (case (maps_lookup (ProofContext.theory_of lthy) s) of

    89                SOME (info) => list_comb (Const (#relfun info, tys_out),

    90                               map (fn ty => tyRel ty rty rel lthy) tys)

    91              | NONE  => HOLogic.eq_const ty

    92             )

    93             end

    94         | _ => HOLogic.eq_const ty)

    95 *}

    96 

    97 (* 

    98 ML {* cterm_of @{theory} 

    99   (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 

   100          @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 

   101 *} 

   102 *)

   103 

   104 

   105 ML {*

   106 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)

   107 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})

   108 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})

   109 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})

   110 *}

   111 

   112 (* applies f to the subterm of an abstractions, otherwise to the given term *)

   113 ML {*

   114 fun apply_subt f trm =

   115   case trm of

   116     Abs (x, T, t) => 

   117        let 

   118          val (x', t') = Term.dest_abs (x, T, t)

   119        in

   120          Term.absfree (x', T, f t') 

   121        end

   122   | _ => f trm

   123 *}

   124 

   125 

   126 

   127 (* FIXME: if there are more than one quotient, then you have to look up the relation *)

   128 ML {*

   129 fun my_reg lthy rel rty trm =

   130   case trm of

   131     Abs (x, T, t) =>

   132        if (needs_lift rty T) then

   133          let

   134             val rrel = tyRel T rty rel lthy

   135          in

   136            (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)

   137          end

   138        else

   139          Abs(x, T, (apply_subt (my_reg lthy rel rty) t))

   140   | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>

   141        let

   142           val ty1 = domain_type ty

   143           val ty2 = domain_type ty1

   144           val rrel = tyRel T rty rel lthy

   145        in

   146          if (needs_lift rty T) then

   147            (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

   148          else

   149            Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t

   150        end

   151   | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>

   152        let

   153           val ty1 = domain_type ty

   154           val ty2 = domain_type ty1

   155           val rrel = tyRel T rty rel lthy

   156        in

   157          if (needs_lift rty T) then

   158            (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)

   159          else

   160            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t

   161        end

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

   163       if needs_lift rty (fastype_of t) then

   164         (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)

   165       else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)

   166   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)

   167   | _ => trm

   168 *}

   169 

   170 (* For polymorphic types we need to find the type of the Relation term. *)

   171 (* TODO: we assume that the relation is a Constant. Is this always true? *)

   172 ML {*

   173 fun my_reg_inst lthy rel rty trm =

   174   case rel of

   175     Const (n, _) => Syntax.check_term lthy

   176       (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)

   177 *}

   178 

   179 (*

   180 ML {*

   181   val r = Free ("R", dummyT);

   182   val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});

   183   val t2 = Syntax.check_term @{context} t;

   184   cterm_of @{theory} t2

   185 *}

   186 *)

   187 

   188 text {* Assumes that the given theorem is atomized *}

   189 ML {*

   190   fun build_regularize_goal thm rty rel lthy =

   191      Logic.mk_implies

   192        ((prop_of thm),

   193        (my_reg_inst lthy rel rty (prop_of thm)))

   194 *}

   195 

   196 ML {*

   197 fun regularize thm rty rel rel_eqv rel_refl lthy =

   198   let

   199     val goal = build_regularize_goal thm rty rel lthy;

   200     fun tac ctxt =

   201       (ObjectLogic.full_atomize_tac) THEN'

   202       REPEAT_ALL_NEW (FIRST' [

   203         rtac rel_refl,

   204         atac,

   205         rtac @{thm universal_twice},

   206         (rtac @{thm impI} THEN' atac),

   207         rtac @{thm implication_twice},

   208         EqSubst.eqsubst_tac ctxt [0]

   209           [(@{thm equiv_res_forall} OF [rel_eqv]),

   210            (@{thm equiv_res_exists} OF [rel_eqv])],

   211         (* For a = b \<longrightarrow> a \<approx> b *)

   212         (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),

   213         (rtac @{thm RIGHT_RES_FORALL_REGULAR})

   214       ]);

   215     val cthm = Goal.prove lthy [] [] goal

   216       (fn {context, ...} => tac context 1);

   217   in

   218     cthm OF [thm]

   219   end

   220 *}

   221 

   222 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

   223 axioms Rl_eq: "EQUIV Rl"

   224 

   225 quotient ql = "'a list" / "Rl"

   226   by (rule Rl_eq)

   227 ML {*

   228   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});

   229   ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})

   230 *}

   231 *)

   232 

   233 ML {*

   234 (* returns all subterms where two types differ *)

   235 fun diff (T, S) Ds =

   236   case (T, S) of

   237     (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 

   238   | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds

   239   | (Type (a, Ts), Type (b, Us)) => 

   240       if a = b then diffs (Ts, Us) Ds else (T, S)::Ds

   241   | _ => (T, S)::Ds

   242 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)

   243   | diffs ([], []) Ds = Ds

   244   | diffs _ _ = error "Unequal length of type arguments"

   245 

   246 *}

   247 

   248 ML {*

   249 fun build_repabs_term lthy thm consts rty qty =

   250   let

   251     (* TODO: The rty and qty stored in the quotient_info should

   252        be varified, so this will soon not be needed *)

   253     val rty = Logic.varifyT rty;

   254     val qty = Logic.varifyT qty;

   255 

   256   fun mk_abs tm =

   257     let

   258       val ty = fastype_of tm

   259     in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end

   260   fun mk_repabs tm =

   261     let

   262       val ty = fastype_of tm

   263     in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end

   264 

   265     fun is_lifted_const (Const (x, _)) = member (op =) consts x

   266       | is_lifted_const _ = false;

   267 

   268     fun build_aux lthy tm =

   269       case tm of

   270         Abs (a as (_, vty, _)) =>

   271           let

   272             val (vs, t) = Term.dest_abs a;

   273             val v = Free(vs, vty);

   274             val t' = lambda v (build_aux lthy t)

   275           in

   276             if (not (needs_lift rty (fastype_of tm))) then t'

   277             else mk_repabs (

   278               if not (needs_lift rty vty) then t'

   279               else

   280                 let

   281                   val v' = mk_repabs v;

   282                   (* TODO: I believe 'beta' is not needed any more *)

   283                   val t1 = (* Envir.beta_norm *) (t' $ v')

   284                 in

   285                   lambda v t1

   286                 end)

   287           end

   288       | x =>

   289         case Term.strip_comb tm of

   290           (Const(@{const_name Respects}, _), _) => tm

   291         | (opp, tms0) =>

   292           let

   293             val tms = map (build_aux lthy) tms0

   294             val ty = fastype_of tm

   295           in

   296             if (is_lifted_const opp andalso needs_lift rty ty) then

   297             mk_repabs (list_comb (opp, tms))

   298             else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then

   299               mk_repabs (list_comb (opp, tms))

   300             else if tms = [] then opp

   301             else list_comb(opp, tms)

   302           end

   303   in

   304     repeat_eqsubst_prop lthy @{thms id_def_sym}

   305       (build_aux lthy (Thm.prop_of thm))

   306   end

   307 *}

   308 

   309 text {* Builds provable goals for regularized theorems *}

   310 ML {*

   311 fun build_repabs_goal ctxt thm cons rty qty =

   312   Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))

   313 *}

   314 

   315 ML {*

   316 fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =

   317   let

   318     val rt = build_repabs_term lthy thm consts rty qty;

   319     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);

   320     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

   321       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));

   322     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

   323   in

   324     @{thm Pure.equal_elim_rule1} OF [cthm, thm]

   325   end

   326 *}

   327 

   328 

   329 (* TODO: Check if it behaves properly with varifyed rty *)

   330 ML {*

   331 fun findabs_all rty tm =

   332   case tm of

   333     Abs(_, T, b) =>

   334       let

   335         val b' = subst_bound ((Free ("x", T)), b);

   336         val tys = findabs_all rty b'

   337         val ty = fastype_of tm

   338       in if needs_lift rty ty then (ty :: tys) else tys

   339       end

   340   | f $ a => (findabs_all rty f) @ (findabs_all rty a)

   341   | _ => [];

   342 fun findabs rty tm = distinct (op =) (findabs_all rty tm)

   343 *}

   344 

   345 

   346 (* Currently useful only for LAMBDA_PRS *)

   347 ML {*

   348 fun make_simp_prs_thm lthy quot_thm thm typ =

   349   let

   350     val (_, [lty, rty]) = dest_Type typ;

   351     val thy = ProofContext.theory_of lthy;

   352     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)

   353     val inst = [SOME lcty, NONE, SOME rcty];

   354     val lpi = Drule.instantiate' inst [] thm;

   355     val tac =

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

   357       (quotient_tac quot_thm);

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

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

   360   in

   361     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t

   362   end

   363 *}

   364 

   365 ML {*

   366 fun findallex_all rty qty tm =

   367   case tm of

   368     Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>

   369       let

   370         val (tya, tye) = findallex_all rty qty s

   371       in if needs_lift rty T then

   372         ((T :: tya), tye)

   373       else (tya, tye) end

   374   | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>

   375       let

   376         val (tya, tye) = findallex_all rty qty s

   377       in if needs_lift rty T then

   378         (tya, (T :: tye))

   379       else (tya, tye) end

   380   | Abs(_, T, b) =>

   381       findallex_all rty qty (subst_bound ((Free ("x", T)), b))

   382   | f $ a =>

   383       let

   384         val (a1, e1) = findallex_all rty qty f;

   385         val (a2, e2) = findallex_all rty qty a;

   386       in (a1 @ a2, e1 @ e2) end

   387   | _ => ([], []);

   388 *}

   389 

   390 ML {*

   391 fun findallex lthy rty qty tm =

   392   let

   393     val (a, e) = findallex_all rty qty tm;

   394     val (ad, ed) = (map domain_type a, map domain_type e);

   395     val (au, eu) = (distinct (op =) ad, distinct (op =) ed);

   396     val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)

   397   in

   398     (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)

   399   end

   400 *}

   401 

   402 ML {*

   403 fun make_allex_prs_thm lthy quot_thm thm typ =

   404   let

   405     val (_, [lty, rty]) = dest_Type typ;

   406     val thy = ProofContext.theory_of lthy;

   407     val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)

   408     val inst = [NONE, SOME lcty];

   409     val lpi = Drule.instantiate' inst [] thm;

   410     val tac =

   411       (compose_tac (false, lpi, 1)) THEN_ALL_NEW

   412       (quotient_tac quot_thm);

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

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

   415     val t_noid = MetaSimplifier.rewrite_rule

   416       [@{thm eq_reflection} OF @{thms id_apply}] t;

   417     val t_sym = @{thm "HOL.sym"} OF [t_noid];

   418     val t_eq = @{thm "eq_reflection"} OF [t_sym]

   419   in

   420     t_eq

   421   end

   422 *}

   423 

   424 ML {*

   425 fun lift_thm lthy qty qty_name rsp_thms defs rthm = 

   426 let

   427   val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))

   428 

   429   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

   430   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

   431   val consts = lookup_quot_consts defs;

   432   val t_a = atomize_thm rthm;

   433 

   434   val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

   435 

   436   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;

   437 

   438   val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

   439 

   440   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;

   441 

   442   val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))

   443 

   444   val (alls, exs) = findallex lthy rty qty (prop_of t_a);

   445   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

   446   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

   447   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

   448 

   449   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))

   450 

   451   val abs = findabs rty (prop_of t_a);

   452   val aps = findaps rty (prop_of t_a);

   453   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;

   454   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;

   455   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;

   456   

   457   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))

   458 

   459   val defs_sym = flat (map (add_lower_defs lthy) defs);

   460   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

   461   val t_id = simp_ids lthy t_l;

   462 

   463   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))

   464 

   465   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

   466 

   467   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))

   468 

   469   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

   470 

   471   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))

   472 

   473   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

   474 

   475   val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))

   476 

   477   val t_rv = ObjectLogic.rulify t_r

   478 

   479   val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))

   480 in

   481   Thm.varifyT t_rv

   482 end

   483 *}

   484 

   485 ML {*

   486 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =

   487   let

   488     val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;

   489     val (_, lthy2) = note (name, lifted_thm) lthy;

   490   in

   491     lthy2

   492   end

   493 *}

   494 

   495 

   496 ML {*

   497 fun regularize_goal lthy thm rel_eqv rel_refl qtrm =

   498   let

   499     val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;

   500     fun tac lthy = regularize_tac lthy rel_eqv rel_refl;

   501     val cthm = Goal.prove lthy [] [] reg_trm

   502       (fn {context, ...} => tac context 1);

   503   in

   504     cthm OF [thm]

   505   end

   506 *}

   507 

   508 ML {*

   509 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =

   510   let

   511     val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));

   512     fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'

   513       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));

   514     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);

   515   in

   516     @{thm Pure.equal_elim_rule1} OF [cthm, thm]

   517   end

   518 *}

   519 

   520 

   521 ML {*

   522 fun atomize_goal thy gl =

   523   let

   524     val vars = map Free (Term.add_frees gl []);

   525     val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;

   526     fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;

   527     val glv = fold lambda_all vars gl

   528     val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))

   529     val glf = Type.legacy_freeze gla

   530   in

   531     if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf

   532   end

   533 *}

   534 

   535 

   536 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}

   537 ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}

   538 

   539 

   540 ML {*

   541 fun applic_prs lthy absrep (rty, qty) =

   542   let

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

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

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

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

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

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

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

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

   551     val rhs = list_comb(f, args);

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

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

   554     val llhs = Syntax.check_term lthy lhs;

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

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

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

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

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

   560   in

   561     singleton (ProofContext.export lthy' lthy) t_id

   562   end

   563 *}

   564 

   565 ML {*

   566 fun find_aps_all rtm qtm =

   567   case (rtm, qtm) of

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

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

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

   571       let

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

   573       in

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

   575       end

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

   577   | _ => [];

   578 

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

   580 *}

   581 

   582 

   583 

   584 ML {*

   585 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =

   586 let

   587   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

   588   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

   589   val t_a = atomize_thm rthm;

   590   val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;

   591   val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;

   592   val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;

   593   val (alls, exs) = findallex lthy rty qty (prop_of t_a);

   594   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls

   595   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs

   596   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t

   597   val abs = findabs rty (prop_of t_a);

   598   val aps = findaps rty (prop_of t_a);

   599   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;

   600   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;

   601   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;

   602   val defs_sym = flat (map (add_lower_defs lthy) defs);

   603   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;

   604   val t_id = simp_ids lthy t_l;

   605   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;

   606   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;

   607   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;

   608   val t_rv = ObjectLogic.rulify t_r

   609 in

   610   Thm.varifyT t_rv

   611 end

   612 *}

   613 

   614 ML {*

   615 fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =

   616   let

   617     val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;

   618     val (_, lthy2) = note (name, lifted_thm) lthy;

   619   in

   620     lthy2

   621   end

   622 *}

   623 

   624 ML {*

   625 fun simp_ids_trm trm =

   626   trm |>

   627   MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}

   628   |> cprop_of |> Thm.dest_equals |> snd

   629 

   630 *}

   631 

   632 (* Unused part of the locale *)

   633 

   634 lemma R_trans:

   635   assumes ab: "R a b"

   636   and     bc: "R b c"

   637   shows "R a c"

   638 proof -

   639   have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp

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

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

   642   ultimately show "R a c" unfolding transp_def by blast

   643 qed

   644 

   645 lemma R_sym:

   646   assumes ab: "R a b"

   647   shows "R b a"

   648 proof -

   649   have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp

   650   then show "R b a" using ab unfolding symp_def by blast

   651 qed

   652 

   653 lemma R_trans2:

   654   assumes ac: "R a c"

   655   and     bd: "R b d"

   656   shows "R a b = R c d"

   657 using ac bd

   658 by (blast intro: R_trans R_sym)

   659 

   660 lemma REPS_same:

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

   662 proof -

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

   664   proof

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

   666     from rep_prop

   667     obtain x y

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

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

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

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

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

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

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

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

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

   677   next

   678     assume ab: "a = b"

   679     have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp

   680     then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto

   681   qed

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

   683 qed

   684 

   685 

   686 

   687