signature QUOTIENT_TACS =+
−
sig+
−
    val regularize_tac: Proof.context -> int -> tactic+
−
    val all_inj_repabs_tac: Proof.context -> int -> tactic+
−
    val clean_tac: Proof.context -> int -> tactic+
−
    val procedure_tac: Proof.context -> thm -> int -> tactic+
−
    val lift_tac: Proof.context ->thm -> int -> tactic+
−
    val quotient_tac: Proof.context -> int -> tactic+
−
end;+
−
+
−
structure Quotient_Tacs: QUOTIENT_TACS =+
−
struct+
−
+
−
open Quotient_Info;+
−
open Quotient_Type;+
−
open Quotient_Term;+
−
+
−
+
−
(* Since HOL_basic_ss is too "big" for us,    *)+
−
(* we need to set up our own minimal simpset. *)+
−
fun  mk_minimal_ss ctxt =+
−
  Simplifier.context ctxt empty_ss+
−
    setsubgoaler asm_simp_tac+
−
    setmksimps (mksimps [])+
−
+
−
+
−
+
−
(* various helper functions *)+
−
fun OF1 thm1 thm2 = thm2 RS thm1+
−
+
−
(* makes sure a subgoal is solved *)+
−
fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)+
−
+
−
(* prints warning, if goal is unsolved *)+
−
fun WARN (tac, msg) i st =+
−
 case Seq.pull ((SOLVES' tac) i st) of+
−
     NONE    => (warning msg; Seq.single st)+
−
   | seqcell => Seq.make (fn () => seqcell)+
−
+
−
fun RANGE_WARN xs = RANGE (map WARN xs)+
−
+
−
fun atomize_thm thm =+
−
let+
−
  val thm' = Thm.freezeT (forall_intr_vars thm)+
−
  val thm'' = ObjectLogic.atomize (cprop_of thm')+
−
in+
−
  @{thm equal_elim_rule1} OF [thm'', thm']+
−
end+
−
+
−
+
−
+
−
+
−
(* Regularize Tactic *)+
−
+
−
fun equiv_tac ctxt =+
−
  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))+
−
+
−
fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)+
−
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac+
−
+
−
fun prep_trm thy (x, (T, t)) =+
−
  (cterm_of thy (Var (x, T)), cterm_of thy t)+
−
+
−
fun prep_ty thy (x, (S, ty)) =+
−
  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)+
−
+
−
fun matching_prs thy pat trm =+
−
let+
−
  val univ = Unify.matchers thy [(pat, trm)]+
−
  val SOME (env, _) = Seq.pull univ+
−
  val tenv = Vartab.dest (Envir.term_env env)+
−
  val tyenv = Vartab.dest (Envir.type_env env)+
−
in+
−
  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)+
−
end+
−
+
−
fun calculate_instance ctxt thm redex R1 R2 =+
−
let+
−
  val thy = ProofContext.theory_of ctxt+
−
  val goal = Const (@{const_name "equivp"}, dummyT) $ R2  +
−
             |> Syntax.check_term ctxt+
−
             |> HOLogic.mk_Trueprop +
−
  val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1)+
−
  val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])+
−
  val R1c = cterm_of thy R1+
−
  val thmi = Drule.instantiate' [] [SOME R1c] thm+
−
  val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex+
−
  val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)+
−
in+
−
  SOME thm2+
−
end+
−
handle _ => NONE+
−
(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)+
−
+
−
fun ball_bex_range_simproc ss redex =+
−
let+
−
  val ctxt = Simplifier.the_context ss+
−
in +
−
 case redex of+
−
    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ +
−
      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>+
−
        calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2+
−
+
−
  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ +
−
      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  +
−
        calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2+
−
  | _ => NONE+
−
end+
−
+
−
(* test whether DETERM makes any difference *)+
−
fun quotient_tac ctxt = SOLVES'  +
−
  (REPEAT_ALL_NEW (FIRST'+
−
    [rtac @{thm identity_quotient},+
−
     resolve_tac (quotient_rules_get ctxt)]))+
−
+
−
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)+
−
val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac+
−
+
−
fun solve_quotient_assum ctxt thm =+
−
  case Seq.pull (quotient_tac ctxt 1 thm) of+
−
    SOME (t, _) => t+
−
  | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"+
−
+
−
+
−
(* 0. preliminary simplification step according to *)+
−
(*    thm ball_reg_eqv bex_reg_eqv babs_reg_eqv    *)+
−
(*        ball_reg_eqv_range bex_reg_eqv_range     *)+
−
(*                                                 *)+
−
(* 1. eliminating simple Ball/Bex instances        *)+
−
(*    thm ball_reg_right bex_reg_left              *)+
−
(*                                                 *)+
−
(* 2. monos                                        *)+
−
(* 3. commutation rules for ball and bex           *)+
−
(*    thm ball_all_comm bex_ex_comm                *)+
−
(*                                                 *)+
−
(* 4. then rel-equality (which need to be          *)+
−
(*    instantiated to avoid loops)                 *)+
−
(*    thm eq_imp_rel                               *)+
−
(*                                                 *)+
−
(* 5. then simplification like 0                   *)+
−
(*                                                 *)+
−
(* finally jump back to 1                          *)+
−
+
−
fun regularize_tac ctxt =+
−
let+
−
  val thy = ProofContext.theory_of ctxt+
−
  val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}+
−
  val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}+
−
  val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))+
−
  val simpset = (mk_minimal_ss ctxt) +
−
                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}+
−
                       addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver+
−
  val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)+
−
in+
−
  simp_tac simpset THEN'+
−
  REPEAT_ALL_NEW (CHANGED o FIRST' [+
−
    resolve_tac @{thms ball_reg_right bex_reg_left},+
−
    resolve_tac (Inductive.get_monos ctxt),+
−
    resolve_tac @{thms ball_all_comm bex_ex_comm},+
−
    resolve_tac eq_eqvs,  +
−
    simp_tac simpset])+
−
end+
−
+
−
+
−
+
−
(* Injection Tactic *)+
−
+
−
(* looks for QUOT_TRUE assumtions, and in case its parameter   *)+
−
(* is an application, it returns the function and the argument *)+
−
fun find_qt_asm asms =+
−
let+
−
  fun find_fun trm =+
−
    case trm of+
−
      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true+
−
    | _ => false+
−
in+
−
 case find_first find_fun asms of+
−
   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)+
−
 | _ => NONE+
−
end+
−
+
−
fun quot_true_simple_conv ctxt fnctn ctrm =+
−
  case (term_of ctrm) of+
−
    (Const (@{const_name QUOT_TRUE}, _) $ x) =>+
−
    let+
−
      val fx = fnctn x;+
−
      val thy = ProofContext.theory_of ctxt;+
−
      val cx = cterm_of thy x;+
−
      val cfx = cterm_of thy fx;+
−
      val cxt = ctyp_of thy (fastype_of x);+
−
      val cfxt = ctyp_of thy (fastype_of fx);+
−
      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}+
−
    in+
−
      Conv.rewr_conv thm ctrm+
−
    end+
−
+
−
fun quot_true_conv ctxt fnctn ctrm =+
−
  case (term_of ctrm) of+
−
    (Const (@{const_name QUOT_TRUE}, _) $ _) =>+
−
      quot_true_simple_conv ctxt fnctn ctrm+
−
  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm+
−
  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm+
−
  | _ => Conv.all_conv ctrm+
−
+
−
fun quot_true_tac ctxt fnctn = +
−
   CONVERSION+
−
    ((Conv.params_conv ~1 (fn ctxt =>+
−
       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)+
−
+
−
fun dest_comb (f $ a) = (f, a) +
−
fun dest_bcomb ((_ $ l) $ r) = (l, r) +
−
+
−
(* TODO: Can this be done easier? *)+
−
fun unlam t =+
−
  case t of+
−
    (Abs a) => snd (Term.dest_abs a)+
−
  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))+
−
+
−
fun dest_fun_type (Type("fun", [T, S])) = (T, S)+
−
  | dest_fun_type _ = error "dest_fun_type"+
−
+
−
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl+
−
+
−
+
−
(* we apply apply_rsp only in case if the type needs lifting,      *)+
−
(* which is the case if the type of the data in the QUOT_TRUE      *)+
−
(* assumption is different from the corresponding type in the goal *)+
−
val apply_rsp_tac =+
−
  Subgoal.FOCUS (fn {concl, asms, context,...} =>+
−
  let+
−
    val bare_concl = HOLogic.dest_Trueprop (term_of concl)+
−
    val qt_asm = find_qt_asm (map term_of asms)+
−
  in+
−
    case (bare_concl, qt_asm) of+
−
      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>+
−
         if (fastype_of qt_fun) = (fastype_of f) +
−
         then no_tac                             +
−
         else                                    +
−
           let+
−
             val ty_x = fastype_of x+
−
             val ty_b = fastype_of qt_arg+
−
             val ty_f = range_type (fastype_of f) +
−
             val thy = ProofContext.theory_of context+
−
             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]+
−
             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];+
−
             val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}+
−
           in+
−
             (rtac inst_thm THEN' quotient_tac context) 1+
−
           end+
−
    | _ => no_tac+
−
  end)+
−
+
−
fun equals_rsp_tac R ctxt =+
−
let+
−
  val ty = domain_type (fastype_of R);+
−
  val thy = ProofContext.theory_of ctxt+
−
  val thm = Drule.instantiate' +
−
               [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}+
−
in+
−
  rtac thm THEN' quotient_tac ctxt+
−
end+
−
(* raised by instantiate' *)+
−
handle THM _  => K no_tac  +
−
     | TYPE _ => K no_tac    +
−
     | TERM _ => K no_tac+
−
+
−
+
−
fun rep_abs_rsp_tac ctxt = +
−
  SUBGOAL (fn (goal, i) =>+
−
    case (bare_concl goal) of +
−
      (rel $ _ $ (rep $ (abs $ _))) =>+
−
        (let+
−
           val thy = ProofContext.theory_of ctxt;+
−
           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);+
−
           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];+
−
           val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];+
−
           val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}+
−
         in+
−
           (rtac inst_thm THEN' quotient_tac ctxt) i+
−
         end+
−
         handle THM _ => no_tac | TYPE _ => no_tac)+
−
    | _ => no_tac)+
−
+
−
+
−
(* FIXME /TODO needs to be adapted *)+
−
(*+
−
To prove that the regularised theorem implies the abs/rep injected, +
−
we try:+
−
+
−
 1) theorems 'trans2' from the appropriate QUOT_TYPE+
−
 2) remove lambdas from both sides: lambda_rsp_tac+
−
 3) remove Ball/Bex from the right hand side+
−
 4) use user-supplied RSP theorems+
−
 5) remove rep_abs from the right side+
−
 6) reflexivity of equality+
−
 7) split applications of lifted type (apply_rsp)+
−
 8) split applications of non-lifted type (cong_tac)+
−
 9) apply extentionality+
−
 A) reflexivity of the relation+
−
 B) assumption+
−
    (Lambdas under respects may have left us some assumptions)+
−
 C) proving obvious higher order equalities by simplifying fun_rel+
−
    (not sure if it is still needed?)+
−
 D) unfolding lambda on one side+
−
 E) simplifying (= ===> =) for simpler respectfulness+
−
*)+
−
+
−
+
−
fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>+
−
(case (bare_concl goal) of+
−
    (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)+
−
  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)+
−
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam+
−
+
−
    (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)+
−
| (Const (@{const_name "op ="},_) $+
−
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $+
−
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))+
−
      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}+
−
+
−
    (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)+
−
| (Const (@{const_name fun_rel}, _) $ _ $ _) $+
−
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $+
−
    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)+
−
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam+
−
+
−
    (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)+
−
| Const (@{const_name "op ="},_) $+
−
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $+
−
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)+
−
      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}+
−
+
−
    (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)+
−
| (Const (@{const_name fun_rel}, _) $ _ $ _) $+
−
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $+
−
    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)+
−
      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam+
−
+
−
| (_ $+
−
    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $+
−
    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))+
−
      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]+
−
+
−
| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => +
−
   (rtac @{thm refl} ORELSE'+
−
    (equals_rsp_tac R ctxt THEN' RANGE [+
−
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))+
−
+
−
    (* reflexivity of operators arising from Cong_tac *)+
−
| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}+
−
+
−
   (* respectfulness of constants; in particular of a simple relation *)+
−
| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)+
−
    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt+
−
+
−
    (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)+
−
    (* observe fun_map *)+
−
| _ $ _ $ _+
−
    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) +
−
       ORELSE' rep_abs_rsp_tac ctxt+
−
+
−
| _ => K no_tac+
−
) i)+
−
+
−
fun inj_repabs_step_tac ctxt rel_refl =+
−
 FIRST' [+
−
    inj_repabs_tac_match ctxt,+
−
    (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)+
−
    +
−
    apply_rsp_tac ctxt THEN'+
−
                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],+
−
+
−
    (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)+
−
    (* merge with previous tactic *)+
−
    Cong_Tac.cong_tac @{thm cong} THEN'+
−
                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],+
−
    +
−
    (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)+
−
    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,+
−
    +
−
    (* resolving with R x y assumptions *)+
−
    atac,+
−
    +
−
    (* reflexivity of the basic relations *)+
−
    (* R ... ... *)+
−
    resolve_tac rel_refl]+
−
+
−
fun inj_repabs_tac ctxt =+
−
let+
−
  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)+
−
in+
−
  simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) +
−
  THEN' inj_repabs_step_tac ctxt rel_refl+
−
end+
−
+
−
fun all_inj_repabs_tac ctxt =+
−
  REPEAT_ALL_NEW (inj_repabs_tac ctxt)+
−
+
−
+
−
(* Cleaning of the Theorem *)+
−
+
−
+
−
(* expands all fun_maps, except in front of bound variables *)+
−
fun fun_map_simple_conv xs ctrm =+
−
  case (term_of ctrm) of+
−
    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>+
−
        if (member (op=) xs h) +
−
        then Conv.all_conv ctrm+
−
        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm +
−
  | _ => Conv.all_conv ctrm+
−
+
−
fun fun_map_conv xs ctxt ctrm =+
−
  case (term_of ctrm) of+
−
      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv+
−
                fun_map_simple_conv xs) ctrm+
−
    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm+
−
    | _ => Conv.all_conv ctrm+
−
+
−
fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)+
−
+
−
fun mk_abs u i t =+
−
  if incr_boundvars i u aconv t then Bound i+
−
  else (case t of+
−
     t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)+
−
   | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')+
−
   | Bound j => if i = j then error "make_inst" else t+
−
   | _ => t)+
−
+
−
fun make_inst lhs t =+
−
let+
−
  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;+
−
  val _ $ (Abs (_, _, (_ $ g))) = t;+
−
in+
−
  (f, Abs ("x", T, mk_abs u 0 g))+
−
end+
−
+
−
fun make_inst_id lhs t =+
−
let+
−
  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;+
−
  val _ $ (Abs (_, _, g)) = t;+
−
in+
−
  (f, Abs ("x", T, mk_abs u 0 g))+
−
end+
−
+
−
(* Simplifies a redex using the 'lambda_prs' theorem.        *)+
−
(* First instantiates the types and known subterms.          *)+
−
(* Then solves the quotient assumptions to get Rep2 and Abs1 *)+
−
(* Finally instantiates the function f using make_inst       *)+
−
(* If Rep2 is identity then the pattern is simpler and       *)+
−
(* make_inst_id is used                                      *)+
−
fun lambda_prs_simple_conv ctxt ctrm =+
−
  case (term_of ctrm) of+
−
   (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>+
−
     (let+
−
       val thy = ProofContext.theory_of ctxt+
−
       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)+
−
       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)+
−
       val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]+
−
       val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]+
−
       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}+
−
       val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]+
−
       val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te+
−
       val make_inst = if ty_c = ty_d then make_inst_id else make_inst+
−
       val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)+
−
       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts+
−
     in+
−
       Conv.rewr_conv ti ctrm+
−
     end+
−
     handle _ => Conv.all_conv ctrm)+
−
  | _ => Conv.all_conv ctrm+
−
+
−
val lambda_prs_conv =+
−
  More_Conv.top_conv lambda_prs_simple_conv+
−
+
−
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)+
−
+
−
+
−
(* 1. folding of definitions and preservation lemmas;  *)+
−
(*    and simplification with                          *)+
−
(*    thm babs_prs all_prs ex_prs                      *)+
−
(*                                                     *) +
−
(* 2. unfolding of ---> in front of everything, except *)+
−
(*    bound variables (this prevents lambda_prs from   *)+
−
(*    becoming stuck                                   *)+
−
(*    thm fun_map.simps                                *)+
−
(*                                                     *)+
−
(* 3. simplification with                              *)+
−
(*    thm lambda_prs                                   *)+
−
(*                                                     *)+
−
(* 4. simplification with                              *)+
−
(*    thm Quotient_abs_rep Quotient_rel_rep id_simps   *) +
−
(*                                                     *)+
−
(* 5. Test for refl                                    *)+
−
+
−
fun clean_tac_aux lthy =+
−
  let+
−
    val thy = ProofContext.theory_of lthy;+
−
    val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)+
−
      (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)+
−
    +
−
    val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}+
−
    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) +
−
    fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver+
−
  in+
−
    EVERY' [simp_tac (simps thms1),+
−
            fun_map_tac lthy,+
−
            lambda_prs_tac lthy,+
−
            simp_tac (simps thms2),+
−
            TRY o rtac refl]+
−
  end+
−
+
−
fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)+
−
+
−
(* Tactic for Genralisation of Free Variables in a Goal *)+
−
+
−
fun inst_spec ctrm =+
−
   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}+
−
+
−
fun inst_spec_tac ctrms =+
−
  EVERY' (map (dtac o inst_spec) ctrms)+
−
+
−
fun all_list xs trm = +
−
  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm+
−
+
−
fun apply_under_Trueprop f = +
−
  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop+
−
+
−
fun gen_frees_tac ctxt =+
−
 SUBGOAL (fn (concl, i) =>+
−
  let+
−
    val thy = ProofContext.theory_of ctxt+
−
    val vrs = Term.add_frees concl []+
−
    val cvrs = map (cterm_of thy o Free) vrs+
−
    val concl' = apply_under_Trueprop (all_list vrs) concl+
−
    val goal = Logic.mk_implies (concl', concl)+
−
    val rule = Goal.prove ctxt [] [] goal +
−
      (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))+
−
  in+
−
    rtac rule i+
−
  end)  +
−
+
−
+
−
(* The General Shape of the Lifting Procedure *)+
−
+
−
(* - A is the original raw theorem                       *)+
−
(* - B is the regularized theorem                        *)+
−
(* - C is the rep/abs injected version of B              *)+
−
(* - D is the lifted theorem                             *)+
−
(*                                                       *)+
−
(* - 1st prem is the regularization step                 *)+
−
(* - 2nd prem is the rep/abs injection step              *)+
−
(* - 3rd prem is the cleaning part                       *)+
−
(*                                                       *)+
−
(* the QUOT_TRUE premise in 2 records the lifted theorem *)+
−
+
−
val lifting_procedure = +
−
   @{lemma  "[|A; +
−
               A --> B; +
−
               QUOT_TRUE D ==> B = C; +
−
               C = D|] ==> D" +
−
      by (simp add: QUOT_TRUE_def)}+
−
+
−
fun lift_match_error ctxt fun_str rtrm qtrm =+
−
let+
−
  val rtrm_str = Syntax.string_of_term ctxt rtrm+
−
  val qtrm_str = Syntax.string_of_term ctxt qtrm+
−
  val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, +
−
             "", "does not match with original theorem", rtrm_str]+
−
in+
−
  error msg+
−
end+
−
 +
−
fun procedure_inst ctxt rtrm qtrm =+
−
let+
−
  val thy = ProofContext.theory_of ctxt+
−
  val rtrm' = HOLogic.dest_Trueprop rtrm+
−
  val qtrm' = HOLogic.dest_Trueprop qtrm+
−
  val reg_goal = +
−
        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')+
−
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm+
−
  val inj_goal = +
−
        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))+
−
        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm+
−
in+
−
  Drule.instantiate' []+
−
    [SOME (cterm_of thy rtrm'),+
−
     SOME (cterm_of thy reg_goal),+
−
     NONE,+
−
     SOME (cterm_of thy inj_goal)] lifting_procedure+
−
end+
−
+
−
+
−
(* the tactic leaves three subgoals to be proved *)+
−
fun procedure_tac ctxt rthm =+
−
  ObjectLogic.full_atomize_tac+
−
  THEN' gen_frees_tac ctxt+
−
  THEN' CSUBGOAL (fn (goal, i) =>+
−
    let+
−
      val rthm' = atomize_thm rthm+
−
      val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)+
−
    in+
−
      (rtac rule THEN' rtac rthm') i+
−
    end)+
−
+
−
+
−
(* Automatic Proofs *)+
−
+
−
val msg1 = "Regularize proof failed."+
−
val msg2 = cat_lines ["Injection proof failed.", +
−
                      "This is probably due to missing respects lemmas.",+
−
                      "Try invoking the injection method manually to see", +
−
                      "which lemmas are missing."]+
−
val msg3 = "Cleaning proof failed."+
−
+
−
fun lift_tac ctxt rthm =+
−
  procedure_tac ctxt rthm+
−
  THEN' RANGE_WARN +
−
     [(regularize_tac ctxt, msg1),+
−
      (all_inj_repabs_tac ctxt, msg2),+
−
      (clean_tac ctxt, msg3)]+
−
+
−
end; (* structure *)+
−