
diff -r c129354f2ff6 -r 3104d62e7a16 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 17 14:58:33 2009 +0100
@@ -3,6 +3,8 @@
 uses ("quotient_info.ML")
      ("quotient_typ.ML")
      ("quotient_def.ML")
+     ("quotient_term.ML")
+     ("quotient_tacs.ML")
 begin
 
 locale QUOT_TYPE =
@@ -107,36 +109,31 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
-section {* Simset setup *}
+(* the translation functions *)
+use "quotient_term.ML" 
 
-(* Since HOL_basic_ss is too "big" for us, *)
-(* we set up our own minimal simpset.      *)
-ML {*
-fun  mk_minimal_ss ctxt =
-  Simplifier.context ctxt empty_ss
-    setsubgoaler asm_simp_tac
-    setmksimps (mksimps [])
-*}
+(* tactics *)
+lemma eq_imp_rel:  
+  "equivp R ==> a = b --> R a b" 
+by (simp add: equivp_reflp)
 
-ML {*
-fun OF1 thm1 thm2 = thm2 RS thm1
-*}
+definition
+  "QUOT_TRUE x \<equiv> True"
 
-(* various tactic combinators *)
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
-*}
+lemma quot_true_dests:
+  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
+  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
+  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
+  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
+by (simp_all add: QUOT_TRUE_def ext)
 
-ML {*
-(* 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)
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
 
-fun RANGE_WARN xs = RANGE (map WARN xs)
-*}
+lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+  by(auto simp add: QUOT_TRUE_def)
 
+use "quotient_tacs.ML"
 
 section {* Atomize Infrastructure *}
 
@@ -160,16 +157,6 @@
   then show "A \<equiv> B" by (rule eq_reflection)
 qed
 
-ML {*
-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
-*}
-
 section {* Infrastructure about id *}
 
 lemmas [id_simps] =
@@ -177,902 +164,6 @@
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
 
-section {* Computation of the Regularize Goal *} 
-
-(*
-Regularizing an rtrm means:
- - quantifiers over a type that needs lifting are replaced by
-   bounded quantifiers, for example:
-      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
-
-   the relation R is given by the rty and qty;
- 
- - abstractions over a type that needs lifting are replaced
-   by bounded abstractions:
-      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
-
- - equalities over the type being lifted are replaced by
-   corresponding relations:
-      A = B     \<Longrightarrow>     A \<approx> B
-
-   example with more complicated types of A, B:
-      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
-*)
-
-ML {*
-(* builds the relation that is the argument of respects *)
-fun mk_resp_arg lthy (rty, qty) =
-let
-  val thy = ProofContext.theory_of lthy
-in  
-  if rty = qty
-  then HOLogic.eq_const rty
-  else
-    case (rty, qty) of
-      (Type (s, tys), Type (s', tys')) =>
-       if s = s' 
-       then let
-              val SOME map_info = maps_lookup thy s
-              val args = map (mk_resp_arg lthy) (tys ~~ tys')
-            in
-              list_comb (Const (#relfun map_info, dummyT), args) 
-            end  
-       else let  
-              val SOME qinfo = quotdata_lookup_thy thy s'
-              (* FIXME: check in this case that the rty and qty *)
-              (* FIXME: correspond to each other *)
-              val (s, _) = dest_Const (#rel qinfo)
-              (* FIXME: the relation should only be the string        *)
-              (* FIXME: and the type needs to be calculated as below; *)
-              (* FIXME: maybe one should actually have a term         *)
-              (* FIXME: and one needs to force it to have this type   *)
-            in
-              Const (s, rty --> rty --> @{typ bool})
-            end
-      | _ => HOLogic.eq_const dummyT 
-             (* FIXME: check that the types correspond to each other? *)
-end
-*}
-
-ML {*
-val mk_babs = Const (@{const_name Babs}, dummyT)
-val mk_ball = Const (@{const_name Ball}, dummyT)
-val mk_bex  = Const (@{const_name Bex}, dummyT)
-val mk_resp = Const (@{const_name Respects}, dummyT)
-*}
-
-ML {*
-(* - applies f to the subterm of an abstraction,   *)
-(*   otherwise to the given term,                  *)
-(* - used by regularize, therefore abstracted      *)
-(*   variables do not have to be treated specially *)
-
-fun apply_subt f trm1 trm2 =
-  case (trm1, trm2) of
-    (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
-  | _ => f trm1 trm2
-
-(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)  
-*}
-
-ML {*
-(* produces a regularized version of rtrm     *)
-(* - the result is contains dummyT            *)
-(* - does not need any special treatment of   *)
-(*   bound variables                          *)
-
-fun regularize_trm lthy rtrm qtrm =
-  case (rtrm, qtrm) of
-    (Abs (x, ty, t), Abs (x', ty', t')) =>
-       let
-         val subtrm = Abs(x, ty, regularize_trm lthy t t')
-       in
-         if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
-       end
-
-  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm lthy) t t'
-       in
-         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
-
-  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm lthy) t t'
-       in
-         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
-
-  | (* equalities need to be replaced by appropriate equivalence relations *) 
-    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
-         if ty = ty' then rtrm
-         else mk_resp_arg lthy (domain_type ty, domain_type ty') 
-
-  | (* in this case we check whether the given equivalence relation is correct *) 
-    (rel, Const (@{const_name "op ="}, ty')) =>
-       let 
-         val exc = LIFT_MATCH "regularise (relation mismatch)"
-         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
-         val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
-       in 
-         if rel' = rel then rtrm else raise exc
-       end  
-
-  | (_, Const _) =>
-       let 
-         fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
-           | same_name _ _ = false
-          (* TODO/FIXME: This test is not enough. *) 
-          (*             Why?                     *)
-          (* Because constants can have the same name but not be the same
-             constant.  All overloaded constants have the same name but because
-             of different types they do differ.
-        
-             This code will let one write a theorem where plus on nat is
-             matched to plus on int, even if the latter is defined differently.
-    
-             This would result in hard to understand failures in injection and
-             cleaning. *)
-           (* cu: if I also test the type, then something else breaks *)
-       in
-         if same_name rtrm qtrm then rtrm
-         else 
-           let 
-             val thy = ProofContext.theory_of lthy
-             val qtrm_str = Syntax.string_of_term lthy qtrm
-             val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
-             val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
-             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
-           in 
-             if Pattern.matches thy (rtrm', rtrm) 
-             then rtrm else raise exc2
-           end
-       end 
-
-  | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
-
-  | (Free (x, ty), Free (x', ty')) => 
-       (* this case cannot arrise as we start with two fully atomized terms *)
-       raise (LIFT_MATCH "regularize (frees)")
-
-  | (Bound i, Bound i') =>
-       if i = i' then rtrm 
-       else raise (LIFT_MATCH "regularize (bounds mismatch)")
-
-  | _ =>
-       let 
-         val rtrm_str = Syntax.string_of_term lthy rtrm
-         val qtrm_str = Syntax.string_of_term lthy qtrm
-       in
-         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
-       end
-*}
-
-section {* Regularize Tactic *}
-
-ML {*
-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
-*}
-
-ML {*
-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)
-*}
-
-ML {*
-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
-*}
-
-ML {*
-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? *)
-*}
-
-ML {*
-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
-*}
-
-lemma eq_imp_rel: 
-  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: equivp_reflp)
-
-ML {*
-(* 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
-*}
-
-ML {*
-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 *)
-
-ML {*
-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
-*}
-
-section {* Calculation of the Injected Goal *}
-
-(*
-Injecting repabs means:
-
-  For abstractions:
-  * If the type of the abstraction doesn't need lifting we recurse.
-  * If it does we add RepAbs around the whole term and check if the
-    variable needs lifting.
-    * If it doesn't then we recurse
-    * If it does we recurse and put 'RepAbs' around all occurences
-      of the variable in the obtained subterm. This in combination
-      with the RepAbs above will let us change the type of the
-      abstraction with rewriting.
-  For applications:
-  * If the term is 'Respects' applied to anything we leave it unchanged
-  * If the term needs lifting and the head is a constant that we know
-    how to lift, we put a RepAbs and recurse
-  * If the term needs lifting and the head is a free applied to subterms
-    (if it is not applied we treated it in Abs branch) then we
-    put RepAbs and recurse
-  * Otherwise just recurse.
-*)
-
-ML {*
-fun mk_repabs lthy (T, T') trm = 
-  Quotient_Def.get_fun repF lthy (T, T') 
-    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
-*}
-
-ML {*
-(* bound variables need to be treated properly,    *)
-(* as the type of subterms need to be calculated   *)
-(* in the abstraction case                         *)
-
-fun inj_repabs_trm lthy (rtrm, qtrm) =
- case (rtrm, qtrm) of
-    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-
-  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-
-  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
-      let
-        val rty = fastype_of rtrm
-        val qty = fastype_of qtrm
-      in
-        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
-      end
-
-  | (Abs (x, T, t), Abs (x', T', t')) =>
-      let
-        val rty = fastype_of rtrm
-        val qty = fastype_of qtrm
-        val (y, s) = Term.dest_abs (x, T, t)
-        val (_, s') = Term.dest_abs (x', T', t')
-        val yvar = Free (y, T)
-        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
-      in
-        if rty = qty then result
-        else mk_repabs lthy (rty, qty) result
-      end
-
-  | (t $ s, t' $ s') =>  
-       (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
-
-  | (Free (_, T), Free (_, T')) => 
-        if T = T' then rtrm 
-        else mk_repabs lthy (T, T') rtrm
-
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
-
-  | (_, Const (_, T')) =>
-      let
-        val rty = fastype_of rtrm
-      in 
-        if rty = T' then rtrm
-        else mk_repabs lthy (rty, T') rtrm
-      end   
-  
-  | _ => raise (LIFT_MATCH "injection")
-*}
-
-section {* Injection Tactic *}
-
-definition
-  "QUOT_TRUE x \<equiv> True"
-
-ML {*
-(* looks for QUOT_TRUE assumtions, and in case its argument    *)
-(* 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
-*}
-
-text {*
-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
-*}
-
-lemma quot_true_dests:
-  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
-  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
-  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
-  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
-by (simp_all add: QUOT_TRUE_def ext)
-
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (simp add: QUOT_TRUE_def)
-
-lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
-  by(auto simp add: QUOT_TRUE_def)
-
-ML {*
-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
-*}
-
-ML {*
-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
-*}
-
-ML {*
-fun quot_true_tac ctxt fnctn = 
-   CONVERSION
-    ((Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
-*}
-
-ML {* fun dest_comb (f $ a) = (f, a) *}
-ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
-(* TODO: Can this be done easier? *)
-ML {*
-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)))
-*}
-
-ML {*
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-*}
-
-ML {*
-val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
-*}
-
-ML {*
-(* 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)
-*}
-
-thm equals_rsp
-
-ML {*
-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
-*}
-
-ML {*
-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)
-*}
-
-ML {*
-fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
-(case (bare_concl goal) of
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
-  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
-    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-| (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\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>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\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-| 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\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>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 (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
-    (* observe ---> *)
-| _ $ _ $ _
-    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) 
-       ORELSE' rep_abs_rsp_tac ctxt
-
-| _ => K no_tac
-) i)
-*}
-
-ML {*
-fun inj_repabs_step_tac ctxt rel_refl =
-  (FIRST' [
-    inj_repabs_tac_match ctxt,
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> 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 $ \<dots>) (t' $ \<dots>) ----> 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 =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
-    
-    (* resolving with R x y assumptions *)
-    atac,
-    
-    (* reflexivity of the basic relations *)
-    (* R \<dots> \<dots> *)
-    resolve_tac rel_refl])
-*}
-
-ML {*
-fun inj_repabs_tac ctxt =
-let
-  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
-in
-  inj_repabs_step_tac ctxt rel_refl
-end
-
-fun all_inj_repabs_tac ctxt =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt)
-*}
-
-section {* Cleaning of the Theorem *}
-
-ML {*
-(* expands all fun_maps, except in front of bound variables *)
-
-fun fun_map_simple_conv xs ctxt 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 ctxt) 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)
-*}
-
-ML {* 
-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
-*}
-
-ML {*
-(* 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
-*}
-
-ML {*
-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 *)
-
-ML {*
-fun clean_tac 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
-*}
-
-section {* Tactic for Genralisation of Free Variables in a Goal *}
-
-ML {*
-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)  
-*}
-
-section {* 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 *)
-
-ML {*
-val lifting_procedure = 
-   @{lemma  "\<lbrakk>A; 
-              A \<longrightarrow> B; 
-              QUOT_TRUE D \<Longrightarrow> B = C; 
-              C = D\<rbrakk> \<Longrightarrow> D" 
-             by (simp add: QUOT_TRUE_def)}
-*}
-
-ML {*
-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
-*}
-
-ML {* 
-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
-*}
-
-ML {*
-(* 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)
-*}
-
-section {* Automatic Proofs *}
-
-
-ML {*
-local
-
-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."
-
-in
-
-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
-*}
-
 section {* Methods / Interface *}
 
 ML {*
@@ -1084,23 +175,23 @@
 *}
 
 method_setup lifting =
-  {* Attrib.thm >> (mk_method1 lift_tac) *}
+  {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
   {* Lifting of theorems to quotient types. *}
 
 method_setup lifting_setup =
-  {* Attrib.thm >> (mk_method1 procedure_tac) *}
+  {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
   {* Sets up the three goals for the lifting procedure. *}
 
 method_setup regularize =
-  {* Scan.succeed (mk_method2 regularize_tac)  *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac)  *}
   {* Proves automatically the regularization goals from the lifting procedure. *}
 
 method_setup injection =
-  {* Scan.succeed (mk_method2 all_inj_repabs_tac) *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *}
   {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
 
 method_setup cleaning =
-  {* Scan.succeed (mk_method2 clean_tac) *}
+  {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
   {* Proves automatically the cleaning goals from the lifting procedure. *}
 
 end




