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