# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265983580 -3600
# Node ID 36d596cb63a2f416339dda8948c48cc9787f1c21
# Parent  10a6ba364ce1b1b3db1b4d4b87b62e8dcc680184
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned

diff -r 10a6ba364ce1 -r 36d596cb63a2 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Fri Feb 12 12:06:09 2010 +0100
+++ b/Quot/Examples/FSet.thy	Fri Feb 12 15:06:20 2010 +0100
@@ -363,6 +363,11 @@
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
+lemma eq_imp_rel:
+  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+  by (simp add: equivp_reflp)
+
+
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
 apply(lifting hard)
 apply(regularize)
diff -r 10a6ba364ce1 -r 36d596cb63a2 Quot/Quotient.thy
--- a/Quot/Quotient.thy	Fri Feb 12 12:06:09 2010 +0100
+++ b/Quot/Quotient.thy	Fri Feb 12 15:06:20 2010 +0100
@@ -12,22 +12,23 @@
   ("quotient_tacs.ML")
 begin
 
+
 text {*
   Basic definition for equivalence relations
   that are represented by predicates.
 *}
 
 definition
-  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
+  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
 
 definition
-  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+  "reflp E \<equiv> \<forall>x. E x x"
 
 definition
-  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
 
 definition
-  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
 
 lemma equivp_reflp_symp_transp:
   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
@@ -51,19 +52,15 @@
   shows "equivp R"
   using assms by (simp add: equivp_reflp_symp_transp)
 
-lemma eq_imp_rel:
-  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-  by (simp add: equivp_reflp)
-
 lemma identity_equivp:
   shows "equivp (op =)"
   unfolding equivp_def
   by auto
 
+text {* Partial equivalences: not yet used anywhere *}
 
-text {* Partial equivalences: not yet used anywhere *}
 definition
-  "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
+  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
 lemma equivp_implies_part_equivp:
   assumes a: "equivp E"
@@ -88,7 +85,7 @@
 definition
   Respects
 where
-  "Respects R x \<longleftrightarrow> (R x x)"
+  "Respects R x \<equiv> R x x"
 
 lemma in_respects:
   shows "(x \<in> Respects R) = R x x"
@@ -130,7 +127,7 @@
 section {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<longleftrightarrow>
+  "Quotient E Abs Rep \<equiv>
      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
@@ -354,6 +351,7 @@
   apply(simp add: reflp_def)
   done
 
+(* Next four lemmas are unused *)
 lemma all_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "All P"
@@ -378,6 +376,7 @@
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
+
 lemma ball_all_comm:
   assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
   shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
diff -r 10a6ba364ce1 -r 36d596cb63a2 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Feb 12 12:06:09 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Feb 12 15:06:20 2010 +0100
@@ -153,6 +153,7 @@
 
   finally jump back to 1
 *)
+
 fun regularize_tac ctxt =
 let
   val thy = ProofContext.theory_of ctxt
@@ -163,7 +164,8 @@
                        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)
+  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
+  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
 in
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST'