# HG changeset patch
# User haftmann
# Date 1289307733 -3600
# Node ID c6587375088ecfb89d51f8b3e09b413fa2c9b474
# Parent  2989f9f3aa10209de09a30d2b8b4cfbe68c83a7c
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions

diff -r 2989f9f3aa10 -r c6587375088e src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Nov 09 14:02:13 2010 +0100
+++ b/src/HOL/Quotient.thy	Tue Nov 09 14:02:13 2010 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Plain Hilbert_Choice
+imports Plain Hilbert_Choice Equiv_Relations
 uses
   ("Tools/Quotient/quotient_info.ML")
   ("Tools/Quotient/quotient_typ.ML")
@@ -21,33 +21,49 @@
 *}
 
 definition
-  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+
+lemma refl_reflp:
+  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: refl_on_def reflp_def)
 
 definition
-  "reflp E \<equiv> \<forall>x. E x x"
+  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+
+lemma sym_symp:
+  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: sym_def symp_def)
 
 definition
-  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+
+lemma trans_transp:
+  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
+  by (auto simp add: trans_def transp_def)
 
 definition
-  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
 
 lemma equivp_reflp_symp_transp:
   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
   unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
   by blast
 
+lemma equiv_equivp:
+  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
+  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
+
 lemma equivp_reflp:
   shows "equivp E \<Longrightarrow> E x x"
   by (simp only: equivp_reflp_symp_transp reflp_def)
 
 lemma equivp_symp:
   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
-  by (metis equivp_reflp_symp_transp symp_def)
+  by (simp add: equivp_def)
 
 lemma equivp_transp:
   shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
-  by (metis equivp_reflp_symp_transp transp_def)
+  by (simp add: equivp_def)
 
 lemma equivpI:
   assumes "reflp R" "symp R" "transp R"
@@ -62,7 +78,7 @@
 text {* Partial equivalences *}
 
 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"
@@ -114,6 +130,11 @@
   then show "part_equivp E" unfolding part_equivp_def using a by metis
 qed
 
+lemma part_equivpI:
+  assumes "\<exists>x. R x x" "symp R" "transp R"
+  shows "part_equivp R"
+  using assms by (simp add: part_equivp_refl_symp_transp)
+
 text {* Composition of Relations *}
 
 abbreviation
@@ -128,45 +149,54 @@
 subsection {* Respects predicate *}
 
 definition
-  Respects
+  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
 where
-  "Respects R x \<equiv> R x x"
+  "Respects R x = R x x"
 
 lemma in_respects:
-  shows "(x \<in> Respects R) = R x x"
+  shows "x \<in> Respects R \<longleftrightarrow> R x x"
   unfolding mem_def Respects_def
   by simp
 
 subsection {* Function map and function relation *}
 
 definition
-  fun_map (infixr "--->" 55)
+  fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
 where
-[simp]: "fun_map f g h x = g (h (f x))"
+  "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
+
+lemma fun_map_apply [simp]:
+  "(f ---> g) h x = g (h (f x))"
+  by (simp add: fun_map_def)
+
+lemma fun_map_id:
+  "(id ---> id) = id"
+  by (simp add: fun_eq_iff id_def)
 
 definition
-  fun_rel (infixr "===>" 55)
+  fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
 where
-[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 lemma fun_relI [intro]:
-  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
-  shows "(P ===> Q) x y"
+  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
+  shows "(E1 ===> E2) f g"
   using assms by (simp add: fun_rel_def)
 
-lemma fun_map_id:
-  shows "(id ---> id) = id"
-  by (simp add: fun_eq_iff id_def)
+lemma fun_relE:
+  assumes "(E1 ===> E2) f g" and "E1 x y"
+  obtains "E2 (f x) (g y)"
+  using assms by (simp add: fun_rel_def)
 
 lemma fun_rel_eq:
   shows "((op =) ===> (op =)) = (op =)"
-  by (simp add: fun_eq_iff)
+  by (auto simp add: fun_eq_iff elim: fun_relE)
 
 
 subsection {* 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)))"
 
@@ -232,21 +262,17 @@
   and     q2: "Quotient R2 abs2 rep2"
   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
 proof -
-  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
-    using q1 q2
-    unfolding Quotient_def
-    unfolding fun_eq_iff
-    by simp
+  have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+    using q1 q2 by (simp add: Quotient_def fun_eq_iff)
   moreover
-  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
-    using q1 q2
-    unfolding Quotient_def
-    by (simp (no_asm)) (metis)
+  have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+    by (rule fun_relI)
+      (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
+        simp (no_asm) add: Quotient_def, simp)
   moreover
-  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+  have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
-    unfolding fun_eq_iff
-    apply(auto)
+    apply(auto simp add: fun_rel_def fun_eq_iff)
     using q1 q2 unfolding Quotient_def
     apply(metis)
     using q1 q2 unfolding Quotient_def
@@ -281,7 +307,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by simp
+  by (simp add:)
 
 lemma lambda_prs1:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -289,7 +315,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by simp
+  by (simp add:)
 
 lemma rep_abs_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -317,12 +343,12 @@
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by simp
+  using a by (auto elim: fun_relE)
 
 lemma apply_rsp':
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-  using a by simp
+  using a by (auto elim: fun_relE)
 
 subsection {* lemmas for regularisation of ball and bex *}
 
@@ -370,7 +396,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: in_respects)
+  apply(simp add: in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -384,7 +410,7 @@
   apply(auto)
   apply(rule_tac x="\<lambda>y. f x" in bexI)
   apply(simp)
-  apply(simp add: Respects_def in_respects)
+  apply(simp add: Respects_def in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -429,7 +455,7 @@
 subsection {* Bounded abstraction *}
 
 definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "x \<in> p \<Longrightarrow> Babs p m x = m x"
 
@@ -437,10 +463,10 @@
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
-  apply (auto simp add: Babs_def in_respects)
+  apply (auto simp add: Babs_def in_respects fun_rel_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
-  using a apply (simp add: Babs_def)
-  apply (simp add: in_respects)
+  using a apply (simp add: Babs_def fun_rel_def)
+  apply (simp add: in_respects fun_rel_def)
   using Quotient_rel[OF q]
   by metis
 
@@ -449,7 +475,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   apply (rule ext)
-  apply (simp)
+  apply (simp add:)
   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])
@@ -460,7 +486,7 @@
   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   apply(rule iffI)
   apply(simp_all only: babs_rsp[OF q])
-  apply(auto simp add: Babs_def)
+  apply(auto simp add: Babs_def fun_rel_def)
   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   apply(metis Babs_def)
   apply (simp add: in_respects)
@@ -478,30 +504,29 @@
 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)
+  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
 
 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)
+  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
 
 lemma bex1_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
-  using a
-  by (simp add: Ex1_def in_respects) auto
+  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
 
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
   shows "Ball (Respects R) ((absf ---> id) f) = All f"
-  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
   by metis
 
 lemma ex_prs:
   assumes a: "Quotient R absf repf"
   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
-  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
   by metis
 
 subsection {* @{text Bex1_rel} quantifier *}
@@ -552,7 +577,7 @@
 lemma bex1_rel_rsp:
   assumes a: "Quotient R absf repf"
   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply rule
   apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
@@ -564,7 +589,7 @@
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
   shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
-apply simp
+apply (simp add:)
 apply (subst Bex1_rel_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)
@@ -643,12 +668,12 @@
   shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
-  unfolding o_def fun_eq_iff by simp_all
+  by (simp_all add: fun_eq_iff)
 
 lemma o_rsp:
   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
-  unfolding fun_rel_def o_def fun_eq_iff by auto
+  by (auto intro!: fun_relI elim: fun_relE)
 
 lemma cond_prs:
   assumes a: "Quotient R absf repf"
@@ -664,7 +689,7 @@
 lemma if_rsp:
   assumes q: "Quotient R Abs Rep"
   shows "(op = ===> R ===> R ===> R) If If"
-  by auto
+  by (auto intro!: fun_relI)
 
 lemma let_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -675,11 +700,11 @@
 
 lemma let_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
-  by auto
+  by (auto intro!: fun_relI elim: fun_relE)
 
 lemma mem_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
-  by (simp add: mem_def)
+  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
 
 lemma mem_prs:
   assumes a1: "Quotient R1 Abs1 Rep1"
@@ -689,13 +714,12 @@
 
 lemma id_rsp:
   shows "(R ===> R) id id"
-  by simp
+  by (auto intro: fun_relI)
 
 lemma id_prs:
   assumes a: "Quotient R Abs Rep"
   shows "(Rep ---> Abs) id = id"
-  unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF a])
+  by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
 
 
 locale quot_type =
@@ -710,12 +734,12 @@
 begin
 
 definition
-  abs::"'a \<Rightarrow> 'b"
+  abs :: "'a \<Rightarrow> 'b"
 where
-  "abs x \<equiv> Abs (R x)"
+  "abs x = Abs (R x)"
 
 definition
-  rep::"'b \<Rightarrow> 'a"
+  rep :: "'b \<Rightarrow> 'a"
 where
   "rep a = Eps (Rep a)"
 
@@ -799,7 +823,9 @@
   about the lifted theorem in a tactic.
 *}
 definition
-  "Quot_True (x :: 'a) \<equiv> True"
+  Quot_True :: "'a \<Rightarrow> bool"
+where
+  "Quot_True x \<longleftrightarrow> True"
 
 lemma
   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
@@ -858,4 +884,3 @@
   fun_rel (infixr "===>" 55)
 
 end
-