# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259463558 -3600
# Node ID 2dc708ddb93ab08136724b5492f534b42a413ad1
# Parent  b5e7e73bf31d62cdec89737e5c3af0d0e113b3df
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]

diff -r b5e7e73bf31d -r 2dc708ddb93a FSet.thy
--- a/FSet.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/FSet.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -178,37 +178,38 @@
 
 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
 
-lemma memb_rsp:
+lemma memb_rsp[quot_rsp]:
   fixes z
-  assumes a: "list_eq x y"
+  assumes a: "x \<approx> y"
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
-lemma ho_memb_rsp:
+lemma ho_memb_rsp[quot_rsp]:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
-lemma card1_rsp:
+lemma card1_rsp[quot_rsp]:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
+lemma ho_card1_rsp[quot_rsp]: 
+  "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp:
+lemma cons_rsp[quot_rsp]:
   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:
+lemma ho_cons_rsp[quot_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
 lemma append_rsp_fst:
-  assumes a : "list_eq l1 l2"
+  assumes a : "l1 \<approx> l2"
   shows "(l1 @ s) \<approx> (l2 @ s)"
   using a
   by (induct) (auto intro: list_eq.intros list_eq_refl)
@@ -245,9 +246,9 @@
   apply (rule rev_rsp)
   done
 
-lemma append_rsp:
-  assumes a : "list_eq l1 r1"
-  assumes b : "list_eq l2 r2 "
+lemma append_rsp[quot_rsp]:
+  assumes a : "l1 \<approx> r1"
+  assumes b : "l2 \<approx> r2 "
   shows "(l1 @ l2) \<approx> (r1 @ r2)"
   apply (rule list_eq.intros(6))
   apply (rule append_rsp_fst)
@@ -260,11 +261,11 @@
   apply (rule append_sym_rsp)
   done
 
-lemma ho_append_rsp:
+lemma ho_append_rsp[quot_rsp]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
-lemma map_rsp:
+lemma map_rsp[quot_rsp]:
   assumes a: "a \<approx> b"
   shows "map f a \<approx> map f b"
   using a
@@ -272,16 +273,15 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma ho_map_rsp:
+lemma ho_map_rsp[quot_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: map_rsp)
 
 lemma map_append:
-  "(map f (a @ b)) \<approx>
-  (map f a) @ (map f b)"
+  "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma ho_fold_rsp:
+lemma ho_fold_rsp[quot_rsp]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto simp add: FUN_REL_EQ)
   apply (case_tac "rsp_fold x")
@@ -295,7 +295,6 @@
 
 print_quotients
 
-
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val rsp_thms =
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
@@ -304,7 +303,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma "IN x EMPTY = False"
 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
@@ -328,7 +327,7 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
@@ -393,9 +392,6 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 quotient_def
@@ -409,21 +405,21 @@
   "fset_case \<equiv> list_case"
 
 (* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp:
+lemma list_rec_rsp[quot_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto simp add: FUN_REL_EQ)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
-lemma list_case_rsp:
+lemma list_case_rsp[quot_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
   apply (auto simp add: FUN_REL_EQ)
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
@@ -443,7 +439,7 @@
   apply (assumption)
   done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 (* Construction site starts here *)
 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"
diff -r b5e7e73bf31d -r 2dc708ddb93a IntEx.thy
--- a/IntEx.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/IntEx.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -128,9 +128,9 @@
   apply(auto)
   done
 
-lemma ho_plus_rsp:
-  "(intrel ===> intrel ===> intrel) my_plus my_plus"
-  by (simp)
+lemma ho_plus_rsp[quot_rsp]:
+  shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
+by (simp)
 
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
@@ -140,10 +140,10 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 
 lemma "PLUS a b = PLUS b a"
@@ -199,17 +199,19 @@
 apply simp
 done
 
-lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
+(* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *)
+lemma map_prs: 
+  "map REP_my_int (map ABS_my_int x) = x"
 sorry
 
-lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
+lemma foldl_prs[quot_rsp]: 
+  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
 sorry
 
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(rule foldl_prs) 
 apply(simp add: map_prs)
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
diff -r b5e7e73bf31d -r 2dc708ddb93a LFex.thy
--- a/LFex.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/LFex.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -181,22 +181,36 @@
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp: "(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp: "(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp: "(op = ===> atrm) Var Var" sorry
-lemma app_rsp: "(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp: "(op = ===> atrm) Const Const" sorry
-lemma lam_rsp: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
+lemma kpi_rsp[quot_rsp]: 
+  "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
+lemma tconst_rsp[quot_rsp]: 
+  "(op = ===> aty) TConst TConst" sorry
+lemma tapp_rsp[quot_rsp]: 
+  "(aty ===> atrm ===> aty) TApp TApp" sorry
+lemma tpi_rsp[quot_rsp]: 
+  "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
+lemma var_rsp[quot_rsp]: 
+  "(op = ===> atrm) Var Var" sorry
+lemma app_rsp[quot_rsp]: 
+  "(atrm ===> atrm ===> atrm) App App" sorry
+lemma const_rsp[quot_rsp]: 
+  "(op = ===> atrm) Const Const" sorry
+lemma lam_rsp[quot_rsp]: 
+  "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp: "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp: "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
+lemma perm_kind_rsp[quot_rsp]: 
+  "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
+lemma perm_ty_rsp[quot_rsp]: 
+  "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
+lemma perm_trm_rsp[quot_rsp]: 
+  "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp: "(atrm ===> op =) fv_trm fv_trm" sorry
+lemma fv_ty_rsp[quot_rsp]: 
+  "(aty ===> op =) fv_ty fv_ty" sorry
+lemma fv_kind_rsp[quot_rsp]: 
+  "(akind ===> op =) fv_kind fv_kind" sorry
+lemma fv_trm_rsp[quot_rsp]: 
+  "(atrm ===> op =) fv_trm fv_trm" sorry
 
 
 thm akind_aty_atrm.induct
@@ -269,197 +283,197 @@
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
   val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
 *}
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp} 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
 done
 
 print_quotients
diff -r b5e7e73bf31d -r 2dc708ddb93a QuotMain.thy
--- a/QuotMain.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -235,28 +235,30 @@
 
 section {* Debugging infrastructure for testing tactics *}
 
-ML {*
-fun fst_prem_str ctxt [] = "No subgoals" 
-  | fst_prem_str ctxt thms = (hd thms) |> Syntax.string_of_term ctxt
-*}
+
 
 ML {*
-fun my_print_tac ctxt s thm =
+fun my_print_tac ctxt s i thm =
 let
-  val _ = tracing (s ^ "\n" ^ (fst_prem_str ctxt (prems_of thm)))
+  val prem_str = nth (prems_of thm) (i - 1)
+                 |> Syntax.string_of_term ctxt
+                 handle Subscript => "no subgoal"
+  val _ = tracing (s ^ "\n" ^ prem_str)
 in
   Seq.single thm
-end
-*}
+end *}
+
 
 ML {*
 fun DT ctxt s tac i thm =
-   let
-     val fst_goal_start = fst_prem_str ctxt (prems_of thm)
-   in 
-     EVERY [tac i,
-            my_print_tac ctxt (cat_lines ["before: " ^ s, fst_goal_start, "after: " ^ s])] thm  
-   end
+let
+  val before_goal = nth (prems_of thm) (i - 1)
+                    |> Syntax.string_of_term ctxt
+  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
+                   |> cat_lines
+in 
+  EVERY [tac i, my_print_tac ctxt before_msg i] thm
+end
 
 fun NDT ctxt s tac thm = tac thm  
 *}
@@ -892,7 +894,7 @@
 *)
 
 ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -914,7 +916,7 @@
     NDT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of constants *)
-    DT ctxt "7" (resolve_tac rsp_thms),
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
 
     (* reflexivity of operators arising from Cong_tac *)
     NDT ctxt "8" (rtac @{thm refl}),
@@ -954,8 +956,8 @@
 *}
 
 ML {*
-fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
 *}
 
 
@@ -1194,7 +1196,7 @@
 
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rty quot rsp_thms defs =
+fun lift_tac lthy rthm rel_eqv rty quot defs =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1209,7 +1211,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               all_inj_repabs_tac lthy rty quot rel_refl trans2 rsp_thms,
+               all_inj_repabs_tac lthy rty quot rel_refl trans2,
                clean_tac lthy quot defs aps]]
     end) lthy
 *}
diff -r b5e7e73bf31d -r 2dc708ddb93a quotient_info.ML
--- a/quotient_info.ML	Sun Nov 29 02:51:42 2009 +0100
+++ b/quotient_info.ML	Sun Nov 29 03:59:18 2009 +0100
@@ -18,6 +18,8 @@
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
+
+  val rsp_rules_get: Proof.context -> thm list  
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -111,7 +113,7 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* information about quotient constants *)
+(* info about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term}
 
 structure QConstsData = Theory_Data
@@ -148,6 +150,15 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
+(* respectfulness lemmas *)
+structure RspRules = Named_Thms
+  (val name = "quot_rsp"
+   val description = "Respectfulness theorems.")
+
+val rsp_rules_get = RspRules.get
+
+val _ = Context.>> (Context.map_theory RspRules.setup)
+
 end; (* structure *)
 
 open Quotient_Info