--- a/NEWS Tue Nov 30 00:12:29 2010 +0100
+++ b/NEWS Tue Nov 30 15:58:21 2010 +0100
@@ -92,6 +92,9 @@
*** HOL ***
+* Abandoned locale equiv for equivalence relations. INCOMPATIBILITY: use
+equivI rather than equiv_intro.
+
* Code generator: globbing constant expressions "*" and "Theory.*" have been
replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.
--- a/src/HOL/Algebra/Coset.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy Tue Nov 30 15:58:21 2010 +0100
@@ -606,7 +606,7 @@
proof -
interpret group G by fact
show ?thesis
- proof (intro equiv.intro)
+ proof (intro equivI)
show "refl_on (carrier G) (rcong H)"
by (auto simp add: r_congruent_def refl_on_def)
next
--- a/src/HOL/Equiv_Relations.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy Tue Nov 30 15:58:21 2010 +0100
@@ -8,13 +8,19 @@
imports Big_Operators Relation Plain
begin
-subsection {* Equivalence relations *}
+subsection {* Equivalence relations -- set version *}
+
+definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
+ "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
-locale equiv =
- fixes A and r
- assumes refl_on: "refl_on A r"
- and sym: "sym r"
- and trans: "trans r"
+lemma equivI:
+ "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+ by (simp add: equiv_def)
+
+lemma equivE:
+ assumes "equiv A r"
+ obtains "refl_on A r" and "sym r" and "trans r"
+ using assms by (simp add: equiv_def)
text {*
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
@@ -157,9 +163,17 @@
subsection {* Defining unary operations upon equivalence classes *}
text{*A congruence-preserving function*}
-locale congruent =
- fixes r and f
- assumes congruent: "(y,z) \<in> r ==> f y = f z"
+
+definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
+ "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
+
+lemma congruentI:
+ "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
+ by (auto simp add: congruent_def)
+
+lemma congruentD:
+ "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
+ by (auto simp add: congruent_def)
abbreviation
RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
@@ -214,10 +228,18 @@
subsection {* Defining binary operations upon equivalence classes *}
text{*A congruence-preserving function of two arguments*}
-locale congruent2 =
- fixes r1 and r2 and f
- assumes congruent2:
- "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
+
+definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
+ "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
+
+lemma congruent2I':
+ assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
+ shows "congruent2 r1 r2 f"
+ using assms by (auto simp add: congruent2_def)
+
+lemma congruent2D:
+ "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
+ using assms by (auto simp add: congruent2_def)
text{*Abbreviation for the common case where the relations are identical*}
abbreviation
@@ -331,4 +353,99 @@
apply simp
done
+
+subsection {* Equivalence relations -- predicate version *}
+
+text {* Partial equivalences *}
+
+definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)"
+ -- {* John-Harrison-style characterization *}
+
+lemma part_equivpI:
+ "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
+ by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE)
+
+lemma part_equivpE:
+ assumes "part_equivp R"
+ obtains x where "R x x" and "symp R" and "transp R"
+proof -
+ from assms have 1: "\<exists>x. R x x"
+ and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y"
+ by (unfold part_equivp_def) blast+
+ from 1 obtain x where "R x x" ..
+ moreover have "symp R"
+ proof (rule sympI)
+ fix x y
+ assume "R x y"
+ with 2 [of x y] show "R y x" by auto
+ qed
+ moreover have "transp R"
+ proof (rule transpI)
+ fix x y z
+ assume "R x y" and "R y z"
+ with 2 [of x y] 2 [of y z] show "R x z" by auto
+ qed
+ ultimately show thesis by (rule that)
+qed
+
+lemma part_equivp_refl_symp_transp:
+ "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R"
+ by (auto intro: part_equivpI elim: part_equivpE)
+
+lemma part_equivp_symp:
+ "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+ by (erule part_equivpE, erule sympE)
+
+lemma part_equivp_transp:
+ "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+ by (erule part_equivpE, erule transpE)
+
+lemma part_equivp_typedef:
+ "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
+ by (auto elim: part_equivpE simp add: mem_def)
+
+
+text {* Total equivalences *}
+
+definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *}
+
+lemma equivpI:
+ "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
+ by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
+
+lemma equivpE:
+ assumes "equivp R"
+ obtains "reflp R" and "symp R" and "transp R"
+ using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)
+
+lemma equivp_implies_part_equivp:
+ "equivp R \<Longrightarrow> part_equivp R"
+ by (auto intro: part_equivpI elim: equivpE reflpE)
+
+lemma equivp_equiv:
+ "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
+ by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def)
+
+lemma equivp_reflp_symp_transp:
+ shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
+ by (auto intro: equivpI elim: equivpE)
+
+lemma identity_equivp:
+ "equivp (op =)"
+ by (auto intro: equivpI reflpI sympI transpI)
+
+lemma equivp_reflp:
+ "equivp R \<Longrightarrow> R x x"
+ by (erule equivpE, erule reflpE)
+
+lemma equivp_symp:
+ "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+ by (erule equivpE, erule sympE)
+
+lemma equivp_transp:
+ "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+ by (erule equivpE, erule transpE)
+
end
--- a/src/HOL/Int.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Int.thy Tue Nov 30 15:58:21 2010 +0100
@@ -102,7 +102,7 @@
lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
proof -
have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
- by (simp add: congruent_def)
+ by (auto simp add: congruent_def)
thus ?thesis
by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
qed
@@ -113,7 +113,7 @@
proof -
have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
respects2 intrel"
- by (simp add: congruent2_def)
+ by (auto simp add: congruent2_def)
thus ?thesis
by (simp add: add_int_def UN_UN_split_split_eq
UN_equiv_class2 [OF equiv_intrel equiv_intrel])
@@ -288,7 +288,7 @@
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
- by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
+ by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
del: of_nat_add)
thus ?thesis
by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
@@ -394,7 +394,7 @@
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
have "(\<lambda>(x,y). {x-y}) respects intrel"
- by (simp add: congruent_def) arith
+ by (auto simp add: congruent_def)
thus ?thesis
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
qed
--- a/src/HOL/Library/Fraction_Field.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Tue Nov 30 15:58:21 2010 +0100
@@ -43,7 +43,7 @@
qed
lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
- by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
+ by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
--- a/src/HOL/Library/Quotient_List.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Library/Quotient_List.thy Tue Nov 30 15:58:21 2010 +0100
@@ -10,94 +10,96 @@
declare [[map list = (map, list_all2)]]
-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
+lemma map_id [id_simps]:
+ "map id = id"
+ by (simp add: id_def fun_eq_iff map.identity)
-lemma map_id[id_simps]:
- shows "map id = id"
- apply(simp add: fun_eq_iff)
- apply(rule allI)
- apply(induct_tac x)
- apply(simp_all)
- done
+lemma list_all2_map1:
+ "list_all2 R (map f xs) ys \<longleftrightarrow> list_all2 (\<lambda>x. R (f x)) xs ys"
+ by (induct xs ys rule: list_induct2') simp_all
+
+lemma list_all2_map2:
+ "list_all2 R xs (map f ys) \<longleftrightarrow> list_all2 (\<lambda>x y. R x (f y)) xs ys"
+ by (induct xs ys rule: list_induct2') simp_all
-lemma list_all2_reflp:
- shows "equivp R \<Longrightarrow> list_all2 R xs xs"
- by (induct xs, simp_all add: equivp_reflp)
+lemma list_all2_eq [id_simps]:
+ "list_all2 (op =) = (op =)"
+proof (rule ext)+
+ fix xs ys
+ show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys"
+ by (induct xs ys rule: list_induct2') simp_all
+qed
-lemma list_all2_symp:
- assumes a: "equivp R"
- and b: "list_all2 R xs ys"
- shows "list_all2 R ys xs"
- using list_all2_lengthD[OF b] b
- apply(induct xs ys rule: list_induct2)
- apply(simp_all)
- apply(rule equivp_symp[OF a])
- apply(simp)
- done
+lemma list_reflp:
+ assumes "reflp R"
+ shows "reflp (list_all2 R)"
+proof (rule reflpI)
+ from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
+ fix xs
+ show "list_all2 R xs xs"
+ by (induct xs) (simp_all add: *)
+qed
-lemma list_all2_transp:
- assumes a: "equivp R"
- and b: "list_all2 R xs1 xs2"
- and c: "list_all2 R xs2 xs3"
- shows "list_all2 R xs1 xs3"
- using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
- apply(induct rule: list_induct3)
- apply(simp_all)
- apply(auto intro: equivp_transp[OF a])
- done
+lemma list_symp:
+ assumes "symp R"
+ shows "symp (list_all2 R)"
+proof (rule sympI)
+ from assms have *: "\<And>xs ys. R xs ys \<Longrightarrow> R ys xs" by (rule sympE)
+ fix xs ys
+ assume "list_all2 R xs ys"
+ then show "list_all2 R ys xs"
+ by (induct xs ys rule: list_induct2') (simp_all add: *)
+qed
-lemma list_equivp[quot_equiv]:
- assumes a: "equivp R"
- shows "equivp (list_all2 R)"
- apply (intro equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp add: list_all2_reflp[OF a])
- apply(blast intro: list_all2_symp[OF a])
- apply(blast intro: list_all2_transp[OF a])
- done
+lemma list_transp:
+ assumes "transp R"
+ shows "transp (list_all2 R)"
+proof (rule transpI)
+ from assms have *: "\<And>xs ys zs. R xs ys \<Longrightarrow> R ys zs \<Longrightarrow> R xs zs" by (rule transpE)
+ fix xs ys zs
+ assume A: "list_all2 R xs ys" "list_all2 R ys zs"
+ then have "length xs = length ys" "length ys = length zs" by (blast dest: list_all2_lengthD)+
+ then show "list_all2 R xs zs" using A
+ by (induct xs ys zs rule: list_induct3) (auto intro: *)
+qed
-lemma list_all2_rel:
- assumes q: "Quotient R Abs Rep"
- shows "list_all2 R r s = (list_all2 R r r \<and> list_all2 R s s \<and> (map Abs r = map Abs s))"
- apply(induct r s rule: list_induct2')
- apply(simp_all)
- using Quotient_rel[OF q]
- apply(metis)
- done
+lemma list_equivp [quot_equiv]:
+ "equivp R \<Longrightarrow> equivp (list_all2 R)"
+ by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
-lemma list_quotient[quot_thm]:
- assumes q: "Quotient R Abs Rep"
+lemma list_quotient [quot_thm]:
+ assumes "Quotient R Abs Rep"
shows "Quotient (list_all2 R) (map Abs) (map Rep)"
- unfolding Quotient_def
- apply(subst split_list_all)
- apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
- apply(intro conjI allI)
- apply(induct_tac a)
- apply(simp_all add: Quotient_rep_reflp[OF q])
- apply(rule list_all2_rel[OF q])
- done
+proof (rule QuotientI)
+ from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+ then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
+next
+ from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
+ then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
+ by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
+next
+ fix xs ys
+ from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel)
+ then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> map Abs xs = map Abs ys"
+ by (induct xs ys rule: list_induct2') auto
+qed
-lemma cons_prs[quot_preserve]:
+lemma cons_prs [quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp [quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
by auto
-lemma nil_prs[quot_preserve]:
+lemma nil_prs [quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "map Abs [] = []"
by simp
-lemma nil_rsp[quot_respect]:
+lemma nil_rsp [quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "list_all2 R [] []"
by simp
@@ -109,7 +111,7 @@
by (induct l)
(simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
-lemma map_prs[quot_preserve]:
+lemma map_prs [quot_preserve]:
assumes a: "Quotient R1 abs1 rep1"
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
@@ -117,8 +119,7 @@
by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
(simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
-
-lemma map_rsp[quot_respect]:
+lemma map_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
@@ -137,7 +138,7 @@
shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
-lemma foldr_prs[quot_preserve]:
+lemma foldr_prs [quot_preserve]:
assumes a: "Quotient R1 abs1 rep1"
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
@@ -151,8 +152,7 @@
shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
-
-lemma foldl_prs[quot_preserve]:
+lemma foldl_prs [quot_preserve]:
assumes a: "Quotient R1 abs1 rep1"
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
@@ -217,11 +217,11 @@
qed
qed
-lemma[quot_respect]:
+lemma [quot_respect]:
"((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
by (simp add: list_all2_rsp fun_rel_def)
-lemma[quot_preserve]:
+lemma [quot_preserve]:
assumes a: "Quotient R abs1 rep1"
shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
apply (simp add: fun_eq_iff)
@@ -230,19 +230,11 @@
apply (simp_all add: Quotient_abs_rep[OF a])
done
-lemma[quot_preserve]:
+lemma [quot_preserve]:
assumes a: "Quotient R abs1 rep1"
shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
-lemma list_all2_eq[id_simps]:
- shows "(list_all2 (op =)) = (op =)"
- unfolding fun_eq_iff
- apply(rule allI)+
- apply(induct_tac x xa rule: list_induct2')
- apply(simp_all)
- done
-
lemma list_all2_find_element:
assumes a: "x \<in> set a"
and b: "list_all2 R a b"
--- a/src/HOL/Library/Quotient_Option.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Tue Nov 30 15:58:21 2010 +0100
@@ -18,64 +18,73 @@
declare [[map option = (Option.map, option_rel)]]
-text {* should probably be in Option.thy *}
-lemma split_option_all:
- shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
- apply(auto)
- apply(case_tac x)
- apply(simp_all)
+lemma option_rel_unfold:
+ "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
+ | (Some x, Some y) \<Rightarrow> R x y
+ | _ \<Rightarrow> False)"
+ by (cases x) (cases y, simp_all)+
+
+lemma option_rel_map1:
+ "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
+ by (simp add: option_rel_unfold split: option.split)
+
+lemma option_rel_map2:
+ "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
+ by (simp add: option_rel_unfold split: option.split)
+
+lemma option_map_id [id_simps]:
+ "Option.map id = id"
+ by (simp add: id_def Option.map.identity fun_eq_iff)
+
+lemma option_rel_eq [id_simps]:
+ "option_rel (op =) = (op =)"
+ by (simp add: option_rel_unfold fun_eq_iff split: option.split)
+
+lemma option_reflp:
+ "reflp R \<Longrightarrow> reflp (option_rel R)"
+ by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
+
+lemma option_symp:
+ "symp R \<Longrightarrow> symp (option_rel R)"
+ by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
+
+lemma option_transp:
+ "transp R \<Longrightarrow> transp (option_rel R)"
+ by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
+
+lemma option_equivp [quot_equiv]:
+ "equivp R \<Longrightarrow> equivp (option_rel R)"
+ by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
+
+lemma option_quotient [quot_thm]:
+ assumes "Quotient R Abs Rep"
+ shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
+ apply (rule QuotientI)
+ apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
+ using Quotient_rel [OF assms]
+ apply (simp add: option_rel_unfold split: option.split)
done
-lemma option_quotient[quot_thm]:
- assumes q: "Quotient R Abs Rep"
- shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
- unfolding Quotient_def
- apply(simp add: split_option_all)
- apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
- using q
- unfolding Quotient_def
- apply(blast)
- done
-
-lemma option_equivp[quot_equiv]:
- assumes a: "equivp R"
- shows "equivp (option_rel R)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_option_all)
- apply(blast intro: equivp_reflp[OF a])
- apply(blast intro: equivp_symp[OF a])
- apply(blast intro: equivp_transp[OF a])
- done
-
-lemma option_None_rsp[quot_respect]:
+lemma option_None_rsp [quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "option_rel R None None"
by simp
-lemma option_Some_rsp[quot_respect]:
+lemma option_Some_rsp [quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "(R ===> option_rel R) Some Some"
by auto
-lemma option_None_prs[quot_preserve]:
+lemma option_None_prs [quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "Option.map Abs None = None"
by simp
-lemma option_Some_prs[quot_preserve]:
+lemma option_Some_prs [quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> Option.map Abs) Some = Some"
apply(simp add: fun_eq_iff)
apply(simp add: Quotient_abs_rep[OF q])
done
-lemma option_map_id[id_simps]:
- shows "Option.map id = id"
- by (simp add: fun_eq_iff split_option_all)
-
-lemma option_rel_eq[id_simps]:
- shows "option_rel (op =) = (op =)"
- by (simp add: fun_eq_iff split_option_all)
-
end
--- a/src/HOL/Library/Quotient_Product.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Tue Nov 30 15:58:21 2010 +0100
@@ -19,38 +19,39 @@
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
by (simp add: prod_rel_def)
-lemma prod_equivp[quot_equiv]:
- assumes a: "equivp R1"
- assumes b: "equivp R2"
+lemma map_pair_id [id_simps]:
+ shows "map_pair id id = id"
+ by (simp add: fun_eq_iff)
+
+lemma prod_rel_eq [id_simps]:
+ shows "prod_rel (op =) (op =) = (op =)"
+ by (simp add: fun_eq_iff)
+
+lemma prod_equivp [quot_equiv]:
+ assumes "equivp R1"
+ assumes "equivp R2"
shows "equivp (prod_rel R1 R2)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_paired_all prod_rel_def)
- apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
- apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
- apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
+ using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
+
+lemma prod_quotient [quot_thm]:
+ assumes "Quotient R1 Abs1 Rep1"
+ assumes "Quotient R2 Abs2 Rep2"
+ shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
+ apply (rule QuotientI)
+ apply (simp add: map_pair.compositionality map_pair.identity
+ Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
+ apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
+ using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
+ apply (auto simp add: split_paired_all)
done
-lemma prod_quotient[quot_thm]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
- unfolding Quotient_def
- apply(simp add: split_paired_all)
- apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
- apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
- using q1 q2
- unfolding Quotient_def
- apply(blast)
- done
-
-lemma Pair_rsp[quot_respect]:
+lemma Pair_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
by (auto simp add: prod_rel_def)
-lemma Pair_prs[quot_preserve]:
+lemma Pair_prs [quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
@@ -58,35 +59,35 @@
apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
done
-lemma fst_rsp[quot_respect]:
+lemma fst_rsp [quot_respect]:
assumes "Quotient R1 Abs1 Rep1"
assumes "Quotient R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R1) fst fst"
by auto
-lemma fst_prs[quot_preserve]:
+lemma fst_prs [quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
-lemma snd_rsp[quot_respect]:
+lemma snd_rsp [quot_respect]:
assumes "Quotient R1 Abs1 Rep1"
assumes "Quotient R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R2) snd snd"
by auto
-lemma snd_prs[quot_preserve]:
+lemma snd_prs [quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
-lemma split_rsp[quot_respect]:
+lemma split_rsp [quot_respect]:
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
by (auto intro!: fun_relI elim!: fun_relE)
-lemma split_prs[quot_preserve]:
+lemma split_prs [quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
@@ -111,12 +112,4 @@
declare Pair_eq[quot_preserve]
-lemma map_pair_id[id_simps]:
- shows "map_pair id id = id"
- by (simp add: fun_eq_iff)
-
-lemma prod_rel_eq[id_simps]:
- shows "prod_rel (op =) (op =) = (op =)"
- by (simp add: fun_eq_iff)
-
end
--- a/src/HOL/Library/Quotient_Sum.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Nov 30 15:58:21 2010 +0100
@@ -18,53 +18,68 @@
declare [[map sum = (sum_map, sum_rel)]]
+lemma sum_rel_unfold:
+ "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
+ by (cases x) (cases y, simp_all)+
-text {* should probably be in @{theory Sum_Type} *}
-lemma split_sum_all:
- shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
- apply(auto)
- apply(case_tac x)
- apply(simp_all)
- done
+lemma sum_rel_map1:
+ "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
+ by (simp add: sum_rel_unfold split: sum.split)
+
+lemma sum_rel_map2:
+ "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
+ by (simp add: sum_rel_unfold split: sum.split)
+
+lemma sum_map_id [id_simps]:
+ "sum_map id id = id"
+ by (simp add: id_def sum_map.identity fun_eq_iff)
-lemma sum_equivp[quot_equiv]:
- assumes a: "equivp R1"
- assumes b: "equivp R2"
- shows "equivp (sum_rel R1 R2)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_sum_all)
- apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
- apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
- apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
- done
+lemma sum_rel_eq [id_simps]:
+ "sum_rel (op =) (op =) = (op =)"
+ by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
+
+lemma sum_reflp:
+ "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
+ by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
-lemma sum_quotient[quot_thm]:
+lemma sum_symp:
+ "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
+ by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
+
+lemma sum_transp:
+ "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
+ by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
+
+lemma sum_equivp [quot_equiv]:
+ "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
+ by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
+
+lemma sum_quotient [quot_thm]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
- unfolding Quotient_def
- apply(simp add: split_sum_all)
- apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
- apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
- using q1 q2
- unfolding Quotient_def
- apply(blast)+
+ apply (rule QuotientI)
+ apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
+ Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
+ using Quotient_rel [OF q1] Quotient_rel [OF q2]
+ apply (simp add: sum_rel_unfold split: sum.split)
done
-lemma sum_Inl_rsp[quot_respect]:
+lemma sum_Inl_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R1 ===> sum_rel R1 R2) Inl Inl"
by auto
-lemma sum_Inr_rsp[quot_respect]:
+lemma sum_Inr_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R2 ===> sum_rel R1 R2) Inr Inr"
by auto
-lemma sum_Inl_prs[quot_preserve]:
+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"
@@ -72,7 +87,7 @@
apply(simp add: Quotient_abs_rep[OF q1])
done
-lemma sum_Inr_prs[quot_preserve]:
+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"
@@ -80,12 +95,4 @@
apply(simp add: Quotient_abs_rep[OF q2])
done
-lemma sum_map_id[id_simps]:
- shows "sum_map id id = id"
- by (simp add: fun_eq_iff split_sum_all)
-
-lemma sum_rel_eq[id_simps]:
- shows "sum_rel (op =) (op =) = (op =)"
- by (simp add: fun_eq_iff split_sum_all)
-
end
--- a/src/HOL/NSA/StarDef.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy Tue Nov 30 15:58:21 2010 +0100
@@ -62,7 +62,7 @@
by (simp add: starrel_def)
lemma equiv_starrel: "equiv UNIV starrel"
-proof (rule equiv.intro)
+proof (rule equivI)
show "refl starrel" by (simp add: refl_on_def)
show "sym starrel" by (simp add: sym_def eq_commute)
show "trans starrel" by (auto intro: transI elim!: ultra)
--- a/src/HOL/Predicate.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Predicate.thy Tue Nov 30 15:58:21 2010 +0100
@@ -363,6 +363,44 @@
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
"single_valuedP r == single_valued {(x, y). r x y}"
+(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
+
+definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
+
+definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "symp r \<longleftrightarrow> sym {(x, y). r x y}"
+
+definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transp r \<longleftrightarrow> trans {(x, y). r x y}"
+
+lemma reflpI:
+ "(\<And>x. r x x) \<Longrightarrow> reflp r"
+ by (auto intro: refl_onI simp add: reflp_def)
+
+lemma reflpE:
+ assumes "reflp r"
+ obtains "r x x"
+ using assms by (auto dest: refl_onD simp add: reflp_def)
+
+lemma sympI:
+ "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
+ by (auto intro: symI simp add: symp_def)
+
+lemma sympE:
+ assumes "symp r" and "r x y"
+ obtains "r y x"
+ using assms by (auto dest: symD simp add: symp_def)
+
+lemma transpI:
+ "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
+ by (auto intro: transI simp add: transp_def)
+
+lemma transpE:
+ assumes "transp r" and "r x y" and "r y z"
+ obtains "r x z"
+ using assms by (auto dest: transD simp add: transp_def)
+
subsection {* Predicates as enumerations *}
--- a/src/HOL/Quotient.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Quotient.thy Tue Nov 30 15:58:21 2010 +0100
@@ -14,131 +14,15 @@
("Tools/Quotient/quotient_tacs.ML")
begin
-
text {*
Basic definition for equivalence relations
that are represented by predicates.
*}
-definition
- "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
- "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
- "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
- "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 (simp add: equivp_def)
-
-lemma equivp_transp:
- shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
- by (simp add: equivp_def)
-
-lemma equivpI:
- assumes "reflp R" "symp R" "transp R"
- shows "equivp R"
- using assms by (simp add: equivp_reflp_symp_transp)
-
-lemma identity_equivp:
- shows "equivp (op =)"
- unfolding equivp_def
- by auto
-
-text {* Partial equivalences *}
-
-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)))"
-
-lemma equivp_implies_part_equivp:
- assumes a: "equivp E"
- shows "part_equivp E"
- using a
- unfolding equivp_def part_equivp_def
- by auto
-
-lemma part_equivp_symp:
- assumes e: "part_equivp R"
- and a: "R x y"
- shows "R y x"
- using e[simplified part_equivp_def] a
- by (metis)
-
-lemma part_equivp_typedef:
- shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
- unfolding part_equivp_def mem_def
- apply clarify
- apply (intro exI)
- apply (rule conjI)
- apply assumption
- apply (rule refl)
- done
-
-lemma part_equivp_refl_symp_transp:
- shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
-proof
- assume "part_equivp E"
- then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
- unfolding part_equivp_def symp_def transp_def
- by metis
-next
- assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
- then have b: "(\<forall>x y. E x y \<longrightarrow> E y x)" and c: "(\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
- unfolding symp_def transp_def by (metis, metis)
- have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
- proof (intro allI iffI conjI)
- fix x y
- assume d: "E x y"
- then show "E x x" using b c by metis
- show "E y y" using b c d by metis
- show "E x = E y" unfolding fun_eq_iff using b c d by metis
- next
- fix x y
- assume "E x x \<and> E y y \<and> E x = E y"
- then show "E x y" using b c by metis
- qed
- 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
- rel_conj (infixr "OOO" 75)
+ rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
where
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"
@@ -169,16 +53,16 @@
definition
fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
where
- "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+ "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
lemma fun_relI [intro]:
- assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
- shows "(E1 ===> E2) f g"
+ assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
using assms by (simp add: fun_rel_def)
lemma fun_relE:
- assumes "(E1 ===> E2) f g" and "E1 x y"
- obtains "E2 (f x) (g y)"
+ assumes "(R1 ===> R2) f g" and "R1 x y"
+ obtains "R2 (f x) (g y)"
using assms by (simp add: fun_rel_def)
lemma fun_rel_eq:
@@ -189,34 +73,41 @@
subsection {* Quotient Predicate *}
definition
- "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)))"
+ "Quotient R Abs Rep \<longleftrightarrow>
+ (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
+ (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
+
+lemma QuotientI:
+ assumes "\<And>a. Abs (Rep a) = a"
+ and "\<And>a. R (Rep a) (Rep a)"
+ and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
+ shows "Quotient R Abs Rep"
+ using assms unfolding Quotient_def by blast
lemma Quotient_abs_rep:
- assumes a: "Quotient E Abs Rep"
+ assumes a: "Quotient R Abs Rep"
shows "Abs (Rep a) = a"
using a
unfolding Quotient_def
by simp
lemma Quotient_rep_reflp:
- assumes a: "Quotient E Abs Rep"
- shows "E (Rep a) (Rep a)"
+ assumes a: "Quotient R Abs Rep"
+ shows "R (Rep a) (Rep a)"
using a
unfolding Quotient_def
by blast
lemma Quotient_rel:
- assumes a: "Quotient E Abs Rep"
- shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+ assumes a: "Quotient R Abs Rep"
+ shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
using a
unfolding Quotient_def
by blast
lemma Quotient_rel_rep:
assumes a: "Quotient R Abs Rep"
- shows "R (Rep a) (Rep b) = (a = b)"
+ shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
using a
unfolding Quotient_def
by metis
@@ -228,22 +119,20 @@
by blast
lemma Quotient_rel_abs:
- assumes a: "Quotient E Abs Rep"
- shows "E r s \<Longrightarrow> Abs r = Abs s"
+ assumes a: "Quotient R Abs Rep"
+ shows "R r s \<Longrightarrow> Abs r = Abs s"
using a unfolding Quotient_def
by blast
lemma Quotient_symp:
- assumes a: "Quotient E Abs Rep"
- shows "symp E"
- using a unfolding Quotient_def symp_def
- by metis
+ assumes a: "Quotient R Abs Rep"
+ shows "symp R"
+ using a unfolding Quotient_def using sympI by metis
lemma Quotient_transp:
- assumes a: "Quotient E Abs Rep"
- shows "transp E"
- using a unfolding Quotient_def transp_def
- by metis
+ assumes a: "Quotient R Abs Rep"
+ shows "transp R"
+ using a unfolding Quotient_def using transpI by metis
lemma identity_quotient:
shows "Quotient (op =) id id"
@@ -291,8 +180,7 @@
and a: "R xa xb" "R ya yb"
shows "R xa ya = R xb yb"
using a Quotient_symp[OF q] Quotient_transp[OF q]
- unfolding symp_def transp_def
- by blast
+ by (blast elim: sympE transpE)
lemma lambda_prs:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -300,7 +188,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 add:)
+ by simp
lemma lambda_prs1:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -308,7 +196,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 add:)
+ by simp
lemma rep_abs_rsp:
assumes q: "Quotient R Abs Rep"
@@ -392,9 +280,7 @@
apply(simp add: in_respects fun_rel_def)
apply(rule impI)
using a equivp_reflp_symp_transp[of "R2"]
- apply(simp add: reflp_def)
- apply(simp)
- apply(simp)
+ apply (auto elim: equivpE reflpE)
done
lemma bex_reg_eqv_range:
@@ -406,7 +292,7 @@
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)
+ apply (auto elim: equivpE reflpE)
done
(* Next four lemmas are unused *)
--- a/src/HOL/Rat.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/Rat.thy Tue Nov 30 15:58:21 2010 +0100
@@ -44,7 +44,7 @@
qed
lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
- by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
+ by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
@@ -146,7 +146,7 @@
lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
proof -
have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
- by (simp add: congruent_def)
+ by (simp add: congruent_def split_paired_all)
then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
qed
@@ -781,7 +781,7 @@
lemma of_rat_congruent:
"(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
-apply (rule congruent.intro)
+apply (rule congruentI)
apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
apply (simp only: of_int_mult [symmetric])
done
--- a/src/HOL/RealDef.thy Tue Nov 30 00:12:29 2010 +0100
+++ b/src/HOL/RealDef.thy Tue Nov 30 15:58:21 2010 +0100
@@ -324,7 +324,7 @@
lemma equiv_realrel: "equiv {X. cauchy X} realrel"
using refl_realrel sym_realrel trans_realrel
- by (rule equiv.intro)
+ by (rule equivI)
subsection {* The field of real numbers *}
@@ -358,7 +358,7 @@
apply (simp add: quotientI X)
apply (rule the_equality)
apply clarsimp
- apply (erule congruent.congruent [OF f])
+ apply (erule congruentD [OF f])
apply (erule bspec)
apply simp
apply (rule refl_onD [OF refl_realrel])
@@ -370,14 +370,14 @@
assumes X: "cauchy X" and Y: "cauchy Y"
shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
apply (subst real_case_1 [OF _ X])
- apply (rule congruent.intro)
+ apply (rule congruentI)
apply (subst real_case_1 [OF _ Y])
apply (rule congruent2_implies_congruent [OF equiv_realrel f])
apply (simp add: realrel_def)
apply (subst real_case_1 [OF _ Y])
apply (rule congruent2_implies_congruent [OF equiv_realrel f])
apply (simp add: realrel_def)
- apply (erule congruent2.congruent2 [OF f])
+ apply (erule congruent2D [OF f])
apply (rule refl_onD [OF refl_realrel])
apply (simp add: Y)
apply (rule real_case_1 [OF _ Y])
@@ -416,7 +416,7 @@
lemma minus_respects_realrel:
"(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -492,7 +492,7 @@
lemma inverse_respects_realrel:
"(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
(is "?inv respects realrel")
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -622,7 +622,7 @@
assumes sym: "sym r"
assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
shows "P respects r"
-apply (rule congruent.intro)
+apply (rule congruentI)
apply (rule iffI)
apply (erule (1) P)
apply (erule (1) P [OF symD [OF sym]])