# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265817749 -3600
# Node ID d1eaed018e5d64285a6a53cb6337de0c531adf80
# Parent  8d3f92694e8540bcbceaa973fe00a3f683b34723
Changes from Makarius's code review + some noticed fixes.

diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotBase.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory QuotBase
-imports Plain ATP_Linkup Predicate
+imports Plain ATP_Linkup
 begin
 
 text {*
@@ -11,17 +11,18 @@
   that are represented by predicates.
 *}
 
+(* TODO check where definitions can be changed to \<longleftrightarrow> *)
 definition
-  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
 
 definition
-  "reflp E \<equiv> \<forall>x. E x x"
+  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
 
 definition
-  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
 
 definition
-  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+  "transp E \<longleftrightarrow> (\<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)"
@@ -29,15 +30,15 @@
   by blast
 
 lemma equivp_reflp:
-  shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
+  shows "equivp E \<Longrightarrow> E x x"
   by (simp only: equivp_reflp_symp_transp reflp_def)
 
 lemma equivp_symp:
-  shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
+  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
   by (metis equivp_reflp_symp_transp symp_def)
 
 lemma equivp_transp:
-  shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
+  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
   by (metis equivp_reflp_symp_transp transp_def)
 
 lemma equivpI:
@@ -57,7 +58,7 @@
 
 text {* Partial equivalences: not yet used anywhere *}
 definition
-  "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)))"
+  "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))))"
 
 lemma equivp_implies_part_equivp:
   assumes a: "equivp E"
@@ -81,7 +82,7 @@
 definition
   Respects
 where
-  "Respects R x \<equiv> (R x x)"
+  "Respects R x \<longleftrightarrow> (R x x)"
 
 lemma in_respects:
   shows "(x \<in> Respects R) = R x x"
@@ -123,7 +124,7 @@
 section {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<equiv> 
+  "Quotient E Abs Rep \<longleftrightarrow>
      (\<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)))"
 
@@ -378,7 +379,7 @@
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+  "x \<in> p \<Longrightarrow> Babs p m x = m x"
 
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
@@ -456,7 +457,7 @@
 definition
   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 where
-  "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+  "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
 
 lemma bex1_rel_aux:
   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
@@ -613,102 +614,5 @@
   shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
   using apply_rsp[OF q1 a1] a2 by auto
 
-
-(*** REST OF THE FILE IS UNUSED (until now) ***)
-
-text {*
-lemma in_fun:
-  shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
-  by (simp add: mem_def)
-
-lemma respects_thm:
-  shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
-  unfolding Respects_def
-  by (simp add: expand_fun_eq)
-
-lemma respects_rep_abs:
-  assumes a: "Quotient R1 Abs1 Rep1"
-  and     b: "Respects (R1 ===> R2) f"
-  and     c: "R1 x x"
-  shows "R2 (f (Rep1 (Abs1 x))) (f x)"
-  using a b[simplified respects_thm] c unfolding Quotient_def
-  by blast
-
-lemma respects_mp:
-  assumes a: "Respects (R1 ===> R2) f"
-  and     b: "R1 x y"
-  shows "R2 (f x) (f y)"
-  using a b unfolding Respects_def
-  by simp
-
-lemma respects_o:
-  assumes a: "Respects (R2 ===> R3) f"
-  and     b: "Respects (R1 ===> R2) g"
-  shows "Respects (R1 ===> R3) (f o g)"
-  using a b unfolding Respects_def
-  by simp
-
-lemma fun_rel_eq_rel:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
-                             \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
-  using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
-  by blast
-
-lemma let_babs:
-  "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
-  by (simp add: Babs_def)
-
-lemma fun_rel_equals:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     r1: "Respects (R1 ===> R2) f"
-  and     r2: "Respects (R1 ===> R2) g"
-  shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-  apply(rule_tac iffI)
-  apply(rule)+
-  apply (rule apply_rsp'[of "R1" "R2"])
-  apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
-  apply auto
-  using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-  apply (metis let_rsp q1)
-  apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
-  using r1 unfolding Respects_def expand_fun_eq
-  apply(simp (no_asm_use))
-  apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
-  done
-
-(* ask Peter: fun_rel_IMP used twice *) 
-lemma fun_rel_IMP2:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     r1: "Respects (R1 ===> R2) f"
-  and     r2: "Respects (R1 ===> R2) g" 
-  and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
-  shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  using q1 q2 r1 r2 a
-  by (simp add: fun_rel_equals)
-
-lemma lambda_rep_abs_rsp:
-  assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
-  and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
-  shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
-  using r1 r2 by auto
-
-(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
-lemma id_prs:
-  assumes q: "Quotient R Abs Rep"
-  shows "Abs (id (Rep e)) = id e"
-  using Quotient_abs_rep[OF q] by auto
-
-lemma id_rsp:
-  assumes q: "Quotient R Abs Rep"
-  and     a: "R e1 e2"
-  shows "R (id e1) (id e2)"
-  using a by auto
-
-*}
-
 end
 
diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotMain.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -4,11 +4,12 @@
 
 theory QuotMain
 imports QuotBase
-uses ("quotient_info.ML")
-     ("quotient_typ.ML")
-     ("quotient_def.ML")
-     ("quotient_term.ML")
-     ("quotient_tacs.ML")
+uses
+  ("quotient_info.ML")
+  ("quotient_typ.ML")
+  ("quotient_def.ML")
+  ("quotient_term.ML")
+  ("quotient_tacs.ML")
 begin
 
 locale Quot_Type =
@@ -32,12 +33,7 @@
 where
   "rep a = Eps (Rep a)"
 
-text {*
-  The naming of the lemmas follows the quotient paper
-  by Peter Homeier.
-*}
-
-lemma lem9:
+lemma homeier_lem9:
   shows "R (Eps (R x)) = R x"
 proof -
   have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
@@ -46,21 +42,21 @@
     using equivp unfolding equivp_def by simp
 qed
 
-theorem thm10:
+theorem homeier_thm10:
   shows "abs (rep a) = a"
   unfolding abs_def rep_def
 proof -
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
-  also have "\<dots> = Abs (R x)" using lem9 by simp
+  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
   also have "\<dots> = Abs (Rep a)" using eq by simp
   also have "\<dots> = a" using rep_inverse by simp
   finally
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma lem7:
+lemma homeier_lem7:
   shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
 proof -
   have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
@@ -68,10 +64,10 @@
   finally show "?LHS = ?RHS" by simp
 qed
 
-theorem thm11:
+theorem homeier_thm11:
   shows "R r r' = (abs r = abs r')"
   unfolding abs_def
-  by (simp only: equivp[simplified equivp_def] lem7)
+  by (simp only: equivp[simplified equivp_def] homeier_lem7)
 
 lemma rep_refl:
   shows "R (rep a) (rep a)"
@@ -82,14 +78,14 @@
 lemma rep_abs_rsp:
   shows "R f (rep (abs g)) = R f g"
   and   "R (rep (abs g)) f = R g f"
-  by (simp_all add: thm10 thm11)
+  by (simp_all add: homeier_thm10 homeier_thm11)
 
 lemma Quotient:
   shows "Quotient R abs rep"
   unfolding Quotient_def
-  apply(simp add: thm10)
+  apply(simp add: homeier_thm10)
   apply(simp add: rep_refl)
-  apply(subst thm11[symmetric])
+  apply(subst homeier_thm11[symmetric])
   apply(simp add: equivp[simplified equivp_def])
   done
 
@@ -129,9 +125,9 @@
 use "quotient_def.ML"
 
 
-text {* 
-  An auxiliar constant for recording some information  
-  about the lifted theorem in a tactic.       
+text {*
+  An auxiliary constant for recording some information
+  about the lifted theorem in a tactic.
 *}
 definition
   "Quot_True x \<equiv> True"
@@ -147,11 +143,13 @@
 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   by (simp add: Quot_True_def)
 
+
 text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"
 
 section {* Methods / Interface *}
 
+(* TODO inline *)
 ML {*
 fun mk_method1 tac thms ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) 
@@ -162,27 +160,27 @@
 
 method_setup lifting =
   {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
-  {* Lifting of theorems to quotient types. *}
+  {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
-  {* Sets up the three goals for the lifting procedure. *}
+  {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup regularize =
   {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
-  {* Proves automatically the regularization goals from the lifting procedure. *}
+  {* proves the regularization goals from the quotient lifting procedure *}
 
 method_setup injection =
   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
-  {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+  {* proves the rep/abs injection goals from the quotient lifting procedure *}
 
 method_setup cleaning =
   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
-  {* Proves automatically the cleaning goals from the lifting procedure. *}
+  {* proves the cleaning goals from the quotient lifting procedure *}
 
 attribute_setup quot_lifted =
   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
-  {* Lifting of theorems to quotient types. *}
+  {* lifts theorems to quotient types *}
 
 end
 
diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotOption.thy
--- a/Quot/QuotOption.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotOption.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -62,7 +62,7 @@
   shows "Option.map Abs None = None"
   by simp
 
-lemma option_Some_prs[quot_respect]:
+lemma option_Some_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> Option.map Abs) Some = Some"
   apply(simp add: expand_fun_eq)
diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotSum.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -69,7 +69,7 @@
   shows "(R2 ===> sum_rel R1 R2) Inr Inr"
   by simp
 
-lemma sum_Inl_prs[quot_respect]:
+lemma sum_Inl_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
@@ -77,7 +77,7 @@
   apply(simp add: Quotient_abs_rep[OF q1])
   done
 
-lemma sum_Inr_prs[quot_respect]:
+lemma sum_Inr_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"