204 section {* RepAbs injection *}

   204 section {* infrastructure about id *}

   205 (*

   206 

   207 To prove that the old theorem implies the new one, we first

   208 atomize it and then try:

   209 

   210  1) theorems 'trans2' from the appropriate QUOT_TYPE

   211  2) remove lambdas from both sides (LAMBDA_RES_TAC)

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

   213  4) use user-supplied RSP theorems

   214  5) remove rep_abs from the right side

   215  6) reflexivity of equality

   216  7) split applications of lifted type (apply_rsp)

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

   218  9) apply extentionality

   219 10) reflexivity of the relation

   220 11) assumption

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

   222 12) proving obvious higher order equalities by simplifying fun_rel

   223     (not sure if it is still needed?)

   224 13) unfolding lambda on one side

   225 14) simplifying (= ===> =) for simpler respectfullness

   226 

   227 *)

   228 

   229 

   380 text {* Does the same as 'subst' in a given prop or theorem *}

   227 section {* Does the same as 'subst' in a given theorem *}

   422 ML {*

   271 section {* infrastructure about collecting theorems for calling lifting *}

   423 fun findaps_all rty tm =

   424   case tm of

   425     Abs(_, T, b) =>

   426       findaps_all rty (subst_bound ((Free ("x", T)), b))

   427   | (f $ a) => (findaps_all rty f @ findaps_all rty a)

   428   | Free (_, (T as (Type ("fun", (_ :: _))))) =>

   429       (if needs_lift rty T then [T] else [])

   430   | _ => [];

   431 fun findaps rty tm = distinct (op =) (findaps_all rty tm)

   432 *}

   433 

   434 

   435 

   436 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

   437 ML {*

   438 fun exchange_ty lthy rty qty ty =

   439   let

   440     val thy = ProofContext.theory_of lthy

   441   in

   442     if Sign.typ_instance thy (ty, rty) then

   443       let

   444         val inst = Sign.typ_match thy (rty, ty) Vartab.empty

   445       in

   446         Envir.subst_type inst qty

   447       end

   448     else

   449       let

   450         val (s, tys) = dest_Type ty

   451       in

   452         Type (s, map (exchange_ty lthy rty qty) tys)

   453       end

   454   end

   455   handle TYPE _ => ty (* for dest_Type *)

   456 *}

   457 

   458 

   459 ML {*

   460 fun find_matching_types rty ty =

   461   if Type.raw_instance (Logic.varifyT ty, rty)

   462   then [ty]

   463   else

   464     let val (s, tys) = dest_Type ty in

   465     flat (map (find_matching_types rty) tys)

   466     end

   467     handle TYPE _ => []

   468 *}

   469 

   470 ML {*

   471 fun negF absF = repF

   472   | negF repF = absF

   473 

   474 fun get_fun flag qenv lthy ty =

   475 let

   476   

   477   fun get_fun_aux s fs =

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

   479       SOME info => list_comb (Const (#mapfun info, dummyT), fs)

   480     | NONE      => error ("no map association for type " ^ s))

   481 

   482   fun get_const flag qty =

   483   let 

   484     val thy = ProofContext.theory_of lthy

   485     val qty_name = Long_Name.base_name (fst (dest_Type qty))

   486   in

   487     case flag of

   488       absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)

   489     | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)

   490   end

   491 

   492   fun mk_identity ty = Abs ("", ty, Bound 0)

   493 

   494 in

   495   if (AList.defined (op=) qenv ty)

   496   then (get_const flag ty)

   497   else (case ty of

   498           TFree _ => mk_identity ty

   499         | Type (_, []) => mk_identity ty 

   500         | Type ("fun" , [ty1, ty2]) => 

   501             let

   502               val fs_ty1 = get_fun (negF flag) qenv lthy ty1

   503               val fs_ty2 = get_fun flag qenv lthy ty2

   504             in  

   505               get_fun_aux "fun" [fs_ty1, fs_ty2]

   506             end 

   507         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)

   508         | _ => error ("no type variables allowed"))

   509 end

   510 *}

   511 

   512 ML {*

   513 fun get_fun_OLD flag (rty, qty) lthy ty =

   514   let

   515     val tys = find_matching_types rty ty;

   516     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;

   517     val xchg_ty = exchange_ty lthy rty qty ty

   518   in

   519     get_fun flag qenv lthy xchg_ty

   520   end

   521 *}

   522 

   523 ML {*

   524 fun applic_prs lthy rty qty absrep ty =

   525   let

   526     val rty = Logic.varifyT rty;

   527     val qty = Logic.varifyT qty;

   528     fun absty ty =

   529       exchange_ty lthy rty qty ty

   530     fun mk_rep tm =

   531       let

   532         val ty = exchange_ty lthy qty rty (fastype_of tm)

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

   534     fun mk_abs tm =

   535       let

   536         val ty = fastype_of tm

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

   538     val (l, ltl) = Term.strip_type ty;

   539     val nl = map absty l;

   540     val vs = map (fn _ => "x") l;

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

   542     val args = map Free (vfs ~~ nl);

   543     val lhs = list_comb((Free (fname, nl ---> ltl)), args);

   544     val rargs = map mk_rep args;

   545     val f = Free (fname, nl ---> ltl);

   546     val rhs = mk_abs (list_comb((mk_rep f), rargs));

   547     val eq = Logic.mk_equals (rhs, lhs);

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

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

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

   551     val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;

   552   in

   553     singleton (ProofContext.export lthy' lthy) t_id

   554   end

   555 *}

   950 

   666 section {* RepAbs injection tactic *}

   951 (* Genralisation of free variables in a goal *)

   667 (*

   952 

   668 

   953 ML {*

   669 To prove that the regularised theorem implies the abs/rep injected, we first

   954 fun inst_spec ctrm =

   670 atomize it and then try:

   671 

   672  1) theorems 'trans2' from the appropriate QUOT_TYPE

   673  2) remove lambdas from both sides (LAMBDA_RES_TAC)

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

   675  4) use user-supplied RSP theorems

   676  5) remove rep_abs from the right side

   677  6) reflexivity of equality

   678  7) split applications of lifted type (apply_rsp)

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

   680  9) apply extentionality

   681 10) reflexivity of the relation

   682 11) assumption

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

   684 12) proving obvious higher order equalities by simplifying fun_rel

   685     (not sure if it is still needed?)

   686 13) unfolding lambda on one side

   687 14) simplifying (= ===> =) for simpler respectfullness

   688 

   689 *)

   690 

   691 ML {*

   692 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>

   693   let

   694     val pat = Drule.strip_imp_concl (cprop_of thm)

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

   696   in

   697     rtac (Drule.instantiate insts thm) 1

   698   end

   699   handle _ => no_tac)

   700 *}

   701 

   702 ML {*

   703 fun CHANGED' tac = (fn i => CHANGED (tac i))

   704 *}

   705 

   706 ML {*

   707 fun quotient_tac quot_thm =

   708   REPEAT_ALL_NEW (FIRST' [

   709     rtac @{thm FUN_QUOTIENT},

   710     rtac quot_thm,

   711     rtac @{thm IDENTITY_QUOTIENT},

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

   713     CHANGED' (

   714       (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}

   715       )))

   716   ])

   717 *}

   718 

   719 ML {*

   720 fun LAMBDA_RES_TAC ctxt i st =

   721   (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of

   722     (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>

   723       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'

   724       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})

   725   | _ => fn _ => no_tac) i st

   726 *}

   727 

   728 ML {*

   729 fun WEAK_LAMBDA_RES_TAC ctxt i st =

   730   (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of

   731     (_ $ (_ $ _ $ (Abs(_, _, _)))) =>

   732       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'

   733       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})

   734   | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>

   735       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'

   736       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})

   737   | _ => fn _ => no_tac) i st

   738 *}

   739 

   740 ML {* (* Legacy *)

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

   742   case ty of

   743     Type (s, tys) =>

   744       (s = rty_s) orelse (exists (needs_lift rty) tys)

   745   | _ => false

   746 

   747 *}

   748 

   749 ML {*

   750 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>

   751   let

   752     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;

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

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

   755   in

   756     if needs_lift rty (type_of f) then

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

   758     else no_tac

   759   end

   760   handle _ => no_tac)

   761 *}

   762 

   763 ML {*

   764 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>

   765   let

   766     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $

   767                  (Const (@{const_name Ball}, _) $ _)) = term_of concl

   768   in

   769     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))

   770     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}

   771     THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'

   772     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1

   773   end

   774   handle _ => no_tac)

   775 *}

   776 

   777 ML {*

   778 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>

   779   let

   780     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $

   781                  (Const (@{const_name Bex}, _) $ _)) = term_of concl

   782   in

   783     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))

   784     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}

   785     THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'

   786     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1

   787   end

   788   handle _ => no_tac)

   789 *}

   790 

   791 ML {*

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

   793 *}

   794 

   795 ML {*

   796 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =

   797   (FIRST' [

   798     rtac trans_thm,

   799     LAMBDA_RES_TAC ctxt,

   800     ball_rsp_tac ctxt,

   801     bex_rsp_tac ctxt,

   802     FIRST' (map rtac rsp_thms),

   803     rtac refl,

   804     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),

   805     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),

   806     Cong_Tac.cong_tac @{thm cong},

   807     rtac @{thm ext},

   808     rtac reflex_thm,

   809     atac,

   810     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),

   811     WEAK_LAMBDA_RES_TAC ctxt,

   812     CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))

   813     ])

   814 *}

   815 

   816 

   817 (****************************************)

   818 (* cleaning of the theorem              *)

   819 (****************************************)

   820 

   821 

   822 

   823 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

   824 ML {*

   825 fun exchange_ty lthy rty qty ty =

   826   let

   827     val thy = ProofContext.theory_of lthy

   828   in

   829     if Sign.typ_instance thy (ty, rty) then

   830       let

   831         val inst = Sign.typ_match thy (rty, ty) Vartab.empty

   832       in

   833         Envir.subst_type inst qty

   834       end

   835     else

   836       let

   837         val (s, tys) = dest_Type ty

   838       in

   839         Type (s, map (exchange_ty lthy rty qty) tys)

   840       end

   841   end

   842   handle TYPE _ => ty (* for dest_Type *)

   843 *}

   844 

   845 

   846 ML {*

   847 fun find_matching_types rty ty =

   848   if Type.raw_instance (Logic.varifyT ty, rty)

   849   then [ty]

   850   else

   851     let val (s, tys) = dest_Type ty in

   852     flat (map (find_matching_types rty) tys)

   853     end

   854     handle TYPE _ => []

   855 *}

   856 

   857 ML {*

   858 fun negF absF = repF

   859   | negF repF = absF

   860 

   861 fun get_fun flag qenv lthy ty =

   956    val cty = ctyp_of_term ctrm

   863   

   864   fun get_fun_aux s fs =

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

   866       SOME info => list_comb (Const (#mapfun info, dummyT), fs)

   867     | NONE      => error ("no map association for type " ^ s))

   868 

   869   fun get_const flag qty =

   870   let 

   871     val thy = ProofContext.theory_of lthy

   872     val qty_name = Long_Name.base_name (fst (dest_Type qty))

   873   in

   874     case flag of

   875       absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)

   876     | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)

   877   end

   878 

   879   fun mk_identity ty = Abs ("", ty, Bound 0)

   880 

   958    Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}

   882   if (AList.defined (op=) qenv ty)

   883   then (get_const flag ty)

   884   else (case ty of

   885           TFree _ => mk_identity ty

   886         | Type (_, []) => mk_identity ty 

   887         | Type ("fun" , [ty1, ty2]) => 

   888             let

   889               val fs_ty1 = get_fun (negF flag) qenv lthy ty1

   890               val fs_ty2 = get_fun flag qenv lthy ty2

   891             in  

   892               get_fun_aux "fun" [fs_ty1, fs_ty2]

   893             end 

   894         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)

   895         | _ => error ("no type variables allowed"))

   960 

   897 *}

   961 fun inst_spec_tac ctrms =

   898 

   962   EVERY' (map (dtac o inst_spec) ctrms)

   899 ML {*

   963 

   900 fun get_fun_OLD flag (rty, qty) lthy ty =

   964 fun abs_list (xs, t) = 

   901   let

   965   fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t

   902     val tys = find_matching_types rty ty;

   966 

   903     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;

   967 fun gen_frees_tac ctxt =

   904     val xchg_ty = exchange_ty lthy rty qty ty

   968  SUBGOAL (fn (concl, i) =>

   905   in

   969   let

   906     get_fun flag qenv lthy xchg_ty

   970     val thy = ProofContext.theory_of ctxt

   907   end

   971     val concl' = HOLogic.dest_Trueprop concl

   908 *}

   972     val vrs = Term.add_frees concl' []

   909 

   973     val cvrs = map (cterm_of thy o Free) vrs

   910 ML {*

   974     val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))

   911 fun applic_prs lthy rty qty absrep ty =

   975     val goal = Logic.mk_implies (concl'', concl)

   912   let

   976     val rule = Goal.prove ctxt [] [] goal 

   913     val rty = Logic.varifyT rty;

   977       (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))

   914     val qty = Logic.varifyT qty;

   978   in

   915     fun absty ty =

   979     rtac rule i

   916       exchange_ty lthy rty qty ty

   980   end)  

   917     fun mk_rep tm =

   981 *}

   918       let

   982 

   919         val ty = exchange_ty lthy qty rty (fastype_of tm)

   983 (* General outline of the lifting procedure *)

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

   984 (* **************************************** *)

   921     fun mk_abs tm =

   985 (*                                          *)

   922       let

   986 (* - A is the original raw theorem          *)

   923         val ty = fastype_of tm

   987 (* - B is the regularized theorem           *)

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

   988 (* - C is the rep/abs injected version of B *) 

   925     val (l, ltl) = Term.strip_type ty;

   989 (* - D is the lifted theorem                *)

   926     val nl = map absty l;

   990 (*                                          *)

   927     val vs = map (fn _ => "x") l;

   991 (* - b is the regularization step           *)

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

   992 (* - c is the rep/abs injection step        *)

   929     val args = map Free (vfs ~~ nl);

   993 (* - d is the cleaning part                 *)

   930     val lhs = list_comb((Free (fname, nl ---> ltl)), args);

   994 

   931     val rargs = map mk_rep args;

   995 lemma procedure:

   932     val f = Free (fname, nl ---> ltl);

   996   assumes a: "A"

   933     val rhs = mk_abs (list_comb((mk_rep f), rargs));

   997   and     b: "A \<Longrightarrow> B"

   934     val eq = Logic.mk_equals (rhs, lhs);

   998   and     c: "B = C"

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

   999   and     d: "C = D"

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

  1000   shows   "D"

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

  1001   using a b c d

   938     val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;

  1002   by simp

   939   in

  1003 

   940     singleton (ProofContext.export lthy' lthy) t_id

  1004 ML {*

   941   end

  1005 fun lift_error ctxt fun_str rtrm qtrm =

   942 *}

  1006 let

   943 

  1007   val rtrm_str = Syntax.string_of_term ctxt rtrm

   944 

  1008   val qtrm_str = Syntax.string_of_term ctxt qtrm

   945 ML {*

  1009   val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 

   946 fun findaps_all rty tm =

  1010              "and the lifted theorem", rtrm_str, "do not match"]

   947   case tm of

  1011 in

   948     Abs(_, T, b) =>

  1012   error (space_implode " " msg)

   949       findaps_all rty (subst_bound ((Free ("x", T)), b))

  1013 end

   950   | (f $ a) => (findaps_all rty f @ findaps_all rty a)

  1014 *}

   951   | Free (_, (T as (Type ("fun", (_ :: _))))) =>

  1015 

   952       (if needs_lift rty T then [T] else [])

  1016 ML {* 

   953   | _ => [];

  1017 fun procedure_inst ctxt rtrm qtrm =

   954 fun findaps rty tm = distinct (op =) (findaps_all rty tm)

  1018 let

   955 *}

  1019   val thy = ProofContext.theory_of ctxt

  1020   val rtrm' = HOLogic.dest_Trueprop rtrm

  1021   val qtrm' = HOLogic.dest_Trueprop qtrm

  1022   val reg_goal = 

  1023         Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')

  1024         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm

  1025   val inj_goal = 

  1026         Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))

  1027         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm

  1028 in

  1029   Drule.instantiate' []

  1030     [SOME (cterm_of thy rtrm'),

  1031      SOME (cterm_of thy reg_goal),

  1032      SOME (cterm_of thy inj_goal)]

  1033   @{thm procedure}

  1034 end

  1035 *}

  1036   

  1037 ML {*

  1038 fun procedure_tac rthm ctxt =

  1039   ObjectLogic.full_atomize_tac 

  1040   THEN' gen_frees_tac ctxt

  1041   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>

  1042           let

  1043             val rthm' = atomize_thm rthm

  1044             val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))

  1045           in

  1046            EVERY1 [rtac rule, rtac rthm']

  1047         end) ctxt

  1048 *}

  1049 

  1125     (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>

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

  1150     TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'

  1055     EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), 

  1151     TRY' (lambda_prs_tac lthy quot) THEN'

  1056             lambda_prs_tac lthy quot,

  1152     TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'

  1057             (* TODO: cleaning according to app_prs *)

  1153     simp_tac (HOL_ss addsimps [reps_same])

  1058             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),

  1154   end

  1059             simp_tac (HOL_ss addsimps [reps_same])]

  1060   end

  1061 *}

  1062 

  1063 (* Genralisation of free variables in a goal *)

  1064 

  1065 ML {*

  1066 fun inst_spec ctrm =

  1067 let

  1068    val cty = ctyp_of_term ctrm

  1069 in

  1070    Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}

  1071 end

  1072 

  1073 fun inst_spec_tac ctrms =

  1074   EVERY' (map (dtac o inst_spec) ctrms)

  1075 

  1076 fun abs_list (xs, t) = 

  1077   fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t

  1078 

  1079 fun gen_frees_tac ctxt =

  1080  SUBGOAL (fn (concl, i) =>

  1081   let

  1082     val thy = ProofContext.theory_of ctxt

  1083     val concl' = HOLogic.dest_Trueprop concl

  1084     val vrs = Term.add_frees concl' []

  1085     val cvrs = map (cterm_of thy o Free) vrs

  1086     val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))

  1087     val goal = Logic.mk_implies (concl'', concl)

  1088     val rule = Goal.prove ctxt [] [] goal 

  1089       (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))

  1090   in

  1091     rtac rule i

  1092   end)  

  1093 *}

  1094 

  1095 (* General outline of the lifting procedure *)

  1096 (* **************************************** *)

  1097 (*                                          *)

  1098 (* - A is the original raw theorem          *)

  1099 (* - B is the regularized theorem           *)

  1100 (* - C is the rep/abs injected version of B *) 

  1101 (* - D is the lifted theorem                *)

  1102 (*                                          *)

  1103 (* - b is the regularization step           *)

  1104 (* - c is the rep/abs injection step        *)

  1105 (* - d is the cleaning part                 *)

  1106 

  1107 lemma procedure:

  1108   assumes a: "A"

  1109   and     b: "A \<Longrightarrow> B"

  1110   and     c: "B = C"

  1111   and     d: "C = D"

  1112   shows   "D"

  1113   using a b c d

  1114   by simp

  1115 

  1116 ML {*

  1117 fun lift_error ctxt fun_str rtrm qtrm =

  1118 let

  1119   val rtrm_str = Syntax.string_of_term ctxt rtrm

  1120   val qtrm_str = Syntax.string_of_term ctxt qtrm

  1121   val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 

  1122              "and the lifted theorem", rtrm_str, "do not match"]

  1123 in

  1124   error (space_implode " " msg)

  1125 end

  1126 *}

  1127 

  1128 ML {* 

  1129 fun procedure_inst ctxt rtrm qtrm =

  1130 let

  1131   val thy = ProofContext.theory_of ctxt

  1132   val rtrm' = HOLogic.dest_Trueprop rtrm

  1133   val qtrm' = HOLogic.dest_Trueprop qtrm

  1134   val reg_goal = 

  1135         Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')

  1136         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm

  1137   val inj_goal = 

  1138         Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))

  1139         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm

  1140 in

  1141   Drule.instantiate' []

  1142     [SOME (cterm_of thy rtrm'),

  1143      SOME (cterm_of thy reg_goal),

  1144      SOME (cterm_of thy inj_goal)]

  1145   @{thm procedure}

  1146 end

  1147 *}

  1148   

  1149 ML {*

  1150 fun procedure_tac rthm ctxt =

  1151   ObjectLogic.full_atomize_tac 

  1152   THEN' gen_frees_tac ctxt

  1153   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>

  1154           let

  1155             val rthm' = atomize_thm rthm

  1156             val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))

  1157           in

  1158            EVERY1 [rtac rule, rtac rthm']

  1159         end) ctxt

  1159   (procedure_tac thm lthy) THEN'

  1164   procedure_tac thm lthy THEN'

  1160   (regularize_tac lthy rel_eqv rel_refl) THEN'

  1165   RANGE [regularize_tac lthy rel_eqv rel_refl,

  1161   (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN'

  1166          REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), 

  1162   (clean_tac lthy quot defs reps_same)

  1167          clean_tac lthy quot defs reps_same]