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_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 *)  (* FIXME fragile *)

    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 (ERROR msg) => lift_match_error ctxt msg rtrm qtrm

   607   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')

   608     handle (ERROR 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 *)