src/HOL/Tools/Quotient/quotient_tacs.ML
author wenzelm
Tue Feb 14 20:09:35 2012 +0100 (2012-02-14)
changeset 46468 4db76d47b51a
parent 45782 f82020ca3248
child 47308 9caab698dbe4
permissions -rw-r--r--
simplified use of tacticals;
     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_ss ctxt =
    36   Simplifier.context ctxt empty_ss
    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 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
    61 val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
    62 
    63 fun quotient_tac ctxt =
    64   (REPEAT_ALL_NEW (FIRST'
    65     [rtac @{thm identity_quotient},
    66      resolve_tac (Quotient_Info.quotient_rules ctxt)]))
    67 
    68 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    69 val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
    70 
    71 fun solve_quotient_assm ctxt thm =
    72   case Seq.pull (quotient_tac ctxt 1 thm) of
    73     SOME (t, _) => t
    74   | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
    75 
    76 
    77 fun prep_trm thy (x, (T, t)) =
    78   (cterm_of thy (Var (x, T)), cterm_of thy t)
    79 
    80 fun prep_ty thy (x, (S, ty)) =
    81   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
    82 
    83 fun get_match_inst thy pat trm =
    84   let
    85     val univ = Unify.matchers thy [(pat, trm)]
    86     val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
    87     val tenv = Vartab.dest (Envir.term_env env)
    88     val tyenv = Vartab.dest (Envir.type_env env)
    89   in
    90     (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
    91   end
    92 
    93 (* Calculates the instantiations for the lemmas:
    94 
    95       ball_reg_eqv_range and bex_reg_eqv_range
    96 
    97    Since the left-hand-side contains a non-pattern '?P (f ?x)'
    98    we rely on unification/instantiation to check whether the
    99    theorem applies and return NONE if it doesn't.
   100 *)
   101 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
   102   let
   103     val thy = Proof_Context.theory_of ctxt
   104     fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
   105     val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
   106     val trm_inst = map (SOME o cterm_of thy) [R2, R1]
   107   in
   108     (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
   109       NONE => NONE
   110     | SOME thm' =>
   111         (case try (get_match_inst thy (get_lhs thm')) redex of
   112           NONE => NONE
   113         | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
   114   end
   115 
   116 fun ball_bex_range_simproc ss redex =
   117   let
   118     val ctxt = Simplifier.the_context ss
   119   in
   120     case redex of
   121       (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
   122         (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   123           calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   124 
   125     | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
   126         (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
   127           calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   128 
   129     | _ => NONE
   130   end
   131 
   132 (* Regularize works as follows:
   133 
   134   0. preliminary simplification step according to
   135      ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
   136 
   137   1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
   138 
   139   2. monos
   140 
   141   3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
   142 
   143   4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
   144      to avoid loops
   145 
   146   5. then simplification like 0
   147 
   148   finally jump back to 1
   149 *)
   150 
   151 fun reflp_get ctxt =
   152   map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
   153     handle THM _ => NONE) (Quotient_Info.equiv_rules ctxt)
   154 
   155 val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
   156 
   157 fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules ctxt)
   158 
   159 fun regularize_tac ctxt =
   160   let
   161     val thy = Proof_Context.theory_of ctxt
   162     val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   163     val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
   164     val simproc =
   165       Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   166     val simpset =
   167       mk_minimal_ss ctxt
   168       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   169       addsimprocs [simproc]
   170       addSolver equiv_solver addSolver quotient_solver
   171     val eq_eqvs = eq_imp_rel_get ctxt
   172   in
   173     simp_tac simpset THEN'
   174     TRY o REPEAT_ALL_NEW (CHANGED o FIRST'
   175       [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
   176        resolve_tac (Inductive.get_monos ctxt),
   177        resolve_tac @{thms ball_all_comm bex_ex_comm},
   178        resolve_tac eq_eqvs,
   179        simp_tac simpset])
   180   end
   181 
   182 
   183 
   184 (*** Injection Tactic ***)
   185 
   186 (* Looks for Quot_True assumptions, and in case its parameter
   187    is an application, it returns the function and the argument.
   188 *)
   189 fun find_qt_asm asms =
   190   let
   191     fun find_fun trm =
   192       (case trm of
   193         (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
   194       | _ => false)
   195   in
   196      (case find_first find_fun asms of
   197        SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
   198      | _ => NONE)
   199   end
   200 
   201 fun quot_true_simple_conv ctxt fnctn ctrm =
   202   case term_of ctrm of
   203     (Const (@{const_name Quot_True}, _) $ x) =>
   204       let
   205         val fx = fnctn x;
   206         val thy = Proof_Context.theory_of ctxt;
   207         val cx = cterm_of thy x;
   208         val cfx = cterm_of thy fx;
   209         val cxt = ctyp_of thy (fastype_of x);
   210         val cfxt = ctyp_of thy (fastype_of fx);
   211         val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
   212       in
   213         Conv.rewr_conv thm ctrm
   214       end
   215 
   216 fun quot_true_conv ctxt fnctn ctrm =
   217   (case term_of ctrm of
   218     (Const (@{const_name Quot_True}, _) $ _) =>
   219       quot_true_simple_conv ctxt fnctn ctrm
   220   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   221   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
   222   | _ => Conv.all_conv ctrm)
   223 
   224 fun quot_true_tac ctxt fnctn =
   225   CONVERSION
   226     ((Conv.params_conv ~1 (fn ctxt =>
   227         (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
   228 
   229 fun dest_comb (f $ a) = (f, a)
   230 fun dest_bcomb ((_ $ l) $ r) = (l, r)
   231 
   232 fun unlam t =
   233   (case t of
   234     Abs a => snd (Term.dest_abs a)
   235   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
   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 = Proof_Context.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' SOLVED' (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 = Proof_Context.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 = Proof_Context.theory_of ctxt;
   295           val (ty_a, ty_b) = dest_funT (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         handle TERM _ => no_tac)
   306     | _ => no_tac))
   307 
   308 
   309 (* Injection means to prove that the regularized 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 using fun_relI
   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_relI} THEN' quot_true_tac ctxt unlam
   335 
   336       (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
   337   | (Const (@{const_name HOL.eq},_) $
   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_relI} THEN' quot_true_tac ctxt unlam
   347 
   348       (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
   349   | Const (@{const_name HOL.eq},_) $
   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_relI} 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' quotient_tac ctxt
   368 
   369   | Const (@{const_name HOL.eq},_) $ (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 HOL.eq},_) $ _ $ _ => 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 (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
   380 
   381       (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
   382       (* observe map_fun *)
   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) i)
   388 
   389 fun injection_step_tac ctxt rel_refl =
   390   FIRST' [
   391     injection_match_tac ctxt,
   392 
   393     (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
   394     apply_rsp_tac ctxt THEN'
   395                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
   396 
   397     (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
   398     (* merge with previous tactic *)
   399     Cong_Tac.cong_tac @{thm cong} THEN'
   400                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
   401 
   402     (* resolving with R x y assumptions *)
   403     atac,
   404 
   405     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
   406     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
   407 
   408     (* reflexivity of the basic relations *)
   409     (* R ... ... *)
   410     resolve_tac rel_refl]
   411 
   412 fun injection_tac ctxt =
   413   let
   414     val rel_refl = reflp_get ctxt
   415   in
   416     injection_step_tac ctxt rel_refl
   417   end
   418 
   419 fun all_injection_tac ctxt =
   420   REPEAT_ALL_NEW (injection_tac ctxt)
   421 
   422 
   423 
   424 (*** Cleaning of the Theorem ***)
   425 
   426 (* expands all map_funs, except in front of the (bound) variables listed in xs *)
   427 fun map_fun_simple_conv xs ctrm =
   428   (case term_of ctrm of
   429     ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
   430         if member (op=) xs h
   431         then Conv.all_conv ctrm
   432         else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
   433   | _ => Conv.all_conv ctrm)
   434 
   435 fun map_fun_conv xs ctxt ctrm =
   436   (case term_of ctrm of
   437     _ $ _ =>
   438       (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
   439         map_fun_simple_conv xs) ctrm
   440   | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
   441   | _ => Conv.all_conv ctrm)
   442 
   443 fun map_fun_tac ctxt = CONVERSION (map_fun_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
   448   else
   449     case t of
   450       t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
   451     | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
   452     | Bound j => if i = j then error "make_inst" else t
   453     | _ => t
   454 
   455 fun make_inst lhs t =
   456   let
   457     val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
   458     val _ $ (Abs (_, _, (_ $ g))) = t;
   459   in
   460     (f, Abs ("x", T, mk_abs u 0 g))
   461   end
   462 
   463 fun make_inst_id lhs t =
   464   let
   465     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
   466     val _ $ (Abs (_, _, g)) = t;
   467   in
   468     (f, Abs ("x", T, mk_abs u 0 g))
   469   end
   470 
   471 (* Simplifies a redex using the 'lambda_prs' theorem.
   472    First instantiates the types and known subterms.
   473    Then solves the quotient assumptions to get Rep2 and Abs1
   474    Finally instantiates the function f using make_inst
   475    If Rep2 is an identity then the pattern is simpler and
   476    make_inst_id is used
   477 *)
   478 fun lambda_prs_simple_conv ctxt ctrm =
   479   (case term_of ctrm of
   480     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
   481       let
   482         val thy = Proof_Context.theory_of ctxt
   483         val (ty_b, ty_a) = dest_funT (fastype_of r1)
   484         val (ty_c, ty_d) = dest_funT (fastype_of a2)
   485         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
   486         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
   487         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
   488         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
   489         val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
   490         val (insp, inst) =
   491           if ty_c = ty_d
   492           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   493           else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
   494         val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
   495       in
   496         Conv.rewr_conv thm4 ctrm
   497       end
   498   | _ => Conv.all_conv ctrm)
   499 
   500 fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
   501 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
   502 
   503 
   504 (* Cleaning consists of:
   505 
   506   1. unfolding of ---> in front of everything, except
   507      bound variables (this prevents lambda_prs from
   508      becoming stuck)
   509 
   510   2. simplification with lambda_prs
   511 
   512   3. simplification with:
   513 
   514       - Quotient_abs_rep Quotient_rel_rep
   515         babs_prs all_prs ex_prs ex1_prs
   516 
   517       - id_simps and preservation lemmas and
   518 
   519       - symmetric versions of the definitions
   520         (that is definitions of quotient constants
   521          are folded)
   522 
   523   4. test for refl
   524 *)
   525 fun clean_tac lthy =
   526   let
   527     val thy =  Proof_Context.theory_of lthy
   528     val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
   529     val prs = Quotient_Info.prs_rules lthy
   530     val ids = Quotient_Info.id_simps lthy
   531     val thms =
   532       @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   533 
   534     val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   535   in
   536     EVERY' [
   537       map_fun_tac lthy,
   538       lambda_prs_tac lthy,
   539       simp_tac ss,
   540       TRY o rtac refl]
   541   end
   542 
   543 
   544 (* Tactic for Generalising Free Variables in a Goal *)
   545 
   546 fun inst_spec ctrm =
   547   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
   548 
   549 fun inst_spec_tac ctrms =
   550   EVERY' (map (dtac o inst_spec) ctrms)
   551 
   552 fun all_list xs trm =
   553   fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
   554 
   555 fun apply_under_Trueprop f =
   556   HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
   557 
   558 fun gen_frees_tac ctxt =
   559   SUBGOAL (fn (concl, i) =>
   560     let
   561       val thy = Proof_Context.theory_of ctxt
   562       val vrs = Term.add_frees concl []
   563       val cvrs = map (cterm_of thy o Free) vrs
   564       val concl' = apply_under_Trueprop (all_list vrs) concl
   565       val goal = Logic.mk_implies (concl', concl)
   566       val rule = Goal.prove ctxt [] [] goal
   567         (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
   568     in
   569       rtac rule i
   570     end)
   571 
   572 
   573 (** The General Shape of the Lifting Procedure **)
   574 
   575 (* - A is the original raw theorem
   576    - B is the regularized theorem
   577    - C is the rep/abs injected version of B
   578    - D is the lifted theorem
   579 
   580    - 1st prem is the regularization step
   581    - 2nd prem is the rep/abs injection step
   582    - 3rd prem is the cleaning part
   583 
   584    the Quot_True premise in 2nd records the lifted theorem
   585 *)
   586 val procedure_thm =
   587   @{lemma  "[|A;
   588               A --> B;
   589               Quot_True D ==> B = C;
   590               C = D|] ==> D"
   591       by (simp add: Quot_True_def)}
   592 
   593 (* in case of partial equivalence relations, this form of the 
   594    procedure theorem results in solvable proof obligations 
   595 *)
   596 val partiality_procedure_thm =
   597   @{lemma  "[|B; 
   598               Quot_True D ==> B = C;
   599               C = D|] ==> D"
   600       by (simp add: Quot_True_def)}
   601 
   602 fun lift_match_error ctxt msg rtrm qtrm =
   603   let
   604     val rtrm_str = Syntax.string_of_term ctxt rtrm
   605     val qtrm_str = Syntax.string_of_term ctxt qtrm
   606     val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
   607       "", "does not match with original theorem", rtrm_str]
   608   in
   609     error msg
   610   end
   611 
   612 fun procedure_inst ctxt rtrm qtrm =
   613   let
   614     val thy = Proof_Context.theory_of ctxt
   615     val rtrm' = HOLogic.dest_Trueprop rtrm
   616     val qtrm' = HOLogic.dest_Trueprop qtrm
   617     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
   618       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   619     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   620       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   621   in
   622     Drule.instantiate' []
   623       [SOME (cterm_of thy rtrm'),
   624        SOME (cterm_of thy reg_goal),
   625        NONE,
   626        SOME (cterm_of thy inj_goal)] procedure_thm
   627   end
   628 
   629 
   630 (* Since we use Ball and Bex during the lifting and descending,
   631    we cannot deal with lemmas containing them, unless we unfold
   632    them by default. *)
   633 
   634 val default_unfolds = @{thms Ball_def Bex_def}
   635 
   636 
   637 (** descending as tactic **)
   638 
   639 fun descend_procedure_tac ctxt simps =
   640   let
   641     val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   642   in
   643     full_simp_tac ss
   644     THEN' Object_Logic.full_atomize_tac
   645     THEN' gen_frees_tac ctxt
   646     THEN' SUBGOAL (fn (goal, i) =>
   647       let
   648         val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
   649         val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
   650         val rule = procedure_inst ctxt rtrm  goal
   651       in
   652         rtac rule i
   653       end)
   654   end
   655 
   656 fun descend_tac ctxt simps =
   657   let
   658     val mk_tac_raw =
   659       descend_procedure_tac ctxt simps
   660       THEN' RANGE
   661         [Object_Logic.rulify_tac THEN' (K all_tac),
   662          regularize_tac ctxt,
   663          all_injection_tac ctxt,
   664          clean_tac ctxt]
   665   in
   666     Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
   667   end
   668 
   669 
   670 (** descending for partial equivalence relations **)
   671 
   672 fun partiality_procedure_inst ctxt rtrm qtrm =
   673   let
   674     val thy = Proof_Context.theory_of ctxt
   675     val rtrm' = HOLogic.dest_Trueprop rtrm
   676     val qtrm' = HOLogic.dest_Trueprop qtrm
   677     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
   678       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   679     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
   680       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   681   in
   682     Drule.instantiate' []
   683       [SOME (cterm_of thy reg_goal),
   684        NONE,
   685        SOME (cterm_of thy inj_goal)] partiality_procedure_thm
   686   end
   687 
   688 
   689 fun partiality_descend_procedure_tac ctxt simps =
   690   let
   691     val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   692   in
   693     full_simp_tac ss
   694     THEN' Object_Logic.full_atomize_tac
   695     THEN' gen_frees_tac ctxt
   696     THEN' SUBGOAL (fn (goal, i) =>
   697       let
   698         val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
   699         val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
   700         val rule = partiality_procedure_inst ctxt rtrm  goal
   701       in
   702         rtac rule i
   703       end)
   704   end
   705 
   706 fun partiality_descend_tac ctxt simps =
   707   let
   708     val mk_tac_raw =
   709       partiality_descend_procedure_tac ctxt simps
   710       THEN' RANGE
   711         [Object_Logic.rulify_tac THEN' (K all_tac),
   712          all_injection_tac ctxt,
   713          clean_tac ctxt]
   714   in
   715     Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
   716   end
   717 
   718 
   719 
   720 (** lifting as a tactic **)
   721 
   722 
   723 (* the tactic leaves three subgoals to be proved *)
   724 fun lift_procedure_tac ctxt simps rthm =
   725   let
   726     val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
   727   in
   728     full_simp_tac ss
   729     THEN' Object_Logic.full_atomize_tac
   730     THEN' gen_frees_tac ctxt
   731     THEN' SUBGOAL (fn (goal, i) =>
   732       let
   733         (* full_atomize_tac contracts eta redexes,
   734            so we do it also in the original theorem *)
   735         val rthm' =
   736           rthm |> full_simplify ss
   737                |> Drule.eta_contraction_rule
   738                |> Thm.forall_intr_frees
   739                |> atomize_thm
   740 
   741         val rule = procedure_inst ctxt (prop_of rthm') goal
   742       in
   743         (rtac rule THEN' rtac rthm') i
   744       end)
   745   end
   746 
   747 fun lift_single_tac ctxt simps rthm =
   748   lift_procedure_tac ctxt simps rthm
   749   THEN' RANGE
   750     [ regularize_tac ctxt,
   751       all_injection_tac ctxt,
   752       clean_tac ctxt ]
   753 
   754 fun lift_tac ctxt simps rthms =
   755   Goal.conjunction_tac
   756   THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
   757 
   758 
   759 (* automated lifting with pre-simplification of the theorems;
   760    for internal usage *)
   761 fun lifted ctxt qtys simps rthm =
   762   let
   763     val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
   764     val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm')
   765   in
   766     Goal.prove ctxt' [] [] goal
   767       (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
   768     |> singleton (Proof_Context.export ctxt' ctxt)
   769   end
   770 
   771 
   772 (* lifting as an attribute *)
   773 
   774 val lifted_attrib = Thm.rule_attribute (fn context =>
   775   let
   776     val ctxt = Context.proof_of context
   777     val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
   778   in
   779     lifted ctxt qtys []
   780   end)
   781 
   782 end; (* structure *)