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