--- a/Quot/Examples/FSet.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -177,7 +177,7 @@
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
-lemma ho_memb_rsp[quotient_rsp]:
+lemma ho_memb_rsp[quot_respect]:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
@@ -187,17 +187,17 @@
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp[quotient_rsp]: 
+lemma ho_card1_rsp[quot_respect]: 
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quotient_rsp]:
+lemma cons_rsp[quot_respect]:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule list_eq.intros(5))
 
-lemma ho_cons_rsp[quotient_rsp]:
+lemma ho_cons_rsp[quot_respect]:
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
@@ -254,7 +254,7 @@
   apply (rule append_sym_rsp)
   done
 
-lemma ho_append_rsp[quotient_rsp]:
+lemma ho_append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
@@ -266,7 +266,7 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma ho_map_rsp[quotient_rsp]:
+lemma ho_map_rsp[quot_respect]:
   "(op = ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: map_rsp)
 
@@ -274,7 +274,7 @@
   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma ho_fold_rsp[quotient_rsp]:
+lemma ho_fold_rsp[quot_respect]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto)
   apply (case_tac "rsp_fold x")
@@ -286,7 +286,7 @@
   apply (auto simp add: memb_rsp rsp_fold_def)
 done
 
-lemma list_equiv_rsp[quotient_rsp]:
+lemma list_equiv_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by (auto intro: list_eq.intros)
 
@@ -355,8 +355,6 @@
   apply (assumption)
   done
 
-thm quotient_thm
-
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
@@ -402,14 +400,14 @@
   "fset_case \<equiv> list_case"
 
 (* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quotient_rsp]:
+lemma list_rec_rsp[quot_respect]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
-lemma list_case_rsp[quotient_rsp]:
+lemma list_case_rsp[quot_respect]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
   apply (auto)
   sorry

--- a/Quot/Examples/IntEx.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -12,9 +12,9 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
-thm quotient_equiv
+thm quot_equiv
 
-thm quotient_thm
+thm quot_thm
 
 thm my_int_equivp
 
@@ -132,7 +132,7 @@
   apply(auto)
   done
 
-lemma plus_rsp[quotient_rsp]:
+lemma plus_rsp[quot_respect]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
@@ -171,8 +171,8 @@
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule impI)
 apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(injection)
+apply(cleaning)
 done
 
 
@@ -203,9 +203,7 @@
 done
 
 lemma "foldl PLUS x [] = x"
-apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(lifting rule: ho_tst)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -345,14 +343,10 @@
 done
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst4} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1*})
+apply(lifting rule: lam_tst4)
+apply(cleaning)
 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int])
-apply(tactic {* lambda_prs_tac @{context} 1 *})
-apply(rule refl)
+apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])
 done
 
 end

--- a/Quot/Examples/IntEx2.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -107,21 +107,21 @@
 
 thm add_assoc
 
-lemma plus_raw_rsp[quotient_rsp]:
+lemma plus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
 
-lemma minus_raw_rsp[quotient_rsp]:
+lemma minus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
   by auto
 
-lemma mult_raw_rsp[quotient_rsp]:
+lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(auto)
 apply(simp add: algebra_simps)
 sorry
 
-lemma le_raw_rsp[quotient_rsp]:
+lemma le_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 by auto
 

--- a/Quot/Examples/LFex.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/LFex.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -183,35 +183,35 @@
 end
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp[quotient_rsp]: 
+lemma kpi_rsp[quot_respect]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp[quotient_rsp]: 
+lemma tconst_rsp[quot_respect]: 
   "(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp[quotient_rsp]: 
+lemma tapp_rsp[quot_respect]: 
   "(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp[quotient_rsp]: 
+lemma tpi_rsp[quot_respect]: 
   "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp[quotient_rsp]: 
+lemma var_rsp[quot_respect]: 
   "(op = ===> atrm) Var Var" sorry
-lemma app_rsp[quotient_rsp]: 
+lemma app_rsp[quot_respect]: 
   "(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp[quotient_rsp]: 
+lemma const_rsp[quot_respect]: 
   "(op = ===> atrm) Const Const" sorry
-lemma lam_rsp[quotient_rsp]: 
+lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma perm_kind_rsp[quotient_rsp]: 
+lemma perm_kind_rsp[quot_respect]: 
   "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp[quotient_rsp]: 
+lemma perm_ty_rsp[quot_respect]: 
   "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp[quotient_rsp]: 
+lemma perm_trm_rsp[quot_respect]: 
   "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_ty_rsp[quotient_rsp]: 
+lemma fv_ty_rsp[quot_respect]: 
   "(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp[quotient_rsp]: 
+lemma fv_kind_rsp[quot_respect]: 
   "(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp[quotient_rsp]: 
+lemma fv_trm_rsp[quot_respect]: 
   "(atrm ===> op =) fv_trm fv_trm" sorry
 
 

--- a/Quot/Examples/LamEx.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -128,7 +128,7 @@
 unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp[quotient_rsp]:
+lemma perm_rsp[quot_respect]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp[quotient_rsp]:
+lemma rVar_rsp[quot_respect]:
   "(op = ===> alpha) rVar rVar"
 by (auto intro:a1)
 
-lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp"
 by (auto intro:a2)
 
-lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quot_respect]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"

--- a/Quot/QuotList.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/QuotList.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -12,7 +12,7 @@
 
 declare [[map list = (map, list_rel)]]
 
-lemma list_equivp[quotient_equiv]:
+lemma list_equivp[quot_equiv]:
   assumes a: "equivp R"
   shows "equivp (list_rel R)"
   unfolding equivp_def
@@ -40,7 +40,7 @@
   apply(metis)
   done
 
-lemma list_quotient[quotient_thm]:
+lemma list_quotient[quot_thm]:
   assumes q: "Quotient R Abs Rep"
   shows "Quotient (list_rel R) (map Abs) (map Rep)"
   unfolding Quotient_def
@@ -72,7 +72,7 @@
   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
 by (induct t) (simp_all add: Quotient_abs_rep[OF q])
 
-lemma cons_rsp[quotient_rsp]:
+lemma cons_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_rel R ===> list_rel R) op # op #"
 by (auto)
@@ -82,7 +82,7 @@
   shows "map Abs [] \<equiv> []"
 by (simp)
 
-lemma nil_rsp[quotient_rsp]:
+lemma nil_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "list_rel R [] []"
 by simp
@@ -93,7 +93,7 @@
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma map_rsp[quotient_rsp]:
+lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
@@ -131,7 +131,7 @@
          induct     doesn't accept 'rule'.
    that's why the proof uses manual generalisation and needs assumptions
    both in conclusion for induction and in assumptions. *)
-lemma foldl_rsp[quotient_rsp]:
+lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"

--- a/Quot/QuotMain.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -148,15 +148,15 @@
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
-lemmas [quotient_thm] =
+lemmas [quot_thm] =
   fun_quotient prod_quotient
 
-lemmas [quotient_rsp] =
+lemmas [quot_respect] =
   quot_rel_rsp pair_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
-lemmas [quotient_equiv] =
+lemmas [quot_equiv] =
   identity_equivp prod_equivp
 
 (* definition of the quotient types *)
@@ -1063,6 +1063,7 @@
     EVERY' [lambda_prs_tac lthy,
             simp_tac (simps thms1),
             simp_tac (simps thms2),
+            lambda_prs_tac lthy,
             TRY o rtac refl]
   end
 *}
@@ -1185,6 +1186,7 @@
                     (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
+(* methods / interface *)
 ML {*
 val rule_spec =  Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm
 

--- a/Quot/quotient_info.ML	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 17:30:00 2009 +0100
@@ -26,6 +26,7 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list  
+  val prs_rules_get: Proof.context -> thm list  
   val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
@@ -180,7 +181,7 @@
 
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
-  (val name = "quotient_equiv"
+  (val name = "quot_equiv"
    val description = "Equivalence relation theorems.")
 
 val equiv_rules_get = EquivRules.get
@@ -188,11 +189,18 @@
 
 (* respectfulness theorems *)
 structure RspRules = Named_Thms
-  (val name = "quotient_rsp"
+  (val name = "quot_respect"
    val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get
 
+(* preservation theorems *)
+structure PrsRules = Named_Thms
+  (val name = "quot_preserve"
+   val description = "Respectfulness theorems.")
+
+val prs_rules_get = PrsRules.get
+
 (* respectfulness theorems *)
 structure IdSimps = Named_Thms
   (val name = "id_simps"
@@ -202,7 +210,7 @@
 
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
-  (val name = "quotient_thm"
+  (val name = "quot_thm"
    val description = "Quotient theorems.")
 
 val quotient_rules_get = QuotientRules.get