--- a/FSet.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/FSet.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -295,8 +295,7 @@
 
 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}
-  @ @{thms ho_all_prs ho_ex_prs} *}
+  @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
 
 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"; *}

--- a/IntEx.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/IntEx.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -134,7 +134,7 @@
 
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
-ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms ho_plus_rsp} *}
 ML {* val defs = @{thms PLUS_def} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}

--- a/LFex.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/LFex.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -492,6 +492,21 @@
 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *}) apply (rule refl)
 done
 
+(* Does not work:
+lemma
+  assumes a0: "P1 TYP"
+  and     a1: "\<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind)"
+  and     a2: "\<And>id. P2 (TCONST id)"
+  and     a3: "\<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm)"
+  and     a4: "\<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2)"
+  and     a5: "\<And>id. P3 (CONS id)"
+  and     a6: "\<And>name. P3 (VAR name)"
+  and     a7: "\<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2)"
+  and     a8: "\<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)"
+  shows "P1 mkind \<and> P2 mty \<and> P3 mtrm"
+using a0 a1 a2 a3 a4 a5 a6 a7 a8
+*)
+
 lemma "\<lbrakk>P1 TYP;
   \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind);
   \<And>id. P2 (TCONST id);
@@ -501,6 +516,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
+
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}

--- a/LamEx.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/LamEx.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -171,8 +171,7 @@
 
 ML {* val qty = @{typ "lam"} *}
 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @
-  @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}

--- a/QuotMain.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -136,6 +136,7 @@
 
 end
 
+(* EQUALS_RSP is stronger *)
 lemma equiv_trans2:
   assumes e: "EQUIV R"
   and     ac: "R a c"
@@ -927,13 +928,13 @@
     NDT ctxt "2" (lambda_res_tac ctxt),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    NDT ctxt "3" (rtac @{thm ball_rsp}),
 
     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
     NDT ctxt "4" (ball_rsp_tac ctxt),
 
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+    NDT ctxt "5" (rtac @{thm bex_rsp}),
 
     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
     NDT ctxt "6" (bex_rsp_tac ctxt),
@@ -1030,8 +1031,7 @@
 
 ML {*
 fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot)
+  (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
 *}
 
 (* Rewrites the term with LAMBDA_PRS thm.

--- a/QuotScript.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/QuotScript.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -223,6 +223,7 @@
 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
 by blast
 
+(* TODO: it is the same as APPLY_RSP *)
 (* q1 and q2 not used; see next lemma *)
 lemma FUN_REL_MP:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
@@ -430,6 +431,17 @@
 
 
 
+
+
+lemma COND_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "(if a then b else c) = absf (if a then repf b else repf c)"
+  using a unfolding QUOTIENT_def by auto
+
+
+
+
+
 (* Set of lemmas for regularisation of ball and bex *)
 lemma ball_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
@@ -525,49 +537,29 @@
   "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
 
-
-
-(* TODO: Add similar *)
-lemma RES_FORALL_RSP:
-  shows "\<And>f g. (R ===> (op =)) f g ==>
-        (Ball (Respects R) f = Ball (Respects R) g)"
-  apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
-  done
+(* 2 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "Ball (Respects R) f = Ball (Respects R) g"
+  using a by (simp add: Ball_def IN_RESPECTS)
 
-lemma RES_EXISTS_RSP:
-  shows "\<And>f g. (R ===> (op =)) f g ==>
-        (Bex (Respects R) f = Bex (Respects R) g)"
-  apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
-  done
+lemma bex_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex (Respects R) f = Bex (Respects R) g)"
+  using a by (simp add: Bex_def IN_RESPECTS)
 
-
-lemma FORALL_PRS:
+(* 2 lemmas needed for cleaning of quantifiers *)
+lemma all_prs:
   assumes a: "QUOTIENT R absf repf"
-  shows "All f = Ball (Respects R) ((absf ---> id) f)"
-  using a
-  unfolding QUOTIENT_def
+  shows "Ball (Respects R) ((absf ---> id) f) = All f"
+  using a unfolding QUOTIENT_def
   by (metis IN_RESPECTS fun_map.simps id_apply)
 
-lemma EXISTS_PRS:
-  assumes a: "QUOTIENT R absf repf"
-  shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
-  using a
-  unfolding QUOTIENT_def
-  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-
-lemma COND_PRS:
+lemma ex_prs:
   assumes a: "QUOTIENT R absf repf"
-  shows "(if a then b else c) = absf (if a then repf b else repf c)"
-  using a unfolding QUOTIENT_def by auto
-
-(* These are the fixed versions, general ones need to be proved. *)
-lemma ho_all_prs:
-  shows "((op = ===> op =) ===> op =) All All"
-  by auto
-
-lemma ho_ex_prs:
-  shows "((op = ===> op =) ===> op =) Ex Ex"
-  by auto
+  shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+  using a unfolding QUOTIENT_def
+  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
 
 end