src/HOL/Tools/Quotient/quotient_tacs.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35222 4f1fba00f66d
child 35788 f1deaca15ca3
permissions -rw-r--r--
modernized structure Object_Logic;
     1 (*  Title:      quotient_tacs.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 
     4     Tactics for solving goal arising from lifting
     5     theorems to quotient types.
     6 *)
     7 
     8 signature QUOTIENT_TACS =
     9 sig
    10   val regularize_tac: Proof.context -> int -> tactic
    11   val injection_tac: Proof.context -> int -> tactic
    12   val all_injection_tac: Proof.context -> int -> tactic
    13   val clean_tac: Proof.context -> int -> tactic
    14   val procedure_tac: Proof.context -> thm -> int -> tactic
    15   val lift_tac: Proof.context -> thm list -> int -> tactic
    16   val quotient_tac: Proof.context -> int -> tactic
    17   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
    18   val lifted_attrib: attribute
    19 end;
    20 
    21 structure Quotient_Tacs: QUOTIENT_TACS =
    22 struct
    23 
    24 open Quotient_Info;
    25 open Quotient_Term;
    26 
    27 
    28 (** various helper fuctions **)
    29 
    30 (* Since HOL_basic_ss is too "big" for us, we *)
    31 (* need to set up our own minimal simpset.    *)
    32 fun mk_minimal_ss ctxt =
    33   Simplifier.context ctxt empty_ss
    34     setsubgoaler asm_simp_tac
    35     setmksimps (mksimps [])
    36 
    37 (* composition of two theorems, used in maps *)
    38 fun OF1 thm1 thm2 = thm2 RS thm1
    39 
    40 (* prints a warning, if the subgoal is not solved *)
    41 fun WARN (tac, msg) i st =
    42  case Seq.pull (SOLVED' tac i st) of
    43      NONE    => (warning msg; Seq.single st)
    44    | seqcell => Seq.make (fn () => seqcell)
    45 
    46 fun RANGE_WARN tacs = RANGE (map WARN tacs)
    47 
    48 fun atomize_thm thm =
    49 let
    50   val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
    51   val thm'' = Object_Logic.atomize (cprop_of thm')
    52 in
    53   @{thm equal_elim_rule1} OF [thm'', thm']
    54 end
    55 
    56 
    57 
    58 (*** Regularize Tactic ***)
    59 
    60 (** solvers for equivp and quotient assumptions **)
    61 
    62 fun equiv_tac ctxt =
    63   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
    64 
    65 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
    66 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
    67 
    68 fun quotient_tac ctxt =
    69   (REPEAT_ALL_NEW (FIRST'
    70     [rtac @{thm identity_quotient},
    71      resolve_tac (quotient_rules_get ctxt)]))
    72 
    73 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    74 val quotient_solver =
    75   Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
    76 
    77 fun solve_quotient_assm ctxt thm =
    78   case Seq.pull (quotient_tac ctxt 1 thm) of
    79     SOME (t, _) => t
    80   | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
    81 
    82 
    83 fun prep_trm thy (x, (T, t)) =
    84   (cterm_of thy (Var (x, T)), cterm_of thy t)
    85 
    86 fun prep_ty thy (x, (S, ty)) =
    87   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
    88 
    89 fun get_match_inst thy pat trm =
    90 let
    91   val univ = Unify.matchers thy [(pat, trm)]
    92   val SOME (env, _) = Seq.pull univ             (* raises BIND, if no unifier *)
    93   val tenv = Vartab.dest (Envir.term_env env)
    94   val tyenv = Vartab.dest (Envir.type_env env)
    95 in
    96   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
    97 end
    98 
    99 (* Calculates the instantiations for the lemmas:
   100 
   101       ball_reg_eqv_range and bex_reg_eqv_range
   102 
   103    Since the left-hand-side contains a non-pattern '?P (f ?x)'
   104    we rely on unification/instantiation to check whether the
   105    theorem applies and return NONE if it doesn't.
   106 *)
   107 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
   108 let
   109   val thy = ProofContext.theory_of ctxt
   110   fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
   111   val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
   112   val trm_inst = map (SOME o cterm_of thy) [R2, R1]
   113 in
   114   case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
   115     NONE => NONE
   116   | SOME thm' =>
   117       (case try (get_match_inst thy (get_lhs thm')) redex of
   118         NONE => NONE
   119       | SOME inst2 => try (Drule.instantiate inst2) thm')
   120 end
   121 
   122 fun ball_bex_range_simproc ss redex =
   123 let
   124   val ctxt = Simplifier.the_context ss
   125 in
   126   case redex of
   127     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
   128       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   129         calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   130 
   131   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
   132       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   133         calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   134 
   135   | _ => NONE
   136 end
   137 
   138 (* Regularize works as follows:
   139 
   140   0. preliminary simplification step according to
   141      ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
   142 
   143   1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
   144 
   145   2. monos
   146 
   147   3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
   148 
   149   4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
   150      to avoid loops
   151 
   152   5. then simplification like 0
   153 
   154   finally jump back to 1
   155 *)
   156 
   157 fun regularize_tac ctxt =
   158 let
   159   val thy = ProofContext.theory_of ctxt
   160   val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   161   val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
   162   val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   163   val simpset = (mk_minimal_ss ctxt)
   164                        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   165                        addsimprocs [simproc]
   166                        addSolver equiv_solver addSolver quotient_solver
   167   val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
   168   val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
   169 in
   170   simp_tac simpset THEN'
   171   REPEAT_ALL_NEW (CHANGED o FIRST'
   172     [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
   173      resolve_tac (Inductive.get_monos ctxt),
   174      resolve_tac @{thms ball_all_comm bex_ex_comm},
   175      resolve_tac eq_eqvs,
   176      simp_tac simpset])
   177 end
   178 
   179 
   180 
   181 (*** Injection Tactic ***)
   182 
   183 (* Looks for Quot_True assumptions, and in case its parameter
   184    is an application, it returns the function and the argument.
   185 *)
   186 fun find_qt_asm asms =
   187 let
   188   fun find_fun trm =
   189     case trm of
   190       (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
   191     | _ => false
   192 in
   193  case find_first find_fun asms of
   194    SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
   195  | _ => NONE
   196 end
   197 
   198 fun quot_true_simple_conv ctxt fnctn ctrm =
   199   case (term_of ctrm) of
   200     (Const (@{const_name Quot_True}, _) $ x) =>
   201     let
   202       val fx = fnctn x;
   203       val thy = ProofContext.theory_of ctxt;
   204       val cx = cterm_of thy x;
   205       val cfx = cterm_of thy fx;
   206       val cxt = ctyp_of thy (fastype_of x);
   207       val cfxt = ctyp_of thy (fastype_of fx);
   208       val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   209     in
   210       Conv.rewr_conv thm ctrm
   211     end
   212 
   213 fun quot_true_conv ctxt fnctn ctrm =
   214   case (term_of ctrm) of
   215     (Const (@{const_name Quot_True}, _) $ _) =>
   216       quot_true_simple_conv ctxt fnctn ctrm
   217   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   218   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
   219   | _ => Conv.all_conv ctrm
   220 
   221 fun quot_true_tac ctxt fnctn =
   222    CONVERSION
   223     ((Conv.params_conv ~1 (fn ctxt =>
   224        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
   225 
   226 fun dest_comb (f $ a) = (f, a)
   227 fun dest_bcomb ((_ $ l) $ r) = (l, r)
   228 
   229 fun unlam t =
   230   case t of
   231     (Abs a) => snd (Term.dest_abs a)
   232   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
   233 
   234 fun dest_fun_type (Type("fun", [T, S])) = (T, S)
   235   | dest_fun_type _ = error "dest_fun_type"
   236 
   237 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
   238 
   239 (* We apply apply_rsp only in case if the type needs lifting.
   240    This is the case if the type of the data in the Quot_True
   241    assumption is different from the corresponding type in the goal.
   242 *)
   243 val apply_rsp_tac =
   244   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   245   let
   246     val bare_concl = HOLogic.dest_Trueprop (term_of concl)
   247     val qt_asm = find_qt_asm (map term_of asms)
   248   in
   249     case (bare_concl, qt_asm) of
   250       (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
   251          if fastype_of qt_fun = fastype_of f
   252          then no_tac
   253          else
   254            let
   255              val ty_x = fastype_of x
   256              val ty_b = fastype_of qt_arg
   257              val ty_f = range_type (fastype_of f)
   258              val thy = ProofContext.theory_of context
   259              val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
   260              val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
   261              val inst_thm = Drule.instantiate' ty_inst
   262                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
   263            in
   264              (rtac inst_thm THEN' quotient_tac context) 1
   265            end
   266     | _ => no_tac
   267   end)
   268 
   269 (* Instantiates and applies 'equals_rsp'. Since the theorem is
   270    complex we rely on instantiation to tell us if it applies
   271 *)
   272 fun equals_rsp_tac R ctxt =
   273 let
   274   val thy = ProofContext.theory_of ctxt
   275 in
   276   case try (cterm_of thy) R of (* There can be loose bounds in R *)
   277     SOME ctm =>
   278       let
   279         val ty = domain_type (fastype_of R)
   280       in
   281         case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
   282           [SOME (cterm_of thy R)]) @{thm equals_rsp} of
   283           SOME thm => rtac thm THEN' quotient_tac ctxt
   284         | NONE => K no_tac
   285       end
   286   | _ => K no_tac
   287 end
   288 
   289 fun rep_abs_rsp_tac ctxt =
   290   SUBGOAL (fn (goal, i) =>
   291     case (try bare_concl goal) of
   292       SOME (rel $ _ $ (rep $ (abs $ _))) =>
   293         let
   294           val thy = ProofContext.theory_of ctxt;
   295           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
   296           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
   297         in
   298           case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
   299             SOME t_inst =>
   300               (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
   301                 SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
   302               | NONE => no_tac)
   303           | NONE => no_tac
   304         end
   305     | _ => no_tac)
   306 
   307 
   308 
   309 (* Injection means to prove that the regularised theorem implies
   310    the abs/rep injected one.
   311 
   312    The deterministic part:
   313     - remove lambdas from both sides
   314     - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
   315     - prove Ball/Bex relations unfolding fun_rel_id
   316     - reflexivity of equality
   317     - prove equality of relations using equals_rsp
   318     - use user-supplied RSP theorems
   319     - solve 'relation of relations' goals using quot_rel_rsp
   320     - remove rep_abs from the right side
   321       (Lambdas under respects may have left us some assumptions)
   322 
   323    Then in order:
   324     - split applications of lifted type (apply_rsp)
   325     - split applications of non-lifted type (cong_tac)
   326     - apply extentionality
   327     - assumption
   328     - reflexivity of the relation
   329 *)
   330 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
   331 (case (bare_concl goal) of
   332     (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   333   (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
   334       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   335 
   336     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   337 | (Const (@{const_name "op ="},_) $
   338     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   339     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   340       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   341 
   342     (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
   343 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   344     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   345     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   346       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   347 
   348     (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   349 | Const (@{const_name "op ="},_) $
   350     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   351     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   352       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   353 
   354     (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
   355 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   356     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   357     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   358       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   359 
   360 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   361     (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
   362       => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
   363 
   364 | (_ $
   365     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   366     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   367       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
   368 
   369 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
   370    (rtac @{thm refl} ORELSE'
   371     (equals_rsp_tac R ctxt THEN' RANGE [
   372        quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
   373 
   374     (* reflexivity of operators arising from Cong_tac *)
   375 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
   376 
   377    (* respectfulness of constants; in particular of a simple relation *)
   378 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
   379     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
   380 
   381     (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
   382     (* observe fun_map *)
   383 | _ $ _ $ _
   384     => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
   385        ORELSE' rep_abs_rsp_tac ctxt
   386 
   387 | _ => K no_tac
   388 ) i)
   389 
   390 fun injection_step_tac ctxt rel_refl =
   391  FIRST' [
   392     injection_match_tac ctxt,
   393 
   394     (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
   395     apply_rsp_tac ctxt THEN'
   396                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
   397 
   398     (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
   399     (* merge with previous tactic *)
   400     Cong_Tac.cong_tac @{thm cong} THEN'
   401                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
   402 
   403     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
   404     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
   405 
   406     (* resolving with R x y assumptions *)
   407     atac,
   408 
   409     (* reflexivity of the basic relations *)
   410     (* R ... ... *)
   411     resolve_tac rel_refl]
   412 
   413 fun injection_tac ctxt =
   414 let
   415   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
   416 in
   417   injection_step_tac ctxt rel_refl
   418 end
   419 
   420 fun all_injection_tac ctxt =
   421   REPEAT_ALL_NEW (injection_tac ctxt)
   422 
   423 
   424 
   425 (*** Cleaning of the Theorem ***)
   426 
   427 (* expands all fun_maps, except in front of the (bound) variables listed in xs *)
   428 fun fun_map_simple_conv xs ctrm =
   429   case (term_of ctrm) of
   430     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
   431         if member (op=) xs h
   432         then Conv.all_conv ctrm
   433         else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
   434   | _ => Conv.all_conv ctrm
   435 
   436 fun fun_map_conv xs ctxt ctrm =
   437   case (term_of ctrm) of
   438       _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
   439                 fun_map_simple_conv xs) ctrm
   440     | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
   441     | _ => Conv.all_conv ctrm
   442 
   443 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
   444 
   445 (* custom matching functions *)
   446 fun mk_abs u i t =
   447   if incr_boundvars i u aconv t then Bound i else
   448   case t of
   449     t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
   450   | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
   451   | Bound j => if i = j then error "make_inst" else t
   452   | _ => t
   453 
   454 fun make_inst lhs t =
   455 let
   456   val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
   457   val _ $ (Abs (_, _, (_ $ g))) = t;
   458 in
   459   (f, Abs ("x", T, mk_abs u 0 g))
   460 end
   461 
   462 fun make_inst_id lhs t =
   463 let
   464   val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
   465   val _ $ (Abs (_, _, g)) = t;
   466 in
   467   (f, Abs ("x", T, mk_abs u 0 g))
   468 end
   469 
   470 (* Simplifies a redex using the 'lambda_prs' theorem.
   471    First instantiates the types and known subterms.
   472    Then solves the quotient assumptions to get Rep2 and Abs1
   473    Finally instantiates the function f using make_inst
   474    If Rep2 is an identity then the pattern is simpler and
   475    make_inst_id is used
   476 *)
   477 fun lambda_prs_simple_conv ctxt ctrm =
   478   case (term_of ctrm) of
   479     (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
   480       let
   481         val thy = ProofContext.theory_of ctxt
   482         val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
   483         val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
   484         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
   485         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
   486         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   487         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
   488         val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
   489         val (insp, inst) =
   490           if ty_c = ty_d
   491           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   492           else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   493         val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
   494       in
   495         Conv.rewr_conv thm4 ctrm
   496       end
   497   | _ => Conv.all_conv ctrm
   498 
   499 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
   500 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
   501 
   502 
   503 (* Cleaning consists of:
   504 
   505   1. unfolding of ---> in front of everything, except
   506      bound variables (this prevents lambda_prs from
   507      becoming stuck)
   508 
   509   2. simplification with lambda_prs
   510 
   511   3. simplification with:
   512 
   513       - Quotient_abs_rep Quotient_rel_rep
   514         babs_prs all_prs ex_prs ex1_prs
   515 
   516       - id_simps and preservation lemmas and
   517 
   518       - symmetric versions of the definitions
   519         (that is definitions of quotient constants
   520          are folded)
   521 
   522   4. test for refl
   523 *)
   524 fun clean_tac lthy =
   525 let
   526   val defs = map (symmetric o #def) (qconsts_dest lthy)
   527   val prs = prs_rules_get lthy
   528   val ids = id_simps_get lthy
   529   val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   530 
   531   val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   532 in
   533   EVERY' [fun_map_tac lthy,
   534           lambda_prs_tac lthy,
   535           simp_tac ss,
   536           TRY o rtac refl]
   537 end
   538 
   539 
   540 
   541 (** Tactic for Generalising Free Variables in a Goal **)
   542 
   543 fun inst_spec ctrm =
   544    Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
   545 
   546 fun inst_spec_tac ctrms =
   547   EVERY' (map (dtac o inst_spec) ctrms)
   548 
   549 fun all_list xs trm =
   550   fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
   551 
   552 fun apply_under_Trueprop f =
   553   HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
   554 
   555 fun gen_frees_tac ctxt =
   556   SUBGOAL (fn (concl, i) =>
   557     let
   558       val thy = ProofContext.theory_of ctxt
   559       val vrs = Term.add_frees concl []
   560       val cvrs = map (cterm_of thy o Free) vrs
   561       val concl' = apply_under_Trueprop (all_list vrs) concl
   562       val goal = Logic.mk_implies (concl', concl)
   563       val rule = Goal.prove ctxt [] [] goal
   564         (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
   565     in
   566       rtac rule i
   567     end)
   568 
   569 
   570 (** The General Shape of the Lifting Procedure **)
   571 
   572 (* - A is the original raw theorem
   573    - B is the regularized theorem
   574    - C is the rep/abs injected version of B
   575    - D is the lifted theorem
   576 
   577    - 1st prem is the regularization step
   578    - 2nd prem is the rep/abs injection step
   579    - 3rd prem is the cleaning part
   580 
   581    the Quot_True premise in 2nd records the lifted theorem
   582 *)
   583 val lifting_procedure_thm =
   584   @{lemma  "[|A;
   585               A --> B;
   586               Quot_True D ==> B = C;
   587               C = D|] ==> D"
   588       by (simp add: Quot_True_def)}
   589 
   590 fun lift_match_error ctxt msg rtrm qtrm =
   591 let
   592   val rtrm_str = Syntax.string_of_term ctxt rtrm
   593   val qtrm_str = Syntax.string_of_term ctxt qtrm
   594   val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
   595     "", "does not match with original theorem", rtrm_str]
   596 in
   597   error msg
   598 end
   599 
   600 fun procedure_inst ctxt rtrm qtrm =
   601 let
   602   val thy = ProofContext.theory_of ctxt
   603   val rtrm' = HOLogic.dest_Trueprop rtrm
   604   val qtrm' = HOLogic.dest_Trueprop qtrm
   605   val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
   606     handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
   607   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   608     handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
   609 in
   610   Drule.instantiate' []
   611     [SOME (cterm_of thy rtrm'),
   612      SOME (cterm_of thy reg_goal),
   613      NONE,
   614      SOME (cterm_of thy inj_goal)] lifting_procedure_thm
   615 end
   616 
   617 (* the tactic leaves three subgoals to be proved *)
   618 fun procedure_tac ctxt rthm =
   619   Object_Logic.full_atomize_tac
   620   THEN' gen_frees_tac ctxt
   621   THEN' SUBGOAL (fn (goal, i) =>
   622     let
   623       val rthm' = atomize_thm rthm
   624       val rule = procedure_inst ctxt (prop_of rthm') goal
   625     in
   626       (rtac rule THEN' rtac rthm') i
   627     end)
   628 
   629 
   630 (* Automatic Proofs *)
   631 
   632 val msg1 = "The regularize proof failed."
   633 val msg2 = cat_lines ["The injection proof failed.",
   634                       "This is probably due to missing respects lemmas.",
   635                       "Try invoking the injection method manually to see",
   636                       "which lemmas are missing."]
   637 val msg3 = "The cleaning proof failed."
   638 
   639 fun lift_tac ctxt rthms =
   640 let
   641   fun mk_tac rthm =
   642     procedure_tac ctxt rthm
   643     THEN' RANGE_WARN
   644       [(regularize_tac ctxt, msg1),
   645        (all_injection_tac ctxt, msg2),
   646        (clean_tac ctxt, msg3)]
   647 in
   648   simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
   649   THEN' RANGE (map mk_tac rthms)
   650 end
   651 
   652 (* An Attribute which automatically constructs the qthm *)
   653 fun lifted_attrib_aux context thm =
   654 let
   655   val ctxt = Context.proof_of context
   656   val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
   657   val goal = (quotient_lift_all ctxt' o prop_of) thm'
   658 in
   659   Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
   660   |> singleton (ProofContext.export ctxt' ctxt)
   661 end;
   662 
   663 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
   664 
   665 end; (* structure *)