1.1 --- a/NEWS Tue Nov 30 08:58:47 2010 -0800
1.2 +++ b/NEWS Tue Nov 30 18:40:23 2010 +0100
1.3 @@ -92,6 +92,9 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* Abandoned locale equiv for equivalence relations. INCOMPATIBILITY: use
1.8 +equivI rather than equiv_intro.
1.9 +
1.10 * Code generator: globbing constant expressions "*" and "Theory.*" have been
1.11 replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.
1.12
2.1 --- a/src/HOL/Algebra/Coset.thy Tue Nov 30 08:58:47 2010 -0800
2.2 +++ b/src/HOL/Algebra/Coset.thy Tue Nov 30 18:40:23 2010 +0100
2.3 @@ -606,7 +606,7 @@
2.4 proof -
2.5 interpret group G by fact
2.6 show ?thesis
2.7 - proof (intro equiv.intro)
2.8 + proof (intro equivI)
2.9 show "refl_on (carrier G) (rcong H)"
2.10 by (auto simp add: r_congruent_def refl_on_def)
2.11 next
3.1 --- a/src/HOL/Equiv_Relations.thy Tue Nov 30 08:58:47 2010 -0800
3.2 +++ b/src/HOL/Equiv_Relations.thy Tue Nov 30 18:40:23 2010 +0100
3.3 @@ -8,13 +8,19 @@
3.4 imports Big_Operators Relation Plain
3.5 begin
3.6
3.7 -subsection {* Equivalence relations *}
3.8 +subsection {* Equivalence relations -- set version *}
3.9
3.10 -locale equiv =
3.11 - fixes A and r
3.12 - assumes refl_on: "refl_on A r"
3.13 - and sym: "sym r"
3.14 - and trans: "trans r"
3.15 +definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
3.16 + "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
3.17 +
3.18 +lemma equivI:
3.19 + "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
3.20 + by (simp add: equiv_def)
3.21 +
3.22 +lemma equivE:
3.23 + assumes "equiv A r"
3.24 + obtains "refl_on A r" and "sym r" and "trans r"
3.25 + using assms by (simp add: equiv_def)
3.26
3.27 text {*
3.28 Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
3.29 @@ -157,9 +163,17 @@
3.30 subsection {* Defining unary operations upon equivalence classes *}
3.31
3.32 text{*A congruence-preserving function*}
3.33 -locale congruent =
3.34 - fixes r and f
3.35 - assumes congruent: "(y,z) \<in> r ==> f y = f z"
3.36 +
3.37 +definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
3.38 + "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
3.39 +
3.40 +lemma congruentI:
3.41 + "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
3.42 + by (auto simp add: congruent_def)
3.43 +
3.44 +lemma congruentD:
3.45 + "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
3.46 + by (auto simp add: congruent_def)
3.47
3.48 abbreviation
3.49 RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
3.50 @@ -214,10 +228,18 @@
3.51 subsection {* Defining binary operations upon equivalence classes *}
3.52
3.53 text{*A congruence-preserving function of two arguments*}
3.54 -locale congruent2 =
3.55 - fixes r1 and r2 and f
3.56 - assumes congruent2:
3.57 - "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
3.58 +
3.59 +definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
3.60 + "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
3.61 +
3.62 +lemma congruent2I':
3.63 + assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
3.64 + shows "congruent2 r1 r2 f"
3.65 + using assms by (auto simp add: congruent2_def)
3.66 +
3.67 +lemma congruent2D:
3.68 + "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
3.69 + using assms by (auto simp add: congruent2_def)
3.70
3.71 text{*Abbreviation for the common case where the relations are identical*}
3.72 abbreviation
3.73 @@ -331,4 +353,99 @@
3.74 apply simp
3.75 done
3.76
3.77 +
3.78 +subsection {* Equivalence relations -- predicate version *}
3.79 +
3.80 +text {* Partial equivalences *}
3.81 +
3.82 +definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
3.83 + "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)"
3.84 + -- {* John-Harrison-style characterization *}
3.85 +
3.86 +lemma part_equivpI:
3.87 + "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
3.88 + by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE)
3.89 +
3.90 +lemma part_equivpE:
3.91 + assumes "part_equivp R"
3.92 + obtains x where "R x x" and "symp R" and "transp R"
3.93 +proof -
3.94 + from assms have 1: "\<exists>x. R x x"
3.95 + and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y"
3.96 + by (unfold part_equivp_def) blast+
3.97 + from 1 obtain x where "R x x" ..
3.98 + moreover have "symp R"
3.99 + proof (rule sympI)
3.100 + fix x y
3.101 + assume "R x y"
3.102 + with 2 [of x y] show "R y x" by auto
3.103 + qed
3.104 + moreover have "transp R"
3.105 + proof (rule transpI)
3.106 + fix x y z
3.107 + assume "R x y" and "R y z"
3.108 + with 2 [of x y] 2 [of y z] show "R x z" by auto
3.109 + qed
3.110 + ultimately show thesis by (rule that)
3.111 +qed
3.112 +
3.113 +lemma part_equivp_refl_symp_transp:
3.114 + "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R"
3.115 + by (auto intro: part_equivpI elim: part_equivpE)
3.116 +
3.117 +lemma part_equivp_symp:
3.118 + "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
3.119 + by (erule part_equivpE, erule sympE)
3.120 +
3.121 +lemma part_equivp_transp:
3.122 + "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
3.123 + by (erule part_equivpE, erule transpE)
3.124 +
3.125 +lemma part_equivp_typedef:
3.126 + "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
3.127 + by (auto elim: part_equivpE simp add: mem_def)
3.128 +
3.129 +
3.130 +text {* Total equivalences *}
3.131 +
3.132 +definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
3.133 + "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *}
3.134 +
3.135 +lemma equivpI:
3.136 + "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
3.137 + by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
3.138 +
3.139 +lemma equivpE:
3.140 + assumes "equivp R"
3.141 + obtains "reflp R" and "symp R" and "transp R"
3.142 + using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)
3.143 +
3.144 +lemma equivp_implies_part_equivp:
3.145 + "equivp R \<Longrightarrow> part_equivp R"
3.146 + by (auto intro: part_equivpI elim: equivpE reflpE)
3.147 +
3.148 +lemma equivp_equiv:
3.149 + "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
3.150 + by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def)
3.151 +
3.152 +lemma equivp_reflp_symp_transp:
3.153 + shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
3.154 + by (auto intro: equivpI elim: equivpE)
3.155 +
3.156 +lemma identity_equivp:
3.157 + "equivp (op =)"
3.158 + by (auto intro: equivpI reflpI sympI transpI)
3.159 +
3.160 +lemma equivp_reflp:
3.161 + "equivp R \<Longrightarrow> R x x"
3.162 + by (erule equivpE, erule reflpE)
3.163 +
3.164 +lemma equivp_symp:
3.165 + "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
3.166 + by (erule equivpE, erule sympE)
3.167 +
3.168 +lemma equivp_transp:
3.169 + "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
3.170 + by (erule equivpE, erule transpE)
3.171 +
3.172 end
4.1 --- a/src/HOL/Induct/QuoDataType.thy Tue Nov 30 08:58:47 2010 -0800
4.2 +++ b/src/HOL/Induct/QuoDataType.thy Tue Nov 30 18:40:23 2010 +0100
4.3 @@ -176,7 +176,7 @@
4.4 Abs_Msg (msgrel``{MPAIR U V})"
4.5 proof -
4.6 have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
4.7 - by (simp add: congruent2_def msgrel.MPAIR)
4.8 + by (auto simp add: congruent2_def msgrel.MPAIR)
4.9 thus ?thesis
4.10 by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
4.11 qed
4.12 @@ -184,7 +184,7 @@
4.13 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
4.14 proof -
4.15 have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
4.16 - by (simp add: congruent_def msgrel.CRYPT)
4.17 + by (auto simp add: congruent_def msgrel.CRYPT)
4.18 thus ?thesis
4.19 by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
4.20 qed
4.21 @@ -193,7 +193,7 @@
4.22 "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
4.23 proof -
4.24 have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
4.25 - by (simp add: congruent_def msgrel.DECRYPT)
4.26 + by (auto simp add: congruent_def msgrel.DECRYPT)
4.27 thus ?thesis
4.28 by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
4.29 qed
4.30 @@ -221,7 +221,7 @@
4.31 "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
4.32
4.33 lemma nonces_congruent: "freenonces respects msgrel"
4.34 -by (simp add: congruent_def msgrel_imp_eq_freenonces)
4.35 +by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
4.36
4.37
4.38 text{*Now prove the four equations for @{term nonces}*}
4.39 @@ -256,7 +256,7 @@
4.40 "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
4.41
4.42 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
4.43 -by (simp add: congruent_def msgrel_imp_eqv_freeleft)
4.44 +by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
4.45
4.46 text{*Now prove the four equations for @{term left}*}
4.47
4.48 @@ -290,7 +290,7 @@
4.49 "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
4.50
4.51 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
4.52 -by (simp add: congruent_def msgrel_imp_eqv_freeright)
4.53 +by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
4.54
4.55 text{*Now prove the four equations for @{term right}*}
4.56
4.57 @@ -425,7 +425,7 @@
4.58 "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
4.59
4.60 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
4.61 -by (simp add: congruent_def msgrel_imp_eq_freediscrim)
4.62 +by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
4.63
4.64 text{*Now prove the four equations for @{term discrim}*}
4.65
5.1 --- a/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 30 08:58:47 2010 -0800
5.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy Tue Nov 30 18:40:23 2010 +0100
5.3 @@ -125,14 +125,19 @@
5.4 | "freeargs (FNCALL F Xs) = Xs"
5.5
5.6 theorem exprel_imp_eqv_freeargs:
5.7 - "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
5.8 -apply (induct set: exprel)
5.9 -apply (erule_tac [4] listrel.induct)
5.10 -apply (simp_all add: listrel.intros)
5.11 -apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
5.12 -apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
5.13 -done
5.14 -
5.15 + assumes "U \<sim> V"
5.16 + shows "(freeargs U, freeargs V) \<in> listrel exprel"
5.17 +proof -
5.18 + from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
5.19 + from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
5.20 + from assms show ?thesis
5.21 + apply induct
5.22 + apply (erule_tac [4] listrel.induct)
5.23 + apply (simp_all add: listrel.intros)
5.24 + apply (blast intro: symD [OF sym])
5.25 + apply (blast intro: transD [OF trans])
5.26 + done
5.27 +qed
5.28
5.29
5.30 subsection{*The Initial Algebra: A Quotiented Message Type*}
5.31 @@ -220,7 +225,7 @@
5.32 Abs_Exp (exprel``{PLUS U V})"
5.33 proof -
5.34 have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
5.35 - by (simp add: congruent2_def exprel.PLUS)
5.36 + by (auto simp add: congruent2_def exprel.PLUS)
5.37 thus ?thesis
5.38 by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
5.39 qed
5.40 @@ -236,13 +241,13 @@
5.41
5.42 lemma FnCall_respects:
5.43 "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
5.44 - by (simp add: congruent_def exprel.FNCALL)
5.45 + by (auto simp add: congruent_def exprel.FNCALL)
5.46
5.47 lemma FnCall_sing:
5.48 "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
5.49 proof -
5.50 have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
5.51 - by (simp add: congruent_def FNCALL_Cons listrel.intros)
5.52 + by (auto simp add: congruent_def FNCALL_Cons listrel.intros)
5.53 thus ?thesis
5.54 by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
5.55 qed
5.56 @@ -255,7 +260,7 @@
5.57 "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
5.58 proof -
5.59 have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
5.60 - by (simp add: congruent_def exprel.FNCALL)
5.61 + by (auto simp add: congruent_def exprel.FNCALL)
5.62 thus ?thesis
5.63 by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
5.64 listset_Rep_Exp_Abs_Exp)
5.65 @@ -275,7 +280,7 @@
5.66 "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
5.67
5.68 lemma vars_respects: "freevars respects exprel"
5.69 -by (simp add: congruent_def exprel_imp_eq_freevars)
5.70 +by (auto simp add: congruent_def exprel_imp_eq_freevars)
5.71
5.72 text{*The extension of the function @{term vars} to lists*}
5.73 primrec vars_list :: "exp list \<Rightarrow> nat set" where
5.74 @@ -340,7 +345,7 @@
5.75 "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
5.76
5.77 lemma fun_respects: "(%U. {freefun U}) respects exprel"
5.78 -by (simp add: congruent_def exprel_imp_eq_freefun)
5.79 +by (auto simp add: congruent_def exprel_imp_eq_freefun)
5.80
5.81 lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
5.82 apply (cases Xs rule: eq_Abs_ExpList)
5.83 @@ -358,7 +363,7 @@
5.84 by (induct set: listrel) simp_all
5.85
5.86 lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
5.87 -by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
5.88 +by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
5.89
5.90 lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
5.91 apply (cases Xs rule: eq_Abs_ExpList)
5.92 @@ -387,7 +392,7 @@
5.93 "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
5.94
5.95 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
5.96 -by (simp add: congruent_def exprel_imp_eq_freediscrim)
5.97 +by (auto simp add: congruent_def exprel_imp_eq_freediscrim)
5.98
5.99 text{*Now prove the four equations for @{term discrim}*}
5.100
6.1 --- a/src/HOL/Int.thy Tue Nov 30 08:58:47 2010 -0800
6.2 +++ b/src/HOL/Int.thy Tue Nov 30 18:40:23 2010 +0100
6.3 @@ -102,7 +102,7 @@
6.4 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
6.5 proof -
6.6 have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
6.7 - by (simp add: congruent_def)
6.8 + by (auto simp add: congruent_def)
6.9 thus ?thesis
6.10 by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
6.11 qed
6.12 @@ -113,7 +113,7 @@
6.13 proof -
6.14 have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
6.15 respects2 intrel"
6.16 - by (simp add: congruent2_def)
6.17 + by (auto simp add: congruent2_def)
6.18 thus ?thesis
6.19 by (simp add: add_int_def UN_UN_split_split_eq
6.20 UN_equiv_class2 [OF equiv_intrel equiv_intrel])
6.21 @@ -288,7 +288,7 @@
6.22 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
6.23 proof -
6.24 have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
6.25 - by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
6.26 + by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
6.27 del: of_nat_add)
6.28 thus ?thesis
6.29 by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
6.30 @@ -394,7 +394,7 @@
6.31 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
6.32 proof -
6.33 have "(\<lambda>(x,y). {x-y}) respects intrel"
6.34 - by (simp add: congruent_def) arith
6.35 + by (auto simp add: congruent_def)
6.36 thus ?thesis
6.37 by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
6.38 qed
7.1 --- a/src/HOL/Library/Fraction_Field.thy Tue Nov 30 08:58:47 2010 -0800
7.2 +++ b/src/HOL/Library/Fraction_Field.thy Tue Nov 30 18:40:23 2010 +0100
7.3 @@ -43,7 +43,7 @@
7.4 qed
7.5
7.6 lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
7.7 - by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
7.8 + by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
7.9
7.10 lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
7.11 lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
7.12 @@ -121,7 +121,7 @@
7.13 lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
7.14 proof -
7.15 have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
7.16 - by (simp add: congruent_def)
7.17 + by (simp add: congruent_def split_paired_all)
7.18 then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
7.19 qed
7.20
8.1 --- a/src/HOL/Library/Quotient_List.thy Tue Nov 30 08:58:47 2010 -0800
8.2 +++ b/src/HOL/Library/Quotient_List.thy Tue Nov 30 18:40:23 2010 +0100
8.3 @@ -10,94 +10,96 @@
8.4
8.5 declare [[map list = (map, list_all2)]]
8.6
8.7 -lemma split_list_all:
8.8 - shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
8.9 - apply(auto)
8.10 - apply(case_tac x)
8.11 - apply(simp_all)
8.12 - done
8.13 +lemma map_id [id_simps]:
8.14 + "map id = id"
8.15 + by (simp add: id_def fun_eq_iff map.identity)
8.16
8.17 -lemma map_id[id_simps]:
8.18 - shows "map id = id"
8.19 - apply(simp add: fun_eq_iff)
8.20 - apply(rule allI)
8.21 - apply(induct_tac x)
8.22 - apply(simp_all)
8.23 - done
8.24 +lemma list_all2_map1:
8.25 + "list_all2 R (map f xs) ys \<longleftrightarrow> list_all2 (\<lambda>x. R (f x)) xs ys"
8.26 + by (induct xs ys rule: list_induct2') simp_all
8.27
8.28 -lemma list_all2_reflp:
8.29 - shows "equivp R \<Longrightarrow> list_all2 R xs xs"
8.30 - by (induct xs, simp_all add: equivp_reflp)
8.31 +lemma list_all2_map2:
8.32 + "list_all2 R xs (map f ys) \<longleftrightarrow> list_all2 (\<lambda>x y. R x (f y)) xs ys"
8.33 + by (induct xs ys rule: list_induct2') simp_all
8.34
8.35 -lemma list_all2_symp:
8.36 - assumes a: "equivp R"
8.37 - and b: "list_all2 R xs ys"
8.38 - shows "list_all2 R ys xs"
8.39 - using list_all2_lengthD[OF b] b
8.40 - apply(induct xs ys rule: list_induct2)
8.41 - apply(simp_all)
8.42 - apply(rule equivp_symp[OF a])
8.43 - apply(simp)
8.44 - done
8.45 +lemma list_all2_eq [id_simps]:
8.46 + "list_all2 (op =) = (op =)"
8.47 +proof (rule ext)+
8.48 + fix xs ys
8.49 + show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys"
8.50 + by (induct xs ys rule: list_induct2') simp_all
8.51 +qed
8.52
8.53 -lemma list_all2_transp:
8.54 - assumes a: "equivp R"
8.55 - and b: "list_all2 R xs1 xs2"
8.56 - and c: "list_all2 R xs2 xs3"
8.57 - shows "list_all2 R xs1 xs3"
8.58 - using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
8.59 - apply(induct rule: list_induct3)
8.60 - apply(simp_all)
8.61 - apply(auto intro: equivp_transp[OF a])
8.62 - done
8.63 +lemma list_reflp:
8.64 + assumes "reflp R"
8.65 + shows "reflp (list_all2 R)"
8.66 +proof (rule reflpI)
8.67 + from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
8.68 + fix xs
8.69 + show "list_all2 R xs xs"
8.70 + by (induct xs) (simp_all add: *)
8.71 +qed
8.72
8.73 -lemma list_equivp[quot_equiv]:
8.74 - assumes a: "equivp R"
8.75 - shows "equivp (list_all2 R)"
8.76 - apply (intro equivpI)
8.77 - unfolding reflp_def symp_def transp_def
8.78 - apply(simp add: list_all2_reflp[OF a])
8.79 - apply(blast intro: list_all2_symp[OF a])
8.80 - apply(blast intro: list_all2_transp[OF a])
8.81 - done
8.82 +lemma list_symp:
8.83 + assumes "symp R"
8.84 + shows "symp (list_all2 R)"
8.85 +proof (rule sympI)
8.86 + from assms have *: "\<And>xs ys. R xs ys \<Longrightarrow> R ys xs" by (rule sympE)
8.87 + fix xs ys
8.88 + assume "list_all2 R xs ys"
8.89 + then show "list_all2 R ys xs"
8.90 + by (induct xs ys rule: list_induct2') (simp_all add: *)
8.91 +qed
8.92
8.93 -lemma list_all2_rel:
8.94 - assumes q: "Quotient R Abs Rep"
8.95 - shows "list_all2 R r s = (list_all2 R r r \<and> list_all2 R s s \<and> (map Abs r = map Abs s))"
8.96 - apply(induct r s rule: list_induct2')
8.97 - apply(simp_all)
8.98 - using Quotient_rel[OF q]
8.99 - apply(metis)
8.100 - done
8.101 +lemma list_transp:
8.102 + assumes "transp R"
8.103 + shows "transp (list_all2 R)"
8.104 +proof (rule transpI)
8.105 + from assms have *: "\<And>xs ys zs. R xs ys \<Longrightarrow> R ys zs \<Longrightarrow> R xs zs" by (rule transpE)
8.106 + fix xs ys zs
8.107 + assume A: "list_all2 R xs ys" "list_all2 R ys zs"
8.108 + then have "length xs = length ys" "length ys = length zs" by (blast dest: list_all2_lengthD)+
8.109 + then show "list_all2 R xs zs" using A
8.110 + by (induct xs ys zs rule: list_induct3) (auto intro: *)
8.111 +qed
8.112
8.113 -lemma list_quotient[quot_thm]:
8.114 - assumes q: "Quotient R Abs Rep"
8.115 +lemma list_equivp [quot_equiv]:
8.116 + "equivp R \<Longrightarrow> equivp (list_all2 R)"
8.117 + by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
8.118 +
8.119 +lemma list_quotient [quot_thm]:
8.120 + assumes "Quotient R Abs Rep"
8.121 shows "Quotient (list_all2 R) (map Abs) (map Rep)"
8.122 - unfolding Quotient_def
8.123 - apply(subst split_list_all)
8.124 - apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
8.125 - apply(intro conjI allI)
8.126 - apply(induct_tac a)
8.127 - apply(simp_all add: Quotient_rep_reflp[OF q])
8.128 - apply(rule list_all2_rel[OF q])
8.129 - done
8.130 +proof (rule QuotientI)
8.131 + from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
8.132 + then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
8.133 +next
8.134 + from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
8.135 + then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
8.136 + by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
8.137 +next
8.138 + fix xs ys
8.139 + 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)
8.140 + 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"
8.141 + by (induct xs ys rule: list_induct2') auto
8.142 +qed
8.143
8.144 -lemma cons_prs[quot_preserve]:
8.145 +lemma cons_prs [quot_preserve]:
8.146 assumes q: "Quotient R Abs Rep"
8.147 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
8.148 by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
8.149
8.150 -lemma cons_rsp[quot_respect]:
8.151 +lemma cons_rsp [quot_respect]:
8.152 assumes q: "Quotient R Abs Rep"
8.153 shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
8.154 by auto
8.155
8.156 -lemma nil_prs[quot_preserve]:
8.157 +lemma nil_prs [quot_preserve]:
8.158 assumes q: "Quotient R Abs Rep"
8.159 shows "map Abs [] = []"
8.160 by simp
8.161
8.162 -lemma nil_rsp[quot_respect]:
8.163 +lemma nil_rsp [quot_respect]:
8.164 assumes q: "Quotient R Abs Rep"
8.165 shows "list_all2 R [] []"
8.166 by simp
8.167 @@ -109,7 +111,7 @@
8.168 by (induct l)
8.169 (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
8.170
8.171 -lemma map_prs[quot_preserve]:
8.172 +lemma map_prs [quot_preserve]:
8.173 assumes a: "Quotient R1 abs1 rep1"
8.174 and b: "Quotient R2 abs2 rep2"
8.175 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
8.176 @@ -117,8 +119,7 @@
8.177 by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
8.178 (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
8.179
8.180 -
8.181 -lemma map_rsp[quot_respect]:
8.182 +lemma map_rsp [quot_respect]:
8.183 assumes q1: "Quotient R1 Abs1 Rep1"
8.184 and q2: "Quotient R2 Abs2 Rep2"
8.185 shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
8.186 @@ -137,7 +138,7 @@
8.187 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
8.188 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
8.189
8.190 -lemma foldr_prs[quot_preserve]:
8.191 +lemma foldr_prs [quot_preserve]:
8.192 assumes a: "Quotient R1 abs1 rep1"
8.193 and b: "Quotient R2 abs2 rep2"
8.194 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
8.195 @@ -151,8 +152,7 @@
8.196 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
8.197 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
8.198
8.199 -
8.200 -lemma foldl_prs[quot_preserve]:
8.201 +lemma foldl_prs [quot_preserve]:
8.202 assumes a: "Quotient R1 abs1 rep1"
8.203 and b: "Quotient R2 abs2 rep2"
8.204 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
8.205 @@ -217,11 +217,11 @@
8.206 qed
8.207 qed
8.208
8.209 -lemma[quot_respect]:
8.210 +lemma [quot_respect]:
8.211 "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
8.212 by (simp add: list_all2_rsp fun_rel_def)
8.213
8.214 -lemma[quot_preserve]:
8.215 +lemma [quot_preserve]:
8.216 assumes a: "Quotient R abs1 rep1"
8.217 shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
8.218 apply (simp add: fun_eq_iff)
8.219 @@ -230,19 +230,11 @@
8.220 apply (simp_all add: Quotient_abs_rep[OF a])
8.221 done
8.222
8.223 -lemma[quot_preserve]:
8.224 +lemma [quot_preserve]:
8.225 assumes a: "Quotient R abs1 rep1"
8.226 shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
8.227 by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
8.228
8.229 -lemma list_all2_eq[id_simps]:
8.230 - shows "(list_all2 (op =)) = (op =)"
8.231 - unfolding fun_eq_iff
8.232 - apply(rule allI)+
8.233 - apply(induct_tac x xa rule: list_induct2')
8.234 - apply(simp_all)
8.235 - done
8.236 -
8.237 lemma list_all2_find_element:
8.238 assumes a: "x \<in> set a"
8.239 and b: "list_all2 R a b"
9.1 --- a/src/HOL/Library/Quotient_Option.thy Tue Nov 30 08:58:47 2010 -0800
9.2 +++ b/src/HOL/Library/Quotient_Option.thy Tue Nov 30 18:40:23 2010 +0100
9.3 @@ -18,64 +18,73 @@
9.4
9.5 declare [[map option = (Option.map, option_rel)]]
9.6
9.7 -text {* should probably be in Option.thy *}
9.8 -lemma split_option_all:
9.9 - shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
9.10 - apply(auto)
9.11 - apply(case_tac x)
9.12 - apply(simp_all)
9.13 +lemma option_rel_unfold:
9.14 + "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
9.15 + | (Some x, Some y) \<Rightarrow> R x y
9.16 + | _ \<Rightarrow> False)"
9.17 + by (cases x) (cases y, simp_all)+
9.18 +
9.19 +lemma option_rel_map1:
9.20 + "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
9.21 + by (simp add: option_rel_unfold split: option.split)
9.22 +
9.23 +lemma option_rel_map2:
9.24 + "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
9.25 + by (simp add: option_rel_unfold split: option.split)
9.26 +
9.27 +lemma option_map_id [id_simps]:
9.28 + "Option.map id = id"
9.29 + by (simp add: id_def Option.map.identity fun_eq_iff)
9.30 +
9.31 +lemma option_rel_eq [id_simps]:
9.32 + "option_rel (op =) = (op =)"
9.33 + by (simp add: option_rel_unfold fun_eq_iff split: option.split)
9.34 +
9.35 +lemma option_reflp:
9.36 + "reflp R \<Longrightarrow> reflp (option_rel R)"
9.37 + by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
9.38 +
9.39 +lemma option_symp:
9.40 + "symp R \<Longrightarrow> symp (option_rel R)"
9.41 + by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
9.42 +
9.43 +lemma option_transp:
9.44 + "transp R \<Longrightarrow> transp (option_rel R)"
9.45 + by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
9.46 +
9.47 +lemma option_equivp [quot_equiv]:
9.48 + "equivp R \<Longrightarrow> equivp (option_rel R)"
9.49 + by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
9.50 +
9.51 +lemma option_quotient [quot_thm]:
9.52 + assumes "Quotient R Abs Rep"
9.53 + shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
9.54 + apply (rule QuotientI)
9.55 + 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])
9.56 + using Quotient_rel [OF assms]
9.57 + apply (simp add: option_rel_unfold split: option.split)
9.58 done
9.59
9.60 -lemma option_quotient[quot_thm]:
9.61 - assumes q: "Quotient R Abs Rep"
9.62 - shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
9.63 - unfolding Quotient_def
9.64 - apply(simp add: split_option_all)
9.65 - apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
9.66 - using q
9.67 - unfolding Quotient_def
9.68 - apply(blast)
9.69 - done
9.70 -
9.71 -lemma option_equivp[quot_equiv]:
9.72 - assumes a: "equivp R"
9.73 - shows "equivp (option_rel R)"
9.74 - apply(rule equivpI)
9.75 - unfolding reflp_def symp_def transp_def
9.76 - apply(simp_all add: split_option_all)
9.77 - apply(blast intro: equivp_reflp[OF a])
9.78 - apply(blast intro: equivp_symp[OF a])
9.79 - apply(blast intro: equivp_transp[OF a])
9.80 - done
9.81 -
9.82 -lemma option_None_rsp[quot_respect]:
9.83 +lemma option_None_rsp [quot_respect]:
9.84 assumes q: "Quotient R Abs Rep"
9.85 shows "option_rel R None None"
9.86 by simp
9.87
9.88 -lemma option_Some_rsp[quot_respect]:
9.89 +lemma option_Some_rsp [quot_respect]:
9.90 assumes q: "Quotient R Abs Rep"
9.91 shows "(R ===> option_rel R) Some Some"
9.92 by auto
9.93
9.94 -lemma option_None_prs[quot_preserve]:
9.95 +lemma option_None_prs [quot_preserve]:
9.96 assumes q: "Quotient R Abs Rep"
9.97 shows "Option.map Abs None = None"
9.98 by simp
9.99
9.100 -lemma option_Some_prs[quot_preserve]:
9.101 +lemma option_Some_prs [quot_preserve]:
9.102 assumes q: "Quotient R Abs Rep"
9.103 shows "(Rep ---> Option.map Abs) Some = Some"
9.104 apply(simp add: fun_eq_iff)
9.105 apply(simp add: Quotient_abs_rep[OF q])
9.106 done
9.107
9.108 -lemma option_map_id[id_simps]:
9.109 - shows "Option.map id = id"
9.110 - by (simp add: fun_eq_iff split_option_all)
9.111 -
9.112 -lemma option_rel_eq[id_simps]:
9.113 - shows "option_rel (op =) = (op =)"
9.114 - by (simp add: fun_eq_iff split_option_all)
9.115 -
9.116 end
10.1 --- a/src/HOL/Library/Quotient_Product.thy Tue Nov 30 08:58:47 2010 -0800
10.2 +++ b/src/HOL/Library/Quotient_Product.thy Tue Nov 30 18:40:23 2010 +0100
10.3 @@ -19,38 +19,39 @@
10.4 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
10.5 by (simp add: prod_rel_def)
10.6
10.7 -lemma prod_equivp[quot_equiv]:
10.8 - assumes a: "equivp R1"
10.9 - assumes b: "equivp R2"
10.10 +lemma map_pair_id [id_simps]:
10.11 + shows "map_pair id id = id"
10.12 + by (simp add: fun_eq_iff)
10.13 +
10.14 +lemma prod_rel_eq [id_simps]:
10.15 + shows "prod_rel (op =) (op =) = (op =)"
10.16 + by (simp add: fun_eq_iff)
10.17 +
10.18 +lemma prod_equivp [quot_equiv]:
10.19 + assumes "equivp R1"
10.20 + assumes "equivp R2"
10.21 shows "equivp (prod_rel R1 R2)"
10.22 - apply(rule equivpI)
10.23 - unfolding reflp_def symp_def transp_def
10.24 - apply(simp_all add: split_paired_all prod_rel_def)
10.25 - apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
10.26 - apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
10.27 - apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
10.28 + using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
10.29 +
10.30 +lemma prod_quotient [quot_thm]:
10.31 + assumes "Quotient R1 Abs1 Rep1"
10.32 + assumes "Quotient R2 Abs2 Rep2"
10.33 + shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
10.34 + apply (rule QuotientI)
10.35 + apply (simp add: map_pair.compositionality map_pair.identity
10.36 + Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
10.37 + apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
10.38 + using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
10.39 + apply (auto simp add: split_paired_all)
10.40 done
10.41
10.42 -lemma prod_quotient[quot_thm]:
10.43 - assumes q1: "Quotient R1 Abs1 Rep1"
10.44 - assumes q2: "Quotient R2 Abs2 Rep2"
10.45 - shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
10.46 - unfolding Quotient_def
10.47 - apply(simp add: split_paired_all)
10.48 - apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
10.49 - apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
10.50 - using q1 q2
10.51 - unfolding Quotient_def
10.52 - apply(blast)
10.53 - done
10.54 -
10.55 -lemma Pair_rsp[quot_respect]:
10.56 +lemma Pair_rsp [quot_respect]:
10.57 assumes q1: "Quotient R1 Abs1 Rep1"
10.58 assumes q2: "Quotient R2 Abs2 Rep2"
10.59 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
10.60 by (auto simp add: prod_rel_def)
10.61
10.62 -lemma Pair_prs[quot_preserve]:
10.63 +lemma Pair_prs [quot_preserve]:
10.64 assumes q1: "Quotient R1 Abs1 Rep1"
10.65 assumes q2: "Quotient R2 Abs2 Rep2"
10.66 shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
10.67 @@ -58,35 +59,35 @@
10.68 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
10.69 done
10.70
10.71 -lemma fst_rsp[quot_respect]:
10.72 +lemma fst_rsp [quot_respect]:
10.73 assumes "Quotient R1 Abs1 Rep1"
10.74 assumes "Quotient R2 Abs2 Rep2"
10.75 shows "(prod_rel R1 R2 ===> R1) fst fst"
10.76 by auto
10.77
10.78 -lemma fst_prs[quot_preserve]:
10.79 +lemma fst_prs [quot_preserve]:
10.80 assumes q1: "Quotient R1 Abs1 Rep1"
10.81 assumes q2: "Quotient R2 Abs2 Rep2"
10.82 shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
10.83 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
10.84
10.85 -lemma snd_rsp[quot_respect]:
10.86 +lemma snd_rsp [quot_respect]:
10.87 assumes "Quotient R1 Abs1 Rep1"
10.88 assumes "Quotient R2 Abs2 Rep2"
10.89 shows "(prod_rel R1 R2 ===> R2) snd snd"
10.90 by auto
10.91
10.92 -lemma snd_prs[quot_preserve]:
10.93 +lemma snd_prs [quot_preserve]:
10.94 assumes q1: "Quotient R1 Abs1 Rep1"
10.95 assumes q2: "Quotient R2 Abs2 Rep2"
10.96 shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
10.97 by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
10.98
10.99 -lemma split_rsp[quot_respect]:
10.100 +lemma split_rsp [quot_respect]:
10.101 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
10.102 by (auto intro!: fun_relI elim!: fun_relE)
10.103
10.104 -lemma split_prs[quot_preserve]:
10.105 +lemma split_prs [quot_preserve]:
10.106 assumes q1: "Quotient R1 Abs1 Rep1"
10.107 and q2: "Quotient R2 Abs2 Rep2"
10.108 shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
10.109 @@ -111,12 +112,4 @@
10.110
10.111 declare Pair_eq[quot_preserve]
10.112
10.113 -lemma map_pair_id[id_simps]:
10.114 - shows "map_pair id id = id"
10.115 - by (simp add: fun_eq_iff)
10.116 -
10.117 -lemma prod_rel_eq[id_simps]:
10.118 - shows "prod_rel (op =) (op =) = (op =)"
10.119 - by (simp add: fun_eq_iff)
10.120 -
10.121 end
11.1 --- a/src/HOL/Library/Quotient_Sum.thy Tue Nov 30 08:58:47 2010 -0800
11.2 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Nov 30 18:40:23 2010 +0100
11.3 @@ -18,53 +18,68 @@
11.4
11.5 declare [[map sum = (sum_map, sum_rel)]]
11.6
11.7 +lemma sum_rel_unfold:
11.8 + "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
11.9 + | (Inr x, Inr y) \<Rightarrow> R2 x y
11.10 + | _ \<Rightarrow> False)"
11.11 + by (cases x) (cases y, simp_all)+
11.12
11.13 -text {* should probably be in @{theory Sum_Type} *}
11.14 -lemma split_sum_all:
11.15 - shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
11.16 - apply(auto)
11.17 - apply(case_tac x)
11.18 - apply(simp_all)
11.19 - done
11.20 +lemma sum_rel_map1:
11.21 + "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"
11.22 + by (simp add: sum_rel_unfold split: sum.split)
11.23
11.24 -lemma sum_equivp[quot_equiv]:
11.25 - assumes a: "equivp R1"
11.26 - assumes b: "equivp R2"
11.27 - shows "equivp (sum_rel R1 R2)"
11.28 - apply(rule equivpI)
11.29 - unfolding reflp_def symp_def transp_def
11.30 - apply(simp_all add: split_sum_all)
11.31 - apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
11.32 - apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
11.33 - apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
11.34 - done
11.35 +lemma sum_rel_map2:
11.36 + "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"
11.37 + by (simp add: sum_rel_unfold split: sum.split)
11.38
11.39 -lemma sum_quotient[quot_thm]:
11.40 +lemma sum_map_id [id_simps]:
11.41 + "sum_map id id = id"
11.42 + by (simp add: id_def sum_map.identity fun_eq_iff)
11.43 +
11.44 +lemma sum_rel_eq [id_simps]:
11.45 + "sum_rel (op =) (op =) = (op =)"
11.46 + by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
11.47 +
11.48 +lemma sum_reflp:
11.49 + "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
11.50 + by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
11.51 +
11.52 +lemma sum_symp:
11.53 + "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
11.54 + by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
11.55 +
11.56 +lemma sum_transp:
11.57 + "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
11.58 + by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
11.59 +
11.60 +lemma sum_equivp [quot_equiv]:
11.61 + "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
11.62 + by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
11.63 +
11.64 +lemma sum_quotient [quot_thm]:
11.65 assumes q1: "Quotient R1 Abs1 Rep1"
11.66 assumes q2: "Quotient R2 Abs2 Rep2"
11.67 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
11.68 - unfolding Quotient_def
11.69 - apply(simp add: split_sum_all)
11.70 - apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
11.71 - apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
11.72 - using q1 q2
11.73 - unfolding Quotient_def
11.74 - apply(blast)+
11.75 + apply (rule QuotientI)
11.76 + apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
11.77 + Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
11.78 + using Quotient_rel [OF q1] Quotient_rel [OF q2]
11.79 + apply (simp add: sum_rel_unfold split: sum.split)
11.80 done
11.81
11.82 -lemma sum_Inl_rsp[quot_respect]:
11.83 +lemma sum_Inl_rsp [quot_respect]:
11.84 assumes q1: "Quotient R1 Abs1 Rep1"
11.85 assumes q2: "Quotient R2 Abs2 Rep2"
11.86 shows "(R1 ===> sum_rel R1 R2) Inl Inl"
11.87 by auto
11.88
11.89 -lemma sum_Inr_rsp[quot_respect]:
11.90 +lemma sum_Inr_rsp [quot_respect]:
11.91 assumes q1: "Quotient R1 Abs1 Rep1"
11.92 assumes q2: "Quotient R2 Abs2 Rep2"
11.93 shows "(R2 ===> sum_rel R1 R2) Inr Inr"
11.94 by auto
11.95
11.96 -lemma sum_Inl_prs[quot_preserve]:
11.97 +lemma sum_Inl_prs [quot_preserve]:
11.98 assumes q1: "Quotient R1 Abs1 Rep1"
11.99 assumes q2: "Quotient R2 Abs2 Rep2"
11.100 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
11.101 @@ -72,7 +87,7 @@
11.102 apply(simp add: Quotient_abs_rep[OF q1])
11.103 done
11.104
11.105 -lemma sum_Inr_prs[quot_preserve]:
11.106 +lemma sum_Inr_prs [quot_preserve]:
11.107 assumes q1: "Quotient R1 Abs1 Rep1"
11.108 assumes q2: "Quotient R2 Abs2 Rep2"
11.109 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
11.110 @@ -80,12 +95,4 @@
11.111 apply(simp add: Quotient_abs_rep[OF q2])
11.112 done
11.113
11.114 -lemma sum_map_id[id_simps]:
11.115 - shows "sum_map id id = id"
11.116 - by (simp add: fun_eq_iff split_sum_all)
11.117 -
11.118 -lemma sum_rel_eq[id_simps]:
11.119 - shows "sum_rel (op =) (op =) = (op =)"
11.120 - by (simp add: fun_eq_iff split_sum_all)
11.121 -
11.122 end
12.1 --- a/src/HOL/NSA/StarDef.thy Tue Nov 30 08:58:47 2010 -0800
12.2 +++ b/src/HOL/NSA/StarDef.thy Tue Nov 30 18:40:23 2010 +0100
12.3 @@ -62,7 +62,7 @@
12.4 by (simp add: starrel_def)
12.5
12.6 lemma equiv_starrel: "equiv UNIV starrel"
12.7 -proof (rule equiv.intro)
12.8 +proof (rule equivI)
12.9 show "refl starrel" by (simp add: refl_on_def)
12.10 show "sym starrel" by (simp add: sym_def eq_commute)
12.11 show "trans starrel" by (auto intro: transI elim!: ultra)
13.1 --- a/src/HOL/Predicate.thy Tue Nov 30 08:58:47 2010 -0800
13.2 +++ b/src/HOL/Predicate.thy Tue Nov 30 18:40:23 2010 +0100
13.3 @@ -363,6 +363,44 @@
13.4 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
13.5 "single_valuedP r == single_valued {(x, y). r x y}"
13.6
13.7 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
13.8 +
13.9 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
13.10 + "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
13.11 +
13.12 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
13.13 + "symp r \<longleftrightarrow> sym {(x, y). r x y}"
13.14 +
13.15 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
13.16 + "transp r \<longleftrightarrow> trans {(x, y). r x y}"
13.17 +
13.18 +lemma reflpI:
13.19 + "(\<And>x. r x x) \<Longrightarrow> reflp r"
13.20 + by (auto intro: refl_onI simp add: reflp_def)
13.21 +
13.22 +lemma reflpE:
13.23 + assumes "reflp r"
13.24 + obtains "r x x"
13.25 + using assms by (auto dest: refl_onD simp add: reflp_def)
13.26 +
13.27 +lemma sympI:
13.28 + "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
13.29 + by (auto intro: symI simp add: symp_def)
13.30 +
13.31 +lemma sympE:
13.32 + assumes "symp r" and "r x y"
13.33 + obtains "r y x"
13.34 + using assms by (auto dest: symD simp add: symp_def)
13.35 +
13.36 +lemma transpI:
13.37 + "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
13.38 + by (auto intro: transI simp add: transp_def)
13.39 +
13.40 +lemma transpE:
13.41 + assumes "transp r" and "r x y" and "r y z"
13.42 + obtains "r x z"
13.43 + using assms by (auto dest: transD simp add: transp_def)
13.44 +
13.45
13.46 subsection {* Predicates as enumerations *}
13.47
14.1 --- a/src/HOL/Quotient.thy Tue Nov 30 08:58:47 2010 -0800
14.2 +++ b/src/HOL/Quotient.thy Tue Nov 30 18:40:23 2010 +0100
14.3 @@ -14,131 +14,15 @@
14.4 ("Tools/Quotient/quotient_tacs.ML")
14.5 begin
14.6
14.7 -
14.8 text {*
14.9 Basic definition for equivalence relations
14.10 that are represented by predicates.
14.11 *}
14.12
14.13 -definition
14.14 - "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
14.15 -
14.16 -lemma refl_reflp:
14.17 - "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
14.18 - by (simp add: refl_on_def reflp_def)
14.19 -
14.20 -definition
14.21 - "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
14.22 -
14.23 -lemma sym_symp:
14.24 - "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
14.25 - by (simp add: sym_def symp_def)
14.26 -
14.27 -definition
14.28 - "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
14.29 -
14.30 -lemma trans_transp:
14.31 - "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
14.32 - by (auto simp add: trans_def transp_def)
14.33 -
14.34 -definition
14.35 - "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
14.36 -
14.37 -lemma equivp_reflp_symp_transp:
14.38 - shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
14.39 - unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
14.40 - by blast
14.41 -
14.42 -lemma equiv_equivp:
14.43 - "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
14.44 - by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
14.45 -
14.46 -lemma equivp_reflp:
14.47 - shows "equivp E \<Longrightarrow> E x x"
14.48 - by (simp only: equivp_reflp_symp_transp reflp_def)
14.49 -
14.50 -lemma equivp_symp:
14.51 - shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
14.52 - by (simp add: equivp_def)
14.53 -
14.54 -lemma equivp_transp:
14.55 - shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
14.56 - by (simp add: equivp_def)
14.57 -
14.58 -lemma equivpI:
14.59 - assumes "reflp R" "symp R" "transp R"
14.60 - shows "equivp R"
14.61 - using assms by (simp add: equivp_reflp_symp_transp)
14.62 -
14.63 -lemma identity_equivp:
14.64 - shows "equivp (op =)"
14.65 - unfolding equivp_def
14.66 - by auto
14.67 -
14.68 -text {* Partial equivalences *}
14.69 -
14.70 -definition
14.71 - "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)))"
14.72 -
14.73 -lemma equivp_implies_part_equivp:
14.74 - assumes a: "equivp E"
14.75 - shows "part_equivp E"
14.76 - using a
14.77 - unfolding equivp_def part_equivp_def
14.78 - by auto
14.79 -
14.80 -lemma part_equivp_symp:
14.81 - assumes e: "part_equivp R"
14.82 - and a: "R x y"
14.83 - shows "R y x"
14.84 - using e[simplified part_equivp_def] a
14.85 - by (metis)
14.86 -
14.87 -lemma part_equivp_typedef:
14.88 - shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
14.89 - unfolding part_equivp_def mem_def
14.90 - apply clarify
14.91 - apply (intro exI)
14.92 - apply (rule conjI)
14.93 - apply assumption
14.94 - apply (rule refl)
14.95 - done
14.96 -
14.97 -lemma part_equivp_refl_symp_transp:
14.98 - shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
14.99 -proof
14.100 - assume "part_equivp E"
14.101 - then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
14.102 - unfolding part_equivp_def symp_def transp_def
14.103 - by metis
14.104 -next
14.105 - assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
14.106 - 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)"
14.107 - unfolding symp_def transp_def by (metis, metis)
14.108 - have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
14.109 - proof (intro allI iffI conjI)
14.110 - fix x y
14.111 - assume d: "E x y"
14.112 - then show "E x x" using b c by metis
14.113 - show "E y y" using b c d by metis
14.114 - show "E x = E y" unfolding fun_eq_iff using b c d by metis
14.115 - next
14.116 - fix x y
14.117 - assume "E x x \<and> E y y \<and> E x = E y"
14.118 - then show "E x y" using b c by metis
14.119 - qed
14.120 - then show "part_equivp E" unfolding part_equivp_def using a by metis
14.121 -qed
14.122 -
14.123 -lemma part_equivpI:
14.124 - assumes "\<exists>x. R x x" "symp R" "transp R"
14.125 - shows "part_equivp R"
14.126 - using assms by (simp add: part_equivp_refl_symp_transp)
14.127 -
14.128 text {* Composition of Relations *}
14.129
14.130 abbreviation
14.131 - rel_conj (infixr "OOO" 75)
14.132 + rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
14.133 where
14.134 "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
14.135
14.136 @@ -169,16 +53,16 @@
14.137 definition
14.138 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)
14.139 where
14.140 - "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
14.141 + "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
14.142
14.143 lemma fun_relI [intro]:
14.144 - assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
14.145 - shows "(E1 ===> E2) f g"
14.146 + assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
14.147 + shows "(R1 ===> R2) f g"
14.148 using assms by (simp add: fun_rel_def)
14.149
14.150 lemma fun_relE:
14.151 - assumes "(E1 ===> E2) f g" and "E1 x y"
14.152 - obtains "E2 (f x) (g y)"
14.153 + assumes "(R1 ===> R2) f g" and "R1 x y"
14.154 + obtains "R2 (f x) (g y)"
14.155 using assms by (simp add: fun_rel_def)
14.156
14.157 lemma fun_rel_eq:
14.158 @@ -189,34 +73,41 @@
14.159 subsection {* Quotient Predicate *}
14.160
14.161 definition
14.162 - "Quotient E Abs Rep \<longleftrightarrow>
14.163 - (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
14.164 - (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
14.165 + "Quotient R Abs Rep \<longleftrightarrow>
14.166 + (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
14.167 + (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
14.168 +
14.169 +lemma QuotientI:
14.170 + assumes "\<And>a. Abs (Rep a) = a"
14.171 + and "\<And>a. R (Rep a) (Rep a)"
14.172 + and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
14.173 + shows "Quotient R Abs Rep"
14.174 + using assms unfolding Quotient_def by blast
14.175
14.176 lemma Quotient_abs_rep:
14.177 - assumes a: "Quotient E Abs Rep"
14.178 + assumes a: "Quotient R Abs Rep"
14.179 shows "Abs (Rep a) = a"
14.180 using a
14.181 unfolding Quotient_def
14.182 by simp
14.183
14.184 lemma Quotient_rep_reflp:
14.185 - assumes a: "Quotient E Abs Rep"
14.186 - shows "E (Rep a) (Rep a)"
14.187 + assumes a: "Quotient R Abs Rep"
14.188 + shows "R (Rep a) (Rep a)"
14.189 using a
14.190 unfolding Quotient_def
14.191 by blast
14.192
14.193 lemma Quotient_rel:
14.194 - assumes a: "Quotient E Abs Rep"
14.195 - shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
14.196 + assumes a: "Quotient R Abs Rep"
14.197 + shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
14.198 using a
14.199 unfolding Quotient_def
14.200 by blast
14.201
14.202 lemma Quotient_rel_rep:
14.203 assumes a: "Quotient R Abs Rep"
14.204 - shows "R (Rep a) (Rep b) = (a = b)"
14.205 + shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
14.206 using a
14.207 unfolding Quotient_def
14.208 by metis
14.209 @@ -228,22 +119,20 @@
14.210 by blast
14.211
14.212 lemma Quotient_rel_abs:
14.213 - assumes a: "Quotient E Abs Rep"
14.214 - shows "E r s \<Longrightarrow> Abs r = Abs s"
14.215 + assumes a: "Quotient R Abs Rep"
14.216 + shows "R r s \<Longrightarrow> Abs r = Abs s"
14.217 using a unfolding Quotient_def
14.218 by blast
14.219
14.220 lemma Quotient_symp:
14.221 - assumes a: "Quotient E Abs Rep"
14.222 - shows "symp E"
14.223 - using a unfolding Quotient_def symp_def
14.224 - by metis
14.225 + assumes a: "Quotient R Abs Rep"
14.226 + shows "symp R"
14.227 + using a unfolding Quotient_def using sympI by metis
14.228
14.229 lemma Quotient_transp:
14.230 - assumes a: "Quotient E Abs Rep"
14.231 - shows "transp E"
14.232 - using a unfolding Quotient_def transp_def
14.233 - by metis
14.234 + assumes a: "Quotient R Abs Rep"
14.235 + shows "transp R"
14.236 + using a unfolding Quotient_def using transpI by metis
14.237
14.238 lemma identity_quotient:
14.239 shows "Quotient (op =) id id"
14.240 @@ -291,8 +180,7 @@
14.241 and a: "R xa xb" "R ya yb"
14.242 shows "R xa ya = R xb yb"
14.243 using a Quotient_symp[OF q] Quotient_transp[OF q]
14.244 - unfolding symp_def transp_def
14.245 - by blast
14.246 + by (blast elim: sympE transpE)
14.247
14.248 lemma lambda_prs:
14.249 assumes q1: "Quotient R1 Abs1 Rep1"
14.250 @@ -300,7 +188,7 @@
14.251 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
14.252 unfolding fun_eq_iff
14.253 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
14.254 - by (simp add:)
14.255 + by simp
14.256
14.257 lemma lambda_prs1:
14.258 assumes q1: "Quotient R1 Abs1 Rep1"
14.259 @@ -308,7 +196,7 @@
14.260 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
14.261 unfolding fun_eq_iff
14.262 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
14.263 - by (simp add:)
14.264 + by simp
14.265
14.266 lemma rep_abs_rsp:
14.267 assumes q: "Quotient R Abs Rep"
14.268 @@ -392,9 +280,7 @@
14.269 apply(simp add: in_respects fun_rel_def)
14.270 apply(rule impI)
14.271 using a equivp_reflp_symp_transp[of "R2"]
14.272 - apply(simp add: reflp_def)
14.273 - apply(simp)
14.274 - apply(simp)
14.275 + apply (auto elim: equivpE reflpE)
14.276 done
14.277
14.278 lemma bex_reg_eqv_range:
14.279 @@ -406,7 +292,7 @@
14.280 apply(simp add: Respects_def in_respects fun_rel_def)
14.281 apply(rule impI)
14.282 using a equivp_reflp_symp_transp[of "R2"]
14.283 - apply(simp add: reflp_def)
14.284 + apply (auto elim: equivpE reflpE)
14.285 done
14.286
14.287 (* Next four lemmas are unused *)
15.1 --- a/src/HOL/Quotient_Examples/FSet.thy Tue Nov 30 08:58:47 2010 -0800
15.2 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Nov 30 18:40:23 2010 +0100
15.3 @@ -19,11 +19,21 @@
15.4 where
15.5 [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
15.6
15.7 +lemma list_eq_reflp:
15.8 + "reflp list_eq"
15.9 + by (auto intro: reflpI)
15.10 +
15.11 +lemma list_eq_symp:
15.12 + "symp list_eq"
15.13 + by (auto intro: sympI)
15.14 +
15.15 +lemma list_eq_transp:
15.16 + "transp list_eq"
15.17 + by (auto intro: transpI)
15.18 +
15.19 lemma list_eq_equivp:
15.20 - shows "equivp list_eq"
15.21 - unfolding equivp_reflp_symp_transp
15.22 - unfolding reflp_def symp_def transp_def
15.23 - by auto
15.24 + "equivp list_eq"
15.25 + by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)
15.26
15.27 text {* The @{text fset} type *}
15.28
15.29 @@ -141,7 +151,7 @@
15.30 \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
15.31 then have s: "(list_all2 R OOO op \<approx>) s s" by simp
15.32 have d: "map Abs r \<approx> map Abs s"
15.33 - by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
15.34 + by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
15.35 have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
15.36 by (rule map_list_eq_cong[OF d])
15.37 have y: "list_all2 R (map Rep (map Abs s)) s"
15.38 @@ -267,8 +277,11 @@
15.39 proof (rule fun_relI, elim pred_compE)
15.40 fix a b ba bb
15.41 assume a: "list_all2 op \<approx> a ba"
15.42 + with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
15.43 assume b: "ba \<approx> bb"
15.44 + with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
15.45 assume c: "list_all2 op \<approx> bb b"
15.46 + with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
15.47 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
15.48 proof
15.49 fix x
15.50 @@ -278,9 +291,6 @@
15.51 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
15.52 next
15.53 assume e: "\<exists>xa\<in>set b. x \<in> set xa"
15.54 - have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
15.55 - have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
15.56 - have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
15.57 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
15.58 qed
15.59 qed
15.60 @@ -288,7 +298,6 @@
15.61 qed
15.62
15.63
15.64 -
15.65 section {* Quotient definitions for fsets *}
15.66
15.67
15.68 @@ -474,7 +483,7 @@
15.69 assumes a: "reflp R"
15.70 and b: "list_all2 R l r"
15.71 shows "list_all2 R (z @ l) (z @ r)"
15.72 - by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
15.73 + using a b by (induct z) (auto elim: reflpE)
15.74
15.75 lemma append_rsp2_pre0:
15.76 assumes a:"list_all2 op \<approx> x x'"
15.77 @@ -489,23 +498,14 @@
15.78 apply (rule list_all2_refl'[OF list_eq_equivp])
15.79 apply (simp_all del: list_eq_def)
15.80 apply (rule list_all2_app_l)
15.81 - apply (simp_all add: reflp_def)
15.82 + apply (simp_all add: reflpI)
15.83 done
15.84
15.85 lemma append_rsp2_pre:
15.86 - assumes a:"list_all2 op \<approx> x x'"
15.87 - and b: "list_all2 op \<approx> z z'"
15.88 + assumes "list_all2 op \<approx> x x'"
15.89 + and "list_all2 op \<approx> z z'"
15.90 shows "list_all2 op \<approx> (x @ z) (x' @ z')"
15.91 - apply (rule list_all2_transp[OF fset_equivp])
15.92 - apply (rule append_rsp2_pre0)
15.93 - apply (rule a)
15.94 - using b apply (induct z z' rule: list_induct2')
15.95 - apply (simp_all only: append_Nil2)
15.96 - apply (rule list_all2_refl'[OF list_eq_equivp])
15.97 - apply simp_all
15.98 - apply (rule append_rsp2_pre1)
15.99 - apply simp
15.100 - done
15.101 + using assms by (rule list_all2_appendI)
15.102
15.103 lemma append_rsp2 [quot_respect]:
15.104 "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
16.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Nov 30 08:58:47 2010 -0800
16.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Nov 30 18:40:23 2010 +0100
16.3 @@ -36,16 +36,16 @@
16.4
16.5 theorem equiv_msgrel: "equivp msgrel"
16.6 proof (rule equivpI)
16.7 - show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
16.8 - show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
16.9 - show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
16.10 + show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
16.11 + show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
16.12 + show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
16.13 qed
16.14
16.15 subsection{*Some Functions on the Free Algebra*}
16.16
16.17 subsubsection{*The Set of Nonces*}
16.18
16.19 -fun
16.20 +primrec
16.21 freenonces :: "freemsg \<Rightarrow> nat set"
16.22 where
16.23 "freenonces (NONCE N) = {N}"
16.24 @@ -62,7 +62,7 @@
16.25
16.26 text{*A function to return the left part of the top pair in a message. It will
16.27 be lifted to the initial algrebra, to serve as an example of that process.*}
16.28 -fun
16.29 +primrec
16.30 freeleft :: "freemsg \<Rightarrow> freemsg"
16.31 where
16.32 "freeleft (NONCE N) = NONCE N"
16.33 @@ -75,7 +75,7 @@
16.34 (the abstract constructor) is injective*}
16.35 lemma msgrel_imp_eqv_freeleft_aux:
16.36 shows "freeleft U \<sim> freeleft U"
16.37 - by (induct rule: freeleft.induct) (auto)
16.38 + by (fact msgrel_refl)
16.39
16.40 theorem msgrel_imp_eqv_freeleft:
16.41 assumes a: "U \<sim> V"
16.42 @@ -86,7 +86,7 @@
16.43 subsubsection{*The Right Projection*}
16.44
16.45 text{*A function to return the right part of the top pair in a message.*}
16.46 -fun
16.47 +primrec
16.48 freeright :: "freemsg \<Rightarrow> freemsg"
16.49 where
16.50 "freeright (NONCE N) = NONCE N"
16.51 @@ -99,7 +99,7 @@
16.52 (the abstract constructor) is injective*}
16.53 lemma msgrel_imp_eqv_freeright_aux:
16.54 shows "freeright U \<sim> freeright U"
16.55 - by (induct rule: freeright.induct) (auto)
16.56 + by (fact msgrel_refl)
16.57
16.58 theorem msgrel_imp_eqv_freeright:
16.59 assumes a: "U \<sim> V"
16.60 @@ -110,7 +110,7 @@
16.61 subsubsection{*The Discriminator for Constructors*}
16.62
16.63 text{*A function to distinguish nonces, mpairs and encryptions*}
16.64 -fun
16.65 +primrec
16.66 freediscrim :: "freemsg \<Rightarrow> int"
16.67 where
16.68 "freediscrim (NONCE N) = 0"
17.1 --- a/src/HOL/Rat.thy Tue Nov 30 08:58:47 2010 -0800
17.2 +++ b/src/HOL/Rat.thy Tue Nov 30 18:40:23 2010 +0100
17.3 @@ -44,7 +44,7 @@
17.4 qed
17.5
17.6 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
17.7 - by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
17.8 + by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
17.9
17.10 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
17.11 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
17.12 @@ -146,7 +146,7 @@
17.13 lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
17.14 proof -
17.15 have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
17.16 - by (simp add: congruent_def)
17.17 + by (simp add: congruent_def split_paired_all)
17.18 then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
17.19 qed
17.20
17.21 @@ -781,7 +781,7 @@
17.22
17.23 lemma of_rat_congruent:
17.24 "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
17.25 -apply (rule congruent.intro)
17.26 +apply (rule congruentI)
17.27 apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
17.28 apply (simp only: of_int_mult [symmetric])
17.29 done
18.1 --- a/src/HOL/RealDef.thy Tue Nov 30 08:58:47 2010 -0800
18.2 +++ b/src/HOL/RealDef.thy Tue Nov 30 18:40:23 2010 +0100
18.3 @@ -324,7 +324,7 @@
18.4
18.5 lemma equiv_realrel: "equiv {X. cauchy X} realrel"
18.6 using refl_realrel sym_realrel trans_realrel
18.7 - by (rule equiv.intro)
18.8 + by (rule equivI)
18.9
18.10 subsection {* The field of real numbers *}
18.11
18.12 @@ -358,7 +358,7 @@
18.13 apply (simp add: quotientI X)
18.14 apply (rule the_equality)
18.15 apply clarsimp
18.16 - apply (erule congruent.congruent [OF f])
18.17 + apply (erule congruentD [OF f])
18.18 apply (erule bspec)
18.19 apply simp
18.20 apply (rule refl_onD [OF refl_realrel])
18.21 @@ -370,14 +370,14 @@
18.22 assumes X: "cauchy X" and Y: "cauchy Y"
18.23 shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
18.24 apply (subst real_case_1 [OF _ X])
18.25 - apply (rule congruent.intro)
18.26 + apply (rule congruentI)
18.27 apply (subst real_case_1 [OF _ Y])
18.28 apply (rule congruent2_implies_congruent [OF equiv_realrel f])
18.29 apply (simp add: realrel_def)
18.30 apply (subst real_case_1 [OF _ Y])
18.31 apply (rule congruent2_implies_congruent [OF equiv_realrel f])
18.32 apply (simp add: realrel_def)
18.33 - apply (erule congruent2.congruent2 [OF f])
18.34 + apply (erule congruent2D [OF f])
18.35 apply (rule refl_onD [OF refl_realrel])
18.36 apply (simp add: Y)
18.37 apply (rule real_case_1 [OF _ Y])
18.38 @@ -416,7 +416,7 @@
18.39
18.40 lemma minus_respects_realrel:
18.41 "(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
18.42 -proof (rule congruent.intro)
18.43 +proof (rule congruentI)
18.44 fix X Y assume "(X, Y) \<in> realrel"
18.45 hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
18.46 unfolding realrel_def by simp_all
18.47 @@ -492,7 +492,7 @@
18.48 lemma inverse_respects_realrel:
18.49 "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
18.50 (is "?inv respects realrel")
18.51 -proof (rule congruent.intro)
18.52 +proof (rule congruentI)
18.53 fix X Y assume "(X, Y) \<in> realrel"
18.54 hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
18.55 unfolding realrel_def by simp_all
18.56 @@ -622,7 +622,7 @@
18.57 assumes sym: "sym r"
18.58 assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
18.59 shows "P respects r"
18.60 -apply (rule congruent.intro)
18.61 +apply (rule congruentI)
18.62 apply (rule iffI)
18.63 apply (erule (1) P)
18.64 apply (erule (1) P [OF symD [OF sym]])
19.1 --- a/src/HOL/ZF/Games.thy Tue Nov 30 08:58:47 2010 -0800
19.2 +++ b/src/HOL/ZF/Games.thy Tue Nov 30 18:40:23 2010 +0100
19.3 @@ -893,9 +893,9 @@
19.4 have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel"
19.5 apply (simp add: congruent2_def)
19.6 apply (auto simp add: eq_game_rel_def eq_game_def)
19.7 - apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
19.8 + apply (rule_tac y="plus_game a ba" in ge_game_trans)
19.9 apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
19.10 - apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
19.11 + apply (rule_tac y="plus_game b aa" in ge_game_trans)
19.12 apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
19.13 done
19.14 then show ?thesis
20.1 --- a/src/HOL/ex/Dedekind_Real.thy Tue Nov 30 08:58:47 2010 -0800
20.2 +++ b/src/HOL/ex/Dedekind_Real.thy Tue Nov 30 18:40:23 2010 +0100
20.3 @@ -1288,7 +1288,7 @@
20.4 proof -
20.5 have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
20.6 respects2 realrel"
20.7 - by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma)
20.8 + by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma)
20.9 thus ?thesis
20.10 by (simp add: real_add_def UN_UN_split_split_eq
20.11 UN_equiv_class2 [OF equiv_realrel equiv_realrel])
20.12 @@ -1297,7 +1297,7 @@
20.13 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
20.14 proof -
20.15 have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
20.16 - by (simp add: congruent_def add_commute)
20.17 + by (auto simp add: congruent_def add_commute)
20.18 thus ?thesis
20.19 by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
20.20 qed