# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264499624 -3600
# Node ID da5e4b8317c77985fe5929a6c0e5cca9e1c4c1b8
# Parent  c96e007b512ffb7bf0530dd25bbe613a91afa0ba# Parent  0879d144aaa3961fda32ba2db8def0282e341223
merged

diff -r c96e007b512f -r da5e4b8317c7 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -377,22 +377,6 @@
 apply(assumption)
 done
 
-lemma [quot_respect]:
-  "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"
-apply(simp)
-done
-
-thm quot_preserve
-term split
-
-
-lemma [quot_preserve]:
-  shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"
-apply(simp add: expand_fun_eq)
-apply(simp add: Quotient_abs_rep[OF Quotient_fset])
-done
-
-
 lemma test: "All (\<lambda>(x::'a list, y). x = y)"
 sorry
 
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -72,11 +72,9 @@
 where
   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
 
-lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
-  apply (rule eq_reflection)
-  apply (rule ext)+
-  apply auto
-  done
+lemma eq_comp_r: 
+  shows "((op =) OOO R) = R"
+  by (auto simp add: expand_fun_eq)
 
 section {* Respects predicate *}
 
@@ -108,8 +106,8 @@
   by (simp add: expand_fun_eq id_def)
 
 lemma fun_rel_eq:
-  shows "(op =) ===> (op =) \<equiv> (op =)"
-  by (rule eq_reflection) (simp add: expand_fun_eq)
+  shows "((op =) ===> (op =)) = (op =)"
+  by (simp add: expand_fun_eq)
 
 lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
@@ -396,10 +394,9 @@
 lemma babs_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
-  shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f"
-  apply(rule eq_reflection)
-  apply(rule ext)
-  apply simp
+  shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
+  apply (rule ext)
+  apply (simp)
   apply (subgoal_tac "Rep1 x \<in> Respects R1")
   apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   apply (simp add: in_respects Quotient_rel_rep[OF q1])
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotList.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -1,4 +1,4 @@
-theory QuotList
+ theory QuotList
 imports QuotMain List
 begin
 
@@ -17,13 +17,13 @@
 text {* should probably be in Sum_Type.thy *}
 lemma split_list_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
-lemma map_id[id_simps]: "map id \<equiv> id"
-  apply(rule eq_reflection)
+lemma map_id[id_simps]: 
+  shows "map id = id"
   apply(simp add: expand_fun_eq)
   apply(rule allI)
   apply(induct_tac x)
@@ -112,8 +112,8 @@
 
 lemma nil_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
-  shows "map Abs [] \<equiv> []"
-  by (simp)
+  shows "map Abs [] = []"
+  by simp
 
 lemma nil_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
@@ -215,8 +215,7 @@
   done
 
 lemma list_rel_eq[id_simps]:
-  shows "list_rel (op =) \<equiv> (op =)"
-  apply(rule eq_reflection)
+  shows "(list_rel (op =)) = (op =)"
   unfolding expand_fun_eq
   apply(rule allI)+
   apply(induct_tac x xa rule: list_induct2')
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotMain.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -47,8 +47,7 @@
 qed
 
 theorem thm10:
-  shows "abs (rep a) \<equiv> a"
-  apply  (rule eq_reflection)
+  shows "abs (rep a) = a"
   unfolding abs_def rep_def
 proof -
   from rep_prop
@@ -112,10 +111,10 @@
 text {* Lemmas about simplifying id's. *}
 lemmas [id_simps] =
   id_def[symmetric]
-  fun_map_id[THEN eq_reflection]
+  fun_map_id
   id_apply[THEN eq_reflection]
-  id_o[THEN eq_reflection]
-  o_id[THEN eq_reflection]
+  id_o
+  o_id
   eq_comp_r
 
 text {* Translation functions for the lifting process. *}
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotOption.thy
--- a/Quot/QuotOption.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotOption.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -70,13 +70,11 @@
   done
 
 lemma option_map_id[id_simps]: 
-  shows "Option.map id \<equiv> id"
-  apply (rule eq_reflection)
+  shows "Option.map id = id"
   by (simp add: expand_fun_eq split_option_all)
 
 lemma option_rel_eq[id_simps]: 
-  shows "option_rel (op =) \<equiv> (op =)"
-  apply(rule eq_reflection)
+  shows "option_rel (op =) = (op =)"
   by (simp add: expand_fun_eq split_option_all)
 
 end
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotProd.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -82,14 +82,23 @@
   apply(simp add: Quotient_abs_rep[OF q2])
   done
 
+lemma split_rsp[quot_respect]:
+  shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
+  by auto
+  
+lemma split_prs[quot_preserve]:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
 lemma prod_fun_id[id_simps]: 
-  shows "prod_fun id id \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
+  shows "prod_fun id id = id"
+  by (simp add: prod_fun_def)
 
 lemma prod_rel_eq[id_simps]: 
-  shows "prod_rel (op =) (op =) \<equiv> (op =)"
-  apply (rule eq_reflection)
-  apply (simp add: expand_fun_eq)
-  done
+  shows "prod_rel (op =) (op =) = (op =)"
+  by (simp add: expand_fun_eq)
+ 
 
 end
diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotSum.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -84,15 +84,11 @@
   done
 
 lemma sum_map_id[id_simps]: 
-  shows "sum_map id id \<equiv> id"
-  apply (rule eq_reflection)
-  apply (simp add: expand_fun_eq split_sum_all)
-  done
+  shows "sum_map id id = id"
+  by (simp add: expand_fun_eq split_sum_all)
 
 lemma sum_rel_eq[id_simps]: 
-  shows "sum_rel (op =) (op =) \<equiv> (op =)"
-  apply (rule eq_reflection)
-  apply(simp add: expand_fun_eq split_sum_all)
-  done
+  shows "sum_rel (op =) (op =) = (op =)"
+  by (simp add: expand_fun_eq split_sum_all)
 
 end
diff -r c96e007b512f -r da5e4b8317c7 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 10:53:44 2010 +0100
@@ -526,8 +526,7 @@
 
   fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs})
-  val ss2 = mk_simps (@{thms Quotient_abs_rep[THEN eq_reflection] 
-                             Quotient_rel_rep[THEN eq_reflection] ex1_prs} @ ids)
+  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids)
 in
   EVERY' [simp_tac ss1,
           fun_map_tac lthy,