author boehmes Tue Nov 30 21:54:15 2010 +0100 (2010-11-30) changeset 40829 edd1e0764da1 parent 40828 47ff261431c4 parent 40827 abbc05c20e24 child 40835 fc750e794458
merged
```     1.1 --- a/NEWS	Tue Nov 30 18:22:43 2010 +0100
1.2 +++ b/NEWS	Tue Nov 30 21:54:15 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 18:22:43 2010 +0100
2.2 +++ b/src/HOL/Algebra/Coset.thy	Tue Nov 30 21:54:15 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 18:22:43 2010 +0100
3.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Nov 30 21:54:15 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 +definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
3.11 +  "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
3.12
3.13 -locale equiv =
3.14 -  fixes A and r
3.15 -  assumes refl_on: "refl_on A r"
3.16 -    and sym: "sym r"
3.17 -    and trans: "trans r"
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/HOLCF/Library/List_Cpo.thy	Tue Nov 30 18:22:43 2010 +0100
4.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 21:54:15 2010 +0100
4.3 @@ -237,6 +237,54 @@
4.4  deserve to have continuity lemmas.  I'll add more as they are
4.5  needed. *}
4.6
4.7 +subsection {* Lists are a discrete cpo *}
4.8 +
4.9 +instance list :: (discrete_cpo) discrete_cpo
4.10 +proof
4.11 +  fix xs ys :: "'a list"
4.12 +  show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys"
4.13 +    by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
4.14 +qed
4.15 +
4.16 +subsection {* Compactness and chain-finiteness *}
4.17 +
4.18 +lemma compact_Nil [simp]: "compact []"
4.19 +apply (rule compactI2)
4.20 +apply (erule list_chain_cases)
4.21 +apply simp
4.23 +done
4.24 +
4.25 +lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)"
4.26 +apply (rule compactI2)
4.27 +apply (erule list_chain_cases)
4.28 +apply (auto simp add: lub_Cons dest!: compactD2)
4.29 +apply (rename_tac i j, rule_tac x="max i j" in exI)
4.30 +apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
4.31 +apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
4.32 +apply (erule (1) conjI)
4.33 +done
4.34 +
4.35 +lemma compact_Cons_iff [simp]:
4.36 +  "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs"
4.37 +apply (safe intro!: compact_Cons)
4.38 +apply (simp only: compact_def)
4.39 +apply (subgoal_tac "cont (\<lambda>x. x # xs)")
4.40 +apply (drule (1) adm_subst, simp, simp)
4.41 +apply (simp only: compact_def)
4.42 +apply (subgoal_tac "cont (\<lambda>xs. x # xs)")
4.43 +apply (drule (1) adm_subst, simp, simp)
4.44 +done
4.45 +
4.46 +instance list :: (chfin) chfin
4.47 +proof
4.48 +  fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y"
4.49 +  moreover have "\<And>(xs::'a list). compact xs"
4.50 +    by (induct_tac xs, simp_all)
4.51 +  ultimately show "\<exists>i. max_in_chain i Y"
4.52 +    by (rule compact_imp_max_in_chain)
4.53 +qed
4.54 +
4.55  subsection {* Using lists with fixrec *}
4.56
4.57  definition
```
```     5.1 --- a/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 18:22:43 2010 +0100
5.2 +++ b/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 21:54:15 2010 +0100
5.3 @@ -176,7 +176,7 @@
5.4                Abs_Msg (msgrel``{MPAIR U V})"
5.5  proof -
5.6    have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
5.7 -    by (simp add: congruent2_def msgrel.MPAIR)
5.8 +    by (auto simp add: congruent2_def msgrel.MPAIR)
5.9    thus ?thesis
5.10      by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
5.11  qed
5.12 @@ -184,7 +184,7 @@
5.13  lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
5.14  proof -
5.15    have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
5.16 -    by (simp add: congruent_def msgrel.CRYPT)
5.17 +    by (auto simp add: congruent_def msgrel.CRYPT)
5.18    thus ?thesis
5.19      by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
5.20  qed
5.21 @@ -193,7 +193,7 @@
5.22       "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
5.23  proof -
5.24    have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
5.25 -    by (simp add: congruent_def msgrel.DECRYPT)
5.26 +    by (auto simp add: congruent_def msgrel.DECRYPT)
5.27    thus ?thesis
5.28      by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
5.29  qed
5.30 @@ -221,7 +221,7 @@
5.31     "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
5.32
5.33  lemma nonces_congruent: "freenonces respects msgrel"
5.34 -by (simp add: congruent_def msgrel_imp_eq_freenonces)
5.35 +by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
5.36
5.37
5.38  text{*Now prove the four equations for @{term nonces}*}
5.39 @@ -256,7 +256,7 @@
5.40     "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
5.41
5.42  lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
5.43 -by (simp add: congruent_def msgrel_imp_eqv_freeleft)
5.44 +by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
5.45
5.46  text{*Now prove the four equations for @{term left}*}
5.47
5.48 @@ -290,7 +290,7 @@
5.49     "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
5.50
5.51  lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
5.52 -by (simp add: congruent_def msgrel_imp_eqv_freeright)
5.53 +by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
5.54
5.55  text{*Now prove the four equations for @{term right}*}
5.56
5.57 @@ -425,7 +425,7 @@
5.58     "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
5.59
5.60  lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
5.61 -by (simp add: congruent_def msgrel_imp_eq_freediscrim)
5.62 +by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
5.63
5.64  text{*Now prove the four equations for @{term discrim}*}
5.65
```
```     6.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 18:22:43 2010 +0100
6.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 21:54:15 2010 +0100
6.3 @@ -125,14 +125,19 @@
6.4  | "freeargs (FNCALL F Xs) = Xs"
6.5
6.6  theorem exprel_imp_eqv_freeargs:
6.7 -     "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
6.8 -apply (induct set: exprel)
6.9 -apply (erule_tac [4] listrel.induct)
6.11 -apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
6.12 -apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
6.13 -done
6.14 -
6.15 +  assumes "U \<sim> V"
6.16 +  shows "(freeargs U, freeargs V) \<in> listrel exprel"
6.17 +proof -
6.18 +  from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
6.19 +  from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
6.20 +  from assms show ?thesis
6.21 +    apply induct
6.22 +    apply (erule_tac [4] listrel.induct)
6.23 +    apply (simp_all add: listrel.intros)
6.24 +    apply (blast intro: symD [OF sym])
6.25 +    apply (blast intro: transD [OF trans])
6.26 +    done
6.27 +qed
6.28
6.29
6.30  subsection{*The Initial Algebra: A Quotiented Message Type*}
6.31 @@ -220,7 +225,7 @@
6.32               Abs_Exp (exprel``{PLUS U V})"
6.33  proof -
6.34    have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
6.35 -    by (simp add: congruent2_def exprel.PLUS)
6.36 +    by (auto simp add: congruent2_def exprel.PLUS)
6.37    thus ?thesis
6.38      by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
6.39  qed
6.40 @@ -236,13 +241,13 @@
6.41
6.42  lemma FnCall_respects:
6.43       "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
6.44 -  by (simp add: congruent_def exprel.FNCALL)
6.45 +  by (auto simp add: congruent_def exprel.FNCALL)
6.46
6.47  lemma FnCall_sing:
6.48       "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
6.49  proof -
6.50    have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
6.51 -    by (simp add: congruent_def FNCALL_Cons listrel.intros)
6.52 +    by (auto simp add: congruent_def FNCALL_Cons listrel.intros)
6.53    thus ?thesis
6.54      by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
6.55  qed
6.56 @@ -255,7 +260,7 @@
6.57       "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
6.58  proof -
6.59    have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
6.60 -    by (simp add: congruent_def exprel.FNCALL)
6.61 +    by (auto simp add: congruent_def exprel.FNCALL)
6.62    thus ?thesis
6.63      by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
6.64                    listset_Rep_Exp_Abs_Exp)
6.65 @@ -275,7 +280,7 @@
6.66    "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
6.67
6.68  lemma vars_respects: "freevars respects exprel"
6.69 -by (simp add: congruent_def exprel_imp_eq_freevars)
6.70 +by (auto simp add: congruent_def exprel_imp_eq_freevars)
6.71
6.72  text{*The extension of the function @{term vars} to lists*}
6.73  primrec vars_list :: "exp list \<Rightarrow> nat set" where
6.74 @@ -340,7 +345,7 @@
6.75    "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
6.76
6.77  lemma fun_respects: "(%U. {freefun U}) respects exprel"
6.78 -by (simp add: congruent_def exprel_imp_eq_freefun)
6.79 +by (auto simp add: congruent_def exprel_imp_eq_freefun)
6.80
6.81  lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
6.82  apply (cases Xs rule: eq_Abs_ExpList)
6.83 @@ -358,7 +363,7 @@
6.84    by (induct set: listrel) simp_all
6.85
6.86  lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
6.87 -by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
6.88 +by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
6.89
6.90  lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
6.91  apply (cases Xs rule: eq_Abs_ExpList)
6.92 @@ -387,7 +392,7 @@
6.93    "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
6.94
6.95  lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
6.96 -by (simp add: congruent_def exprel_imp_eq_freediscrim)
6.97 +by (auto simp add: congruent_def exprel_imp_eq_freediscrim)
6.98
6.99  text{*Now prove the four equations for @{term discrim}*}
6.100
```
```     7.1 --- a/src/HOL/Int.thy	Tue Nov 30 18:22:43 2010 +0100
7.2 +++ b/src/HOL/Int.thy	Tue Nov 30 21:54:15 2010 +0100
7.3 @@ -102,7 +102,7 @@
7.4  lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
7.5  proof -
7.6    have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
7.7 -    by (simp add: congruent_def)
7.8 +    by (auto simp add: congruent_def)
7.9    thus ?thesis
7.10      by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
7.11  qed
7.12 @@ -113,7 +113,7 @@
7.13  proof -
7.14    have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
7.15          respects2 intrel"
7.16 -    by (simp add: congruent2_def)
7.17 +    by (auto simp add: congruent2_def)
7.18    thus ?thesis
7.20                    UN_equiv_class2 [OF equiv_intrel equiv_intrel])
7.21 @@ -288,7 +288,7 @@
7.22  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
7.23  proof -
7.24    have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
7.28    thus ?thesis
7.29      by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
7.30 @@ -394,7 +394,7 @@
7.31  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
7.32  proof -
7.33    have "(\<lambda>(x,y). {x-y}) respects intrel"
7.34 -    by (simp add: congruent_def) arith
7.35 +    by (auto simp add: congruent_def)
7.36    thus ?thesis
7.37      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
7.38  qed
```
```     8.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 18:22:43 2010 +0100
8.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 21:54:15 2010 +0100
8.3 @@ -43,7 +43,7 @@
8.4  qed
8.5
8.6  lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
8.7 -  by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
8.8 +  by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
8.9
8.10  lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
8.11  lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
8.12 @@ -121,7 +121,7 @@
8.13  lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
8.14  proof -
8.15    have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
8.16 -    by (simp add: congruent_def)
8.17 +    by (simp add: congruent_def split_paired_all)
8.18    then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
8.19  qed
8.20
```
```     9.1 --- a/src/HOL/Library/Quotient_List.thy	Tue Nov 30 18:22:43 2010 +0100
9.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Nov 30 21:54:15 2010 +0100
9.3 @@ -10,94 +10,96 @@
9.4
9.5  declare [[map list = (map, list_all2)]]
9.6
9.7 -lemma split_list_all:
9.8 -  shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
9.9 -  apply(auto)
9.10 -  apply(case_tac x)
9.11 -  apply(simp_all)
9.12 -  done
9.13 +lemma map_id [id_simps]:
9.14 +  "map id = id"
9.15 +  by (simp add: id_def fun_eq_iff map.identity)
9.16
9.17 -lemma map_id[id_simps]:
9.18 -  shows "map id = id"
9.20 -  apply(rule allI)
9.21 -  apply(induct_tac x)
9.22 -  apply(simp_all)
9.23 -  done
9.24 +lemma list_all2_map1:
9.25 +  "list_all2 R (map f xs) ys \<longleftrightarrow> list_all2 (\<lambda>x. R (f x)) xs ys"
9.26 +  by (induct xs ys rule: list_induct2') simp_all
9.27 +
9.28 +lemma list_all2_map2:
9.29 +  "list_all2 R xs (map f ys) \<longleftrightarrow> list_all2 (\<lambda>x y. R x (f y)) xs ys"
9.30 +  by (induct xs ys rule: list_induct2') simp_all
9.31
9.32 -lemma list_all2_reflp:
9.33 -  shows "equivp R \<Longrightarrow> list_all2 R xs xs"
9.34 -  by (induct xs, simp_all add: equivp_reflp)
9.35 +lemma list_all2_eq [id_simps]:
9.36 +  "list_all2 (op =) = (op =)"
9.37 +proof (rule ext)+
9.38 +  fix xs ys
9.39 +  show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys"
9.40 +    by (induct xs ys rule: list_induct2') simp_all
9.41 +qed
9.42
9.43 -lemma list_all2_symp:
9.44 -  assumes a: "equivp R"
9.45 -  and b: "list_all2 R xs ys"
9.46 -  shows "list_all2 R ys xs"
9.47 -  using list_all2_lengthD[OF b] b
9.48 -  apply(induct xs ys rule: list_induct2)
9.49 -  apply(simp_all)
9.50 -  apply(rule equivp_symp[OF a])
9.51 -  apply(simp)
9.52 -  done
9.53 +lemma list_reflp:
9.54 +  assumes "reflp R"
9.55 +  shows "reflp (list_all2 R)"
9.56 +proof (rule reflpI)
9.57 +  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
9.58 +  fix xs
9.59 +  show "list_all2 R xs xs"
9.60 +    by (induct xs) (simp_all add: *)
9.61 +qed
9.62
9.63 -lemma list_all2_transp:
9.64 -  assumes a: "equivp R"
9.65 -  and b: "list_all2 R xs1 xs2"
9.66 -  and c: "list_all2 R xs2 xs3"
9.67 -  shows "list_all2 R xs1 xs3"
9.68 -  using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
9.69 -  apply(induct rule: list_induct3)
9.70 -  apply(simp_all)
9.71 -  apply(auto intro: equivp_transp[OF a])
9.72 -  done
9.73 +lemma list_symp:
9.74 +  assumes "symp R"
9.75 +  shows "symp (list_all2 R)"
9.76 +proof (rule sympI)
9.77 +  from assms have *: "\<And>xs ys. R xs ys \<Longrightarrow> R ys xs" by (rule sympE)
9.78 +  fix xs ys
9.79 +  assume "list_all2 R xs ys"
9.80 +  then show "list_all2 R ys xs"
9.81 +    by (induct xs ys rule: list_induct2') (simp_all add: *)
9.82 +qed
9.83
9.84 -lemma list_equivp[quot_equiv]:
9.85 -  assumes a: "equivp R"
9.86 -  shows "equivp (list_all2 R)"
9.87 -  apply (intro equivpI)
9.88 -  unfolding reflp_def symp_def transp_def
9.89 -  apply(simp add: list_all2_reflp[OF a])
9.90 -  apply(blast intro: list_all2_symp[OF a])
9.91 -  apply(blast intro: list_all2_transp[OF a])
9.92 -  done
9.93 +lemma list_transp:
9.94 +  assumes "transp R"
9.95 +  shows "transp (list_all2 R)"
9.96 +proof (rule transpI)
9.97 +  from assms have *: "\<And>xs ys zs. R xs ys \<Longrightarrow> R ys zs \<Longrightarrow> R xs zs" by (rule transpE)
9.98 +  fix xs ys zs
9.99 +  assume A: "list_all2 R xs ys" "list_all2 R ys zs"
9.100 +  then have "length xs = length ys" "length ys = length zs" by (blast dest: list_all2_lengthD)+
9.101 +  then show "list_all2 R xs zs" using A
9.102 +    by (induct xs ys zs rule: list_induct3) (auto intro: *)
9.103 +qed
9.104
9.105 -lemma list_all2_rel:
9.106 -  assumes q: "Quotient R Abs Rep"
9.107 -  shows "list_all2 R r s = (list_all2 R r r \<and> list_all2 R s s \<and> (map Abs r = map Abs s))"
9.108 -  apply(induct r s rule: list_induct2')
9.109 -  apply(simp_all)
9.110 -  using Quotient_rel[OF q]
9.111 -  apply(metis)
9.112 -  done
9.113 +lemma list_equivp [quot_equiv]:
9.114 +  "equivp R \<Longrightarrow> equivp (list_all2 R)"
9.115 +  by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
9.116
9.117 -lemma list_quotient[quot_thm]:
9.118 -  assumes q: "Quotient R Abs Rep"
9.119 +lemma list_quotient [quot_thm]:
9.120 +  assumes "Quotient R Abs Rep"
9.121    shows "Quotient (list_all2 R) (map Abs) (map Rep)"
9.122 -  unfolding Quotient_def
9.123 -  apply(subst split_list_all)
9.124 -  apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
9.125 -  apply(intro conjI allI)
9.126 -  apply(induct_tac a)
9.127 -  apply(simp_all add: Quotient_rep_reflp[OF q])
9.128 -  apply(rule list_all2_rel[OF q])
9.129 -  done
9.130 +proof (rule QuotientI)
9.131 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
9.132 +  then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
9.133 +next
9.134 +  from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
9.135 +  then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
9.136 +    by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
9.137 +next
9.138 +  fix xs ys
9.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)
9.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"
9.141 +    by (induct xs ys rule: list_induct2') auto
9.142 +qed
9.143
9.144 -lemma cons_prs[quot_preserve]:
9.145 +lemma cons_prs [quot_preserve]:
9.146    assumes q: "Quotient R Abs Rep"
9.147    shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
9.148    by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
9.149
9.150 -lemma cons_rsp[quot_respect]:
9.151 +lemma cons_rsp [quot_respect]:
9.152    assumes q: "Quotient R Abs Rep"
9.153    shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
9.154    by auto
9.155
9.156 -lemma nil_prs[quot_preserve]:
9.157 +lemma nil_prs [quot_preserve]:
9.158    assumes q: "Quotient R Abs Rep"
9.159    shows "map Abs [] = []"
9.160    by simp
9.161
9.162 -lemma nil_rsp[quot_respect]:
9.163 +lemma nil_rsp [quot_respect]:
9.164    assumes q: "Quotient R Abs Rep"
9.165    shows "list_all2 R [] []"
9.166    by simp
9.167 @@ -109,7 +111,7 @@
9.168    by (induct l)
9.169       (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
9.170
9.171 -lemma map_prs[quot_preserve]:
9.172 +lemma map_prs [quot_preserve]:
9.173    assumes a: "Quotient R1 abs1 rep1"
9.174    and     b: "Quotient R2 abs2 rep2"
9.175    shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
9.176 @@ -117,8 +119,7 @@
9.177    by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
9.178      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
9.179
9.180 -
9.181 -lemma map_rsp[quot_respect]:
9.182 +lemma map_rsp [quot_respect]:
9.183    assumes q1: "Quotient R1 Abs1 Rep1"
9.184    and     q2: "Quotient R2 Abs2 Rep2"
9.185    shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
9.186 @@ -137,7 +138,7 @@
9.187    shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
9.188    by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
9.189
9.190 -lemma foldr_prs[quot_preserve]:
9.191 +lemma foldr_prs [quot_preserve]:
9.192    assumes a: "Quotient R1 abs1 rep1"
9.193    and     b: "Quotient R2 abs2 rep2"
9.194    shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
9.195 @@ -151,8 +152,7 @@
9.196    shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
9.197    by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
9.198
9.199 -
9.200 -lemma foldl_prs[quot_preserve]:
9.201 +lemma foldl_prs [quot_preserve]:
9.202    assumes a: "Quotient R1 abs1 rep1"
9.203    and     b: "Quotient R2 abs2 rep2"
9.204    shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
9.205 @@ -217,11 +217,11 @@
9.206      qed
9.207    qed
9.208
9.209 -lemma[quot_respect]:
9.210 +lemma [quot_respect]:
9.211    "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
9.212    by (simp add: list_all2_rsp fun_rel_def)
9.213
9.214 -lemma[quot_preserve]:
9.215 +lemma [quot_preserve]:
9.216    assumes a: "Quotient R abs1 rep1"
9.217    shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
9.219 @@ -230,19 +230,11 @@
9.220    apply (simp_all add: Quotient_abs_rep[OF a])
9.221    done
9.222
9.223 -lemma[quot_preserve]:
9.224 +lemma [quot_preserve]:
9.225    assumes a: "Quotient R abs1 rep1"
9.226    shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
9.227    by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
9.228
9.229 -lemma list_all2_eq[id_simps]:
9.230 -  shows "(list_all2 (op =)) = (op =)"
9.231 -  unfolding fun_eq_iff
9.232 -  apply(rule allI)+
9.233 -  apply(induct_tac x xa rule: list_induct2')
9.234 -  apply(simp_all)
9.235 -  done
9.236 -
9.237  lemma list_all2_find_element:
9.238    assumes a: "x \<in> set a"
9.239    and b: "list_all2 R a b"
```
```    10.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Nov 30 18:22:43 2010 +0100
10.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Nov 30 21:54:15 2010 +0100
10.3 @@ -18,64 +18,73 @@
10.4
10.5  declare [[map option = (Option.map, option_rel)]]
10.6
10.7 -text {* should probably be in Option.thy *}
10.8 -lemma split_option_all:
10.9 -  shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
10.10 -  apply(auto)
10.11 -  apply(case_tac x)
10.12 -  apply(simp_all)
10.13 +lemma option_rel_unfold:
10.14 +  "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
10.15 +    | (Some x, Some y) \<Rightarrow> R x y
10.16 +    | _ \<Rightarrow> False)"
10.17 +  by (cases x) (cases y, simp_all)+
10.18 +
10.19 +lemma option_rel_map1:
10.20 +  "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
10.21 +  by (simp add: option_rel_unfold split: option.split)
10.22 +
10.23 +lemma option_rel_map2:
10.24 +  "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
10.25 +  by (simp add: option_rel_unfold split: option.split)
10.26 +
10.27 +lemma option_map_id [id_simps]:
10.28 +  "Option.map id = id"
10.29 +  by (simp add: id_def Option.map.identity fun_eq_iff)
10.30 +
10.31 +lemma option_rel_eq [id_simps]:
10.32 +  "option_rel (op =) = (op =)"
10.33 +  by (simp add: option_rel_unfold fun_eq_iff split: option.split)
10.34 +
10.35 +lemma option_reflp:
10.36 +  "reflp R \<Longrightarrow> reflp (option_rel R)"
10.37 +  by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
10.38 +
10.39 +lemma option_symp:
10.40 +  "symp R \<Longrightarrow> symp (option_rel R)"
10.41 +  by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
10.42 +
10.43 +lemma option_transp:
10.44 +  "transp R \<Longrightarrow> transp (option_rel R)"
10.45 +  by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
10.46 +
10.47 +lemma option_equivp [quot_equiv]:
10.48 +  "equivp R \<Longrightarrow> equivp (option_rel R)"
10.49 +  by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
10.50 +
10.51 +lemma option_quotient [quot_thm]:
10.52 +  assumes "Quotient R Abs Rep"
10.53 +  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
10.54 +  apply (rule QuotientI)
10.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])
10.56 +  using Quotient_rel [OF assms]
10.57 +  apply (simp add: option_rel_unfold split: option.split)
10.58    done
10.59
10.60 -lemma option_quotient[quot_thm]:
10.61 -  assumes q: "Quotient R Abs Rep"
10.62 -  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
10.63 -  unfolding Quotient_def
10.65 -  apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
10.66 -  using q
10.67 -  unfolding Quotient_def
10.68 -  apply(blast)
10.69 -  done
10.70 -
10.71 -lemma option_equivp[quot_equiv]:
10.72 -  assumes a: "equivp R"
10.73 -  shows "equivp (option_rel R)"
10.74 -  apply(rule equivpI)
10.75 -  unfolding reflp_def symp_def transp_def
10.77 -  apply(blast intro: equivp_reflp[OF a])
10.78 -  apply(blast intro: equivp_symp[OF a])
10.79 -  apply(blast intro: equivp_transp[OF a])
10.80 -  done
10.81 -
10.82 -lemma option_None_rsp[quot_respect]:
10.83 +lemma option_None_rsp [quot_respect]:
10.84    assumes q: "Quotient R Abs Rep"
10.85    shows "option_rel R None None"
10.86    by simp
10.87
10.88 -lemma option_Some_rsp[quot_respect]:
10.89 +lemma option_Some_rsp [quot_respect]:
10.90    assumes q: "Quotient R Abs Rep"
10.91    shows "(R ===> option_rel R) Some Some"
10.92    by auto
10.93
10.94 -lemma option_None_prs[quot_preserve]:
10.95 +lemma option_None_prs [quot_preserve]:
10.96    assumes q: "Quotient R Abs Rep"
10.97    shows "Option.map Abs None = None"
10.98    by simp
10.99
10.100 -lemma option_Some_prs[quot_preserve]:
10.101 +lemma option_Some_prs [quot_preserve]:
10.102    assumes q: "Quotient R Abs Rep"
10.103    shows "(Rep ---> Option.map Abs) Some = Some"
10.106    done
10.107
10.108 -lemma option_map_id[id_simps]:
10.109 -  shows "Option.map id = id"
10.110 -  by (simp add: fun_eq_iff split_option_all)
10.111 -
10.112 -lemma option_rel_eq[id_simps]:
10.113 -  shows "option_rel (op =) = (op =)"
10.114 -  by (simp add: fun_eq_iff split_option_all)
10.115 -
10.116  end
```
```    11.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 18:22:43 2010 +0100
11.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 21:54:15 2010 +0100
11.3 @@ -19,38 +19,39 @@
11.4    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
11.6
11.7 -lemma prod_equivp[quot_equiv]:
11.8 -  assumes a: "equivp R1"
11.9 -  assumes b: "equivp R2"
11.10 +lemma map_pair_id [id_simps]:
11.11 +  shows "map_pair id id = id"
11.12 +  by (simp add: fun_eq_iff)
11.13 +
11.14 +lemma prod_rel_eq [id_simps]:
11.15 +  shows "prod_rel (op =) (op =) = (op =)"
11.16 +  by (simp add: fun_eq_iff)
11.17 +
11.18 +lemma prod_equivp [quot_equiv]:
11.19 +  assumes "equivp R1"
11.20 +  assumes "equivp R2"
11.21    shows "equivp (prod_rel R1 R2)"
11.22 -  apply(rule equivpI)
11.23 -  unfolding reflp_def symp_def transp_def
11.24 -  apply(simp_all add: split_paired_all prod_rel_def)
11.25 -  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
11.26 -  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
11.27 -  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
11.28 +  using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
11.29 +
11.30 +lemma prod_quotient [quot_thm]:
11.31 +  assumes "Quotient R1 Abs1 Rep1"
11.32 +  assumes "Quotient R2 Abs2 Rep2"
11.33 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
11.34 +  apply (rule QuotientI)
11.35 +  apply (simp add: map_pair.compositionality map_pair.identity
11.36 +     Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
11.37 +  apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
11.38 +  using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
11.39 +  apply (auto simp add: split_paired_all)
11.40    done
11.41
11.42 -lemma prod_quotient[quot_thm]:
11.43 -  assumes q1: "Quotient R1 Abs1 Rep1"
11.44 -  assumes q2: "Quotient R2 Abs2 Rep2"
11.45 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
11.46 -  unfolding Quotient_def
11.48 -  apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
11.49 -  apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
11.50 -  using q1 q2
11.51 -  unfolding Quotient_def
11.52 -  apply(blast)
11.53 -  done
11.54 -
11.55 -lemma Pair_rsp[quot_respect]:
11.56 +lemma Pair_rsp [quot_respect]:
11.57    assumes q1: "Quotient R1 Abs1 Rep1"
11.58    assumes q2: "Quotient R2 Abs2 Rep2"
11.59    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
11.60    by (auto simp add: prod_rel_def)
11.61
11.62 -lemma Pair_prs[quot_preserve]:
11.63 +lemma Pair_prs [quot_preserve]:
11.64    assumes q1: "Quotient R1 Abs1 Rep1"
11.65    assumes q2: "Quotient R2 Abs2 Rep2"
11.66    shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
11.67 @@ -58,35 +59,35 @@
11.68    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
11.69    done
11.70
11.71 -lemma fst_rsp[quot_respect]:
11.72 +lemma fst_rsp [quot_respect]:
11.73    assumes "Quotient R1 Abs1 Rep1"
11.74    assumes "Quotient R2 Abs2 Rep2"
11.75    shows "(prod_rel R1 R2 ===> R1) fst fst"
11.76    by auto
11.77
11.78 -lemma fst_prs[quot_preserve]:
11.79 +lemma fst_prs [quot_preserve]:
11.80    assumes q1: "Quotient R1 Abs1 Rep1"
11.81    assumes q2: "Quotient R2 Abs2 Rep2"
11.82    shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
11.83    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
11.84
11.85 -lemma snd_rsp[quot_respect]:
11.86 +lemma snd_rsp [quot_respect]:
11.87    assumes "Quotient R1 Abs1 Rep1"
11.88    assumes "Quotient R2 Abs2 Rep2"
11.89    shows "(prod_rel R1 R2 ===> R2) snd snd"
11.90    by auto
11.91
11.92 -lemma snd_prs[quot_preserve]:
11.93 +lemma snd_prs [quot_preserve]:
11.94    assumes q1: "Quotient R1 Abs1 Rep1"
11.95    assumes q2: "Quotient R2 Abs2 Rep2"
11.96    shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
11.97    by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
11.98
11.99 -lemma split_rsp[quot_respect]:
11.100 +lemma split_rsp [quot_respect]:
11.101    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
11.102    by (auto intro!: fun_relI elim!: fun_relE)
11.103
11.104 -lemma split_prs[quot_preserve]:
11.105 +lemma split_prs [quot_preserve]:
11.106    assumes q1: "Quotient R1 Abs1 Rep1"
11.107    and     q2: "Quotient R2 Abs2 Rep2"
11.108    shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
11.109 @@ -111,12 +112,4 @@
11.110
11.111  declare Pair_eq[quot_preserve]
11.112
11.113 -lemma map_pair_id[id_simps]:
11.114 -  shows "map_pair id id = id"
11.115 -  by (simp add: fun_eq_iff)
11.116 -
11.117 -lemma prod_rel_eq[id_simps]:
11.118 -  shows "prod_rel (op =) (op =) = (op =)"
11.119 -  by (simp add: fun_eq_iff)
11.120 -
11.121  end
```
```    12.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 18:22:43 2010 +0100
12.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 21:54:15 2010 +0100
12.3 @@ -18,53 +18,68 @@
12.4
12.5  declare [[map sum = (sum_map, sum_rel)]]
12.6
12.7 +lemma sum_rel_unfold:
12.8 +  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
12.9 +    | (Inr x, Inr y) \<Rightarrow> R2 x y
12.10 +    | _ \<Rightarrow> False)"
12.11 +  by (cases x) (cases y, simp_all)+
12.12
12.13 -text {* should probably be in @{theory Sum_Type} *}
12.14 -lemma split_sum_all:
12.15 -  shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
12.16 -  apply(auto)
12.17 -  apply(case_tac x)
12.18 -  apply(simp_all)
12.19 -  done
12.20 +lemma sum_rel_map1:
12.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"
12.22 +  by (simp add: sum_rel_unfold split: sum.split)
12.23 +
12.24 +lemma sum_rel_map2:
12.25 +  "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"
12.26 +  by (simp add: sum_rel_unfold split: sum.split)
12.27 +
12.28 +lemma sum_map_id [id_simps]:
12.29 +  "sum_map id id = id"
12.30 +  by (simp add: id_def sum_map.identity fun_eq_iff)
12.31
12.32 -lemma sum_equivp[quot_equiv]:
12.33 -  assumes a: "equivp R1"
12.34 -  assumes b: "equivp R2"
12.35 -  shows "equivp (sum_rel R1 R2)"
12.36 -  apply(rule equivpI)
12.37 -  unfolding reflp_def symp_def transp_def
12.39 -  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
12.40 -  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
12.41 -  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
12.42 -  done
12.43 +lemma sum_rel_eq [id_simps]:
12.44 +  "sum_rel (op =) (op =) = (op =)"
12.45 +  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
12.46 +
12.47 +lemma sum_reflp:
12.48 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
12.49 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
12.50
12.51 -lemma sum_quotient[quot_thm]:
12.52 +lemma sum_symp:
12.53 +  "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
12.54 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
12.55 +
12.56 +lemma sum_transp:
12.57 +  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
12.58 +  by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
12.59 +
12.60 +lemma sum_equivp [quot_equiv]:
12.61 +  "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
12.62 +  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
12.63 +
12.64 +lemma sum_quotient [quot_thm]:
12.65    assumes q1: "Quotient R1 Abs1 Rep1"
12.66    assumes q2: "Quotient R2 Abs2 Rep2"
12.67    shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
12.68 -  unfolding Quotient_def
12.70 -  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
12.71 -  apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
12.72 -  using q1 q2
12.73 -  unfolding Quotient_def
12.74 -  apply(blast)+
12.75 +  apply (rule QuotientI)
12.76 +  apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
12.77 +    Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
12.78 +  using Quotient_rel [OF q1] Quotient_rel [OF q2]
12.79 +  apply (simp add: sum_rel_unfold split: sum.split)
12.80    done
12.81
12.82 -lemma sum_Inl_rsp[quot_respect]:
12.83 +lemma sum_Inl_rsp [quot_respect]:
12.84    assumes q1: "Quotient R1 Abs1 Rep1"
12.85    assumes q2: "Quotient R2 Abs2 Rep2"
12.86    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
12.87    by auto
12.88
12.89 -lemma sum_Inr_rsp[quot_respect]:
12.90 +lemma sum_Inr_rsp [quot_respect]:
12.91    assumes q1: "Quotient R1 Abs1 Rep1"
12.92    assumes q2: "Quotient R2 Abs2 Rep2"
12.93    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
12.94    by auto
12.95
12.96 -lemma sum_Inl_prs[quot_preserve]:
12.97 +lemma sum_Inl_prs [quot_preserve]:
12.98    assumes q1: "Quotient R1 Abs1 Rep1"
12.99    assumes q2: "Quotient R2 Abs2 Rep2"
12.100    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
12.101 @@ -72,7 +87,7 @@
12.103    done
12.104
12.105 -lemma sum_Inr_prs[quot_preserve]:
12.106 +lemma sum_Inr_prs [quot_preserve]:
12.107    assumes q1: "Quotient R1 Abs1 Rep1"
12.108    assumes q2: "Quotient R2 Abs2 Rep2"
12.109    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
12.110 @@ -80,12 +95,4 @@
12.112    done
12.113
12.114 -lemma sum_map_id[id_simps]:
12.115 -  shows "sum_map id id = id"
12.116 -  by (simp add: fun_eq_iff split_sum_all)
12.117 -
12.118 -lemma sum_rel_eq[id_simps]:
12.119 -  shows "sum_rel (op =) (op =) = (op =)"
12.120 -  by (simp add: fun_eq_iff split_sum_all)
12.121 -
12.122  end
```
```    13.1 --- a/src/HOL/NSA/StarDef.thy	Tue Nov 30 18:22:43 2010 +0100
13.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Nov 30 21:54:15 2010 +0100
13.3 @@ -62,7 +62,7 @@
13.5
13.6  lemma equiv_starrel: "equiv UNIV starrel"
13.7 -proof (rule equiv.intro)
13.8 +proof (rule equivI)
13.9    show "refl starrel" by (simp add: refl_on_def)
13.10    show "sym starrel" by (simp add: sym_def eq_commute)
13.11    show "trans starrel" by (auto intro: transI elim!: ultra)
```
```    14.1 --- a/src/HOL/Predicate.thy	Tue Nov 30 18:22:43 2010 +0100
14.2 +++ b/src/HOL/Predicate.thy	Tue Nov 30 21:54:15 2010 +0100
14.3 @@ -363,6 +363,44 @@
14.4  abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
14.5    "single_valuedP r == single_valued {(x, y). r x y}"
14.6
14.7 +(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
14.8 +
14.9 +definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14.10 +  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
14.11 +
14.12 +definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14.13 +  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
14.14 +
14.15 +definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
14.16 +  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
14.17 +
14.18 +lemma reflpI:
14.19 +  "(\<And>x. r x x) \<Longrightarrow> reflp r"
14.20 +  by (auto intro: refl_onI simp add: reflp_def)
14.21 +
14.22 +lemma reflpE:
14.23 +  assumes "reflp r"
14.24 +  obtains "r x x"
14.25 +  using assms by (auto dest: refl_onD simp add: reflp_def)
14.26 +
14.27 +lemma sympI:
14.28 +  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
14.29 +  by (auto intro: symI simp add: symp_def)
14.30 +
14.31 +lemma sympE:
14.32 +  assumes "symp r" and "r x y"
14.33 +  obtains "r y x"
14.34 +  using assms by (auto dest: symD simp add: symp_def)
14.35 +
14.36 +lemma transpI:
14.37 +  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
14.38 +  by (auto intro: transI simp add: transp_def)
14.39 +
14.40 +lemma transpE:
14.41 +  assumes "transp r" and "r x y" and "r y z"
14.42 +  obtains "r x z"
14.43 +  using assms by (auto dest: transD simp add: transp_def)
14.44 +
14.45
14.46  subsection {* Predicates as enumerations *}
14.47
```
```    15.1 --- a/src/HOL/Quotient.thy	Tue Nov 30 18:22:43 2010 +0100
15.2 +++ b/src/HOL/Quotient.thy	Tue Nov 30 21:54:15 2010 +0100
15.3 @@ -14,131 +14,15 @@
15.4    ("Tools/Quotient/quotient_tacs.ML")
15.5  begin
15.6
15.7 -
15.8  text {*
15.9    Basic definition for equivalence relations
15.10    that are represented by predicates.
15.11  *}
15.12
15.13 -definition
15.14 -  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
15.15 -
15.16 -lemma refl_reflp:
15.17 -  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
15.18 -  by (simp add: refl_on_def reflp_def)
15.19 -
15.20 -definition
15.21 -  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
15.22 -
15.23 -lemma sym_symp:
15.24 -  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
15.25 -  by (simp add: sym_def symp_def)
15.26 -
15.27 -definition
15.28 -  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
15.29 -
15.30 -lemma trans_transp:
15.31 -  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
15.32 -  by (auto simp add: trans_def transp_def)
15.33 -
15.34 -definition
15.35 -  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
15.36 -
15.37 -lemma equivp_reflp_symp_transp:
15.38 -  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
15.39 -  unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
15.40 -  by blast
15.41 -
15.42 -lemma equiv_equivp:
15.43 -  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
15.44 -  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
15.45 -
15.46 -lemma equivp_reflp:
15.47 -  shows "equivp E \<Longrightarrow> E x x"
15.48 -  by (simp only: equivp_reflp_symp_transp reflp_def)
15.49 -
15.50 -lemma equivp_symp:
15.51 -  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
15.52 -  by (simp add: equivp_def)
15.53 -
15.54 -lemma equivp_transp:
15.55 -  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
15.56 -  by (simp add: equivp_def)
15.57 -
15.58 -lemma equivpI:
15.59 -  assumes "reflp R" "symp R" "transp R"
15.60 -  shows "equivp R"
15.61 -  using assms by (simp add: equivp_reflp_symp_transp)
15.62 -
15.63 -lemma identity_equivp:
15.64 -  shows "equivp (op =)"
15.65 -  unfolding equivp_def
15.66 -  by auto
15.67 -
15.68 -text {* Partial equivalences *}
15.69 -
15.70 -definition
15.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)))"
15.72 -
15.73 -lemma equivp_implies_part_equivp:
15.74 -  assumes a: "equivp E"
15.75 -  shows "part_equivp E"
15.76 -  using a
15.77 -  unfolding equivp_def part_equivp_def
15.78 -  by auto
15.79 -
15.80 -lemma part_equivp_symp:
15.81 -  assumes e: "part_equivp R"
15.82 -  and a: "R x y"
15.83 -  shows "R y x"
15.84 -  using e[simplified part_equivp_def] a
15.85 -  by (metis)
15.86 -
15.87 -lemma part_equivp_typedef:
15.88 -  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
15.89 -  unfolding part_equivp_def mem_def
15.90 -  apply clarify
15.91 -  apply (intro exI)
15.92 -  apply (rule conjI)
15.93 -  apply assumption
15.94 -  apply (rule refl)
15.95 -  done
15.96 -
15.97 -lemma part_equivp_refl_symp_transp:
15.98 -  shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
15.99 -proof
15.100 -  assume "part_equivp E"
15.101 -  then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
15.102 -  unfolding part_equivp_def symp_def transp_def
15.103 -  by metis
15.104 -next
15.105 -  assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
15.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)"
15.107 -    unfolding symp_def transp_def by (metis, metis)
15.108 -  have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
15.109 -  proof (intro allI iffI conjI)
15.110 -    fix x y
15.111 -    assume d: "E x y"
15.112 -    then show "E x x" using b c by metis
15.113 -    show "E y y" using b c d by metis
15.114 -    show "E x = E y" unfolding fun_eq_iff using b c d by metis
15.115 -  next
15.116 -    fix x y
15.117 -    assume "E x x \<and> E y y \<and> E x = E y"
15.118 -    then show "E x y" using b c by metis
15.119 -  qed
15.120 -  then show "part_equivp E" unfolding part_equivp_def using a by metis
15.121 -qed
15.122 -
15.123 -lemma part_equivpI:
15.124 -  assumes "\<exists>x. R x x" "symp R" "transp R"
15.125 -  shows "part_equivp R"
15.126 -  using assms by (simp add: part_equivp_refl_symp_transp)
15.127 -
15.128  text {* Composition of Relations *}
15.129
15.130  abbreviation
15.131 -  rel_conj (infixr "OOO" 75)
15.132 +  rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
15.133  where
15.134    "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
15.135
15.136 @@ -169,16 +53,16 @@
15.137  definition
15.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)
15.139  where
15.140 -  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
15.141 +  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
15.142
15.143  lemma fun_relI [intro]:
15.144 -  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
15.145 -  shows "(E1 ===> E2) f g"
15.146 +  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
15.147 +  shows "(R1 ===> R2) f g"
15.148    using assms by (simp add: fun_rel_def)
15.149
15.150  lemma fun_relE:
15.151 -  assumes "(E1 ===> E2) f g" and "E1 x y"
15.152 -  obtains "E2 (f x) (g y)"
15.153 +  assumes "(R1 ===> R2) f g" and "R1 x y"
15.154 +  obtains "R2 (f x) (g y)"
15.155    using assms by (simp add: fun_rel_def)
15.156
15.157  lemma fun_rel_eq:
15.158 @@ -189,34 +73,41 @@
15.159  subsection {* Quotient Predicate *}
15.160
15.161  definition
15.162 -  "Quotient E Abs Rep \<longleftrightarrow>
15.163 -     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
15.164 -     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
15.165 +  "Quotient R Abs Rep \<longleftrightarrow>
15.166 +     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
15.167 +     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
15.168 +
15.169 +lemma QuotientI:
15.170 +  assumes "\<And>a. Abs (Rep a) = a"
15.171 +    and "\<And>a. R (Rep a) (Rep a)"
15.172 +    and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
15.173 +  shows "Quotient R Abs Rep"
15.174 +  using assms unfolding Quotient_def by blast
15.175
15.176  lemma Quotient_abs_rep:
15.177 -  assumes a: "Quotient E Abs Rep"
15.178 +  assumes a: "Quotient R Abs Rep"
15.179    shows "Abs (Rep a) = a"
15.180    using a
15.181    unfolding Quotient_def
15.182    by simp
15.183
15.184  lemma Quotient_rep_reflp:
15.185 -  assumes a: "Quotient E Abs Rep"
15.186 -  shows "E (Rep a) (Rep a)"
15.187 +  assumes a: "Quotient R Abs Rep"
15.188 +  shows "R (Rep a) (Rep a)"
15.189    using a
15.190    unfolding Quotient_def
15.191    by blast
15.192
15.193  lemma Quotient_rel:
15.194 -  assumes a: "Quotient E Abs Rep"
15.195 -  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
15.196 +  assumes a: "Quotient R Abs Rep"
15.197 +  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
15.198    using a
15.199    unfolding Quotient_def
15.200    by blast
15.201
15.202  lemma Quotient_rel_rep:
15.203    assumes a: "Quotient R Abs Rep"
15.204 -  shows "R (Rep a) (Rep b) = (a = b)"
15.205 +  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
15.206    using a
15.207    unfolding Quotient_def
15.208    by metis
15.209 @@ -228,22 +119,20 @@
15.210    by blast
15.211
15.212  lemma Quotient_rel_abs:
15.213 -  assumes a: "Quotient E Abs Rep"
15.214 -  shows "E r s \<Longrightarrow> Abs r = Abs s"
15.215 +  assumes a: "Quotient R Abs Rep"
15.216 +  shows "R r s \<Longrightarrow> Abs r = Abs s"
15.217    using a unfolding Quotient_def
15.218    by blast
15.219
15.220  lemma Quotient_symp:
15.221 -  assumes a: "Quotient E Abs Rep"
15.222 -  shows "symp E"
15.223 -  using a unfolding Quotient_def symp_def
15.224 -  by metis
15.225 +  assumes a: "Quotient R Abs Rep"
15.226 +  shows "symp R"
15.227 +  using a unfolding Quotient_def using sympI by metis
15.228
15.229  lemma Quotient_transp:
15.230 -  assumes a: "Quotient E Abs Rep"
15.231 -  shows "transp E"
15.232 -  using a unfolding Quotient_def transp_def
15.233 -  by metis
15.234 +  assumes a: "Quotient R Abs Rep"
15.235 +  shows "transp R"
15.236 +  using a unfolding Quotient_def using transpI by metis
15.237
15.238  lemma identity_quotient:
15.239    shows "Quotient (op =) id id"
15.240 @@ -291,8 +180,7 @@
15.241    and     a: "R xa xb" "R ya yb"
15.242    shows "R xa ya = R xb yb"
15.243    using a Quotient_symp[OF q] Quotient_transp[OF q]
15.244 -  unfolding symp_def transp_def
15.245 -  by blast
15.246 +  by (blast elim: sympE transpE)
15.247
15.248  lemma lambda_prs:
15.249    assumes q1: "Quotient R1 Abs1 Rep1"
15.250 @@ -300,7 +188,7 @@
15.251    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
15.252    unfolding fun_eq_iff
15.253    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
15.255 +  by simp
15.256
15.257  lemma lambda_prs1:
15.258    assumes q1: "Quotient R1 Abs1 Rep1"
15.259 @@ -308,7 +196,7 @@
15.260    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
15.261    unfolding fun_eq_iff
15.262    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
15.264 +  by simp
15.265
15.266  lemma rep_abs_rsp:
15.267    assumes q: "Quotient R Abs Rep"
15.268 @@ -392,9 +280,7 @@
15.270    apply(rule impI)
15.271    using a equivp_reflp_symp_transp[of "R2"]
15.273 -  apply(simp)
15.274 -  apply(simp)
15.275 +  apply (auto elim: equivpE reflpE)
15.276    done
15.277
15.278  lemma bex_reg_eqv_range:
15.279 @@ -406,7 +292,7 @@
15.280    apply(simp add: Respects_def in_respects fun_rel_def)
15.281    apply(rule impI)
15.282    using a equivp_reflp_symp_transp[of "R2"]
15.284 +  apply (auto elim: equivpE reflpE)
15.285    done
15.286
15.287  (* Next four lemmas are unused *)
```
```    16.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 18:22:43 2010 +0100
16.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 21:54:15 2010 +0100
16.3 @@ -19,11 +19,21 @@
16.4  where
16.5    [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
16.6
16.7 +lemma list_eq_reflp:
16.8 +  "reflp list_eq"
16.9 +  by (auto intro: reflpI)
16.10 +
16.11 +lemma list_eq_symp:
16.12 +  "symp list_eq"
16.13 +  by (auto intro: sympI)
16.14 +
16.15 +lemma list_eq_transp:
16.16 +  "transp list_eq"
16.17 +  by (auto intro: transpI)
16.18 +
16.19  lemma list_eq_equivp:
16.20 -  shows "equivp list_eq"
16.21 -  unfolding equivp_reflp_symp_transp
16.22 -  unfolding reflp_def symp_def transp_def
16.23 -  by auto
16.24 +  "equivp list_eq"
16.25 +  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)
16.26
16.27  text {* The @{text fset} type *}
16.28
16.29 @@ -141,7 +151,7 @@
16.30        \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
16.31      then have s: "(list_all2 R OOO op \<approx>) s s" by simp
16.32      have d: "map Abs r \<approx> map Abs s"
16.33 -      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
16.34 +      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
16.35      have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
16.36        by (rule map_list_eq_cong[OF d])
16.37      have y: "list_all2 R (map Rep (map Abs s)) s"
16.38 @@ -267,8 +277,11 @@
16.39  proof (rule fun_relI, elim pred_compE)
16.40    fix a b ba bb
16.41    assume a: "list_all2 op \<approx> a ba"
16.42 +  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
16.43    assume b: "ba \<approx> bb"
16.44 +  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
16.45    assume c: "list_all2 op \<approx> bb b"
16.46 +  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
16.47    have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
16.48    proof
16.49      fix x
16.50 @@ -278,9 +291,6 @@
16.51        show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
16.52      next
16.53        assume e: "\<exists>xa\<in>set b. x \<in> set xa"
16.54 -      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
16.55 -      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
16.56 -      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
16.57        show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
16.58      qed
16.59    qed
16.60 @@ -288,7 +298,6 @@
16.61  qed
16.62
16.63
16.64 -
16.65  section {* Quotient definitions for fsets *}
16.66
16.67
16.68 @@ -474,7 +483,7 @@
16.69    assumes a: "reflp R"
16.70    and b: "list_all2 R l r"
16.71    shows "list_all2 R (z @ l) (z @ r)"
16.72 -  by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
16.73 +  using a b by (induct z) (auto elim: reflpE)
16.74
16.75  lemma append_rsp2_pre0:
16.76    assumes a:"list_all2 op \<approx> x x'"
16.77 @@ -489,23 +498,14 @@
16.78    apply (rule list_all2_refl'[OF list_eq_equivp])
16.79    apply (simp_all del: list_eq_def)
16.80    apply (rule list_all2_app_l)
16.81 -  apply (simp_all add: reflp_def)
16.82 +  apply (simp_all add: reflpI)
16.83    done
16.84
16.85  lemma append_rsp2_pre:
16.86 -  assumes a:"list_all2 op \<approx> x x'"
16.87 -  and     b: "list_all2 op \<approx> z z'"
16.88 +  assumes "list_all2 op \<approx> x x'"
16.89 +    and "list_all2 op \<approx> z z'"
16.90    shows "list_all2 op \<approx> (x @ z) (x' @ z')"
16.91 -  apply (rule list_all2_transp[OF fset_equivp])
16.92 -  apply (rule append_rsp2_pre0)
16.93 -  apply (rule a)
16.94 -  using b apply (induct z z' rule: list_induct2')
16.95 -  apply (simp_all only: append_Nil2)
16.96 -  apply (rule list_all2_refl'[OF list_eq_equivp])
16.97 -  apply simp_all
16.98 -  apply (rule append_rsp2_pre1)
16.99 -  apply simp
16.100 -  done
16.101 +  using assms by (rule list_all2_appendI)
16.102
16.103  lemma append_rsp2 [quot_respect]:
16.104    "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
```
```    17.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 18:22:43 2010 +0100
17.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 21:54:15 2010 +0100
17.3 @@ -36,16 +36,16 @@
17.4
17.5  theorem equiv_msgrel: "equivp msgrel"
17.6  proof (rule equivpI)
17.7 -  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
17.8 -  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
17.9 -  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
17.10 +  show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
17.11 +  show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
17.12 +  show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
17.13  qed
17.14
17.15  subsection{*Some Functions on the Free Algebra*}
17.16
17.17  subsubsection{*The Set of Nonces*}
17.18
17.19 -fun
17.20 +primrec
17.21    freenonces :: "freemsg \<Rightarrow> nat set"
17.22  where
17.23    "freenonces (NONCE N) = {N}"
17.24 @@ -62,7 +62,7 @@
17.25
17.26  text{*A function to return the left part of the top pair in a message.  It will
17.27  be lifted to the initial algrebra, to serve as an example of that process.*}
17.28 -fun
17.29 +primrec
17.30    freeleft :: "freemsg \<Rightarrow> freemsg"
17.31  where
17.32    "freeleft (NONCE N) = NONCE N"
17.33 @@ -75,7 +75,7 @@
17.34    (the abstract constructor) is injective*}
17.35  lemma msgrel_imp_eqv_freeleft_aux:
17.36    shows "freeleft U \<sim> freeleft U"
17.37 -  by (induct rule: freeleft.induct) (auto)
17.38 +  by (fact msgrel_refl)
17.39
17.40  theorem msgrel_imp_eqv_freeleft:
17.41    assumes a: "U \<sim> V"
17.42 @@ -86,7 +86,7 @@
17.43  subsubsection{*The Right Projection*}
17.44
17.45  text{*A function to return the right part of the top pair in a message.*}
17.46 -fun
17.47 +primrec
17.48    freeright :: "freemsg \<Rightarrow> freemsg"
17.49  where
17.50    "freeright (NONCE N) = NONCE N"
17.51 @@ -99,7 +99,7 @@
17.52    (the abstract constructor) is injective*}
17.53  lemma msgrel_imp_eqv_freeright_aux:
17.54    shows "freeright U \<sim> freeright U"
17.55 -  by (induct rule: freeright.induct) (auto)
17.56 +  by (fact msgrel_refl)
17.57
17.58  theorem msgrel_imp_eqv_freeright:
17.59    assumes a: "U \<sim> V"
17.60 @@ -110,7 +110,7 @@
17.61  subsubsection{*The Discriminator for Constructors*}
17.62
17.63  text{*A function to distinguish nonces, mpairs and encryptions*}
17.64 -fun
17.65 +primrec
17.66    freediscrim :: "freemsg \<Rightarrow> int"
17.67  where
17.68     "freediscrim (NONCE N) = 0"
```
```    18.1 --- a/src/HOL/Rat.thy	Tue Nov 30 18:22:43 2010 +0100
18.2 +++ b/src/HOL/Rat.thy	Tue Nov 30 21:54:15 2010 +0100
18.3 @@ -44,7 +44,7 @@
18.4  qed
18.5
18.6  lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
18.7 -  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
18.8 +  by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
18.9
18.10  lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
18.11  lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
18.12 @@ -146,7 +146,7 @@
18.13  lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
18.14  proof -
18.15    have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
18.16 -    by (simp add: congruent_def)
18.17 +    by (simp add: congruent_def split_paired_all)
18.18    then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
18.19  qed
18.20
18.21 @@ -781,7 +781,7 @@
18.22
18.23  lemma of_rat_congruent:
18.24    "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
18.25 -apply (rule congruent.intro)
18.26 +apply (rule congruentI)
18.27  apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
18.28  apply (simp only: of_int_mult [symmetric])
18.29  done
```
```    19.1 --- a/src/HOL/RealDef.thy	Tue Nov 30 18:22:43 2010 +0100
19.2 +++ b/src/HOL/RealDef.thy	Tue Nov 30 21:54:15 2010 +0100
19.3 @@ -14,8 +14,8 @@
19.4  text {*
19.5    This theory contains a formalization of the real numbers as
19.6    equivalence classes of Cauchy sequences of rationals.  See
19.7 -  \url{HOL/ex/Dedekind_Real.thy} for an alternative construction
19.8 -  using Dedekind cuts.
19.9 +  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
19.10 +  construction using Dedekind cuts.
19.11  *}
19.12
19.13  subsection {* Preliminary lemmas *}
19.14 @@ -324,7 +324,7 @@
19.15
19.16  lemma equiv_realrel: "equiv {X. cauchy X} realrel"
19.17    using refl_realrel sym_realrel trans_realrel
19.18 -  by (rule equiv.intro)
19.19 +  by (rule equivI)
19.20
19.21  subsection {* The field of real numbers *}
19.22
19.23 @@ -358,7 +358,7 @@
19.24    apply (simp add: quotientI X)
19.25    apply (rule the_equality)
19.26    apply clarsimp
19.27 -  apply (erule congruent.congruent [OF f])
19.28 +  apply (erule congruentD [OF f])
19.29    apply (erule bspec)
19.30    apply simp
19.31    apply (rule refl_onD [OF refl_realrel])
19.32 @@ -370,14 +370,14 @@
19.33    assumes X: "cauchy X" and Y: "cauchy Y"
19.34    shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
19.35   apply (subst real_case_1 [OF _ X])
19.36 -  apply (rule congruent.intro)
19.37 +  apply (rule congruentI)
19.38    apply (subst real_case_1 [OF _ Y])
19.39     apply (rule congruent2_implies_congruent [OF equiv_realrel f])
19.41    apply (subst real_case_1 [OF _ Y])
19.42     apply (rule congruent2_implies_congruent [OF equiv_realrel f])
19.44 -  apply (erule congruent2.congruent2 [OF f])
19.45 +  apply (erule congruent2D [OF f])
19.46    apply (rule refl_onD [OF refl_realrel])
19.48    apply (rule real_case_1 [OF _ Y])
19.49 @@ -416,7 +416,7 @@
19.50
19.51  lemma minus_respects_realrel:
19.52    "(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
19.53 -proof (rule congruent.intro)
19.54 +proof (rule congruentI)
19.55    fix X Y assume "(X, Y) \<in> realrel"
19.56    hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
19.57      unfolding realrel_def by simp_all
19.58 @@ -492,7 +492,7 @@
19.59  lemma inverse_respects_realrel:
19.60    "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
19.61      (is "?inv respects realrel")
19.62 -proof (rule congruent.intro)
19.63 +proof (rule congruentI)
19.64    fix X Y assume "(X, Y) \<in> realrel"
19.65    hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
19.66      unfolding realrel_def by simp_all
19.67 @@ -622,7 +622,7 @@
19.68    assumes sym: "sym r"
19.69    assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
19.70    shows "P respects r"
19.71 -apply (rule congruent.intro)
19.72 +apply (rule congruentI)
19.73  apply (rule iffI)
19.74  apply (erule (1) P)
19.75  apply (erule (1) P [OF symD [OF sym]])
```
```    20.1 --- a/src/HOL/SEQ.thy	Tue Nov 30 18:22:43 2010 +0100
20.2 +++ b/src/HOL/SEQ.thy	Tue Nov 30 21:54:15 2010 +0100
20.3 @@ -221,15 +221,7 @@
20.4  lemma LIMSEQ_unique:
20.5    fixes a b :: "'a::metric_space"
20.6    shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
20.7 -apply (rule ccontr)
20.8 -apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
20.9 -apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
20.10 -apply (clarify, rename_tac M N)
20.11 -apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
20.12 -apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
20.13 -apply (erule le_less_trans, rule add_strict_mono, simp, simp)
20.14 -apply (subst dist_commute, rule dist_triangle)
20.15 -done
20.16 +by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
20.17
20.18  lemma (in bounded_linear) LIMSEQ:
20.19    "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
```
```    21.1 --- a/src/HOL/Word/Word.thy	Tue Nov 30 18:22:43 2010 +0100
21.2 +++ b/src/HOL/Word/Word.thy	Tue Nov 30 21:54:15 2010 +0100
21.3 @@ -184,13 +184,13 @@
21.4    "word_pred a = word_of_int (Int.pred (uint a))"
21.5
21.6  definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
21.7 -  "a udvd b == EX n>=0. uint b = n * uint a"
21.8 +  "a udvd b = (EX n>=0. uint b = n * uint a)"
21.9
21.10  definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
21.11 -  "a <=s b == sint a <= sint b"
21.12 +  "a <=s b = (sint a <= sint b)"
21.13
21.14  definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
21.15 -  "(x <s y) == (x <=s y & x ~= y)"
21.16 +  "(x <s y) = (x <=s y & x ~= y)"
21.17
21.18
21.19
21.20 @@ -245,76 +245,76 @@
21.21    by (simp only: word_msb_def Min_def)
21.22
21.23  definition setBit :: "'a :: len0 word => nat => 'a word" where
21.24 -  "setBit w n == set_bit w n True"
21.25 +  "setBit w n = set_bit w n True"
21.26
21.27  definition clearBit :: "'a :: len0 word => nat => 'a word" where
21.28 -  "clearBit w n == set_bit w n False"
21.29 +  "clearBit w n = set_bit w n False"
21.30
21.31
21.32  subsection "Shift operations"
21.33
21.34  definition sshiftr1 :: "'a :: len word => 'a word" where
21.35 -  "sshiftr1 w == word_of_int (bin_rest (sint w))"
21.36 +  "sshiftr1 w = word_of_int (bin_rest (sint w))"
21.37
21.38  definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
21.39 -  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
21.40 +  "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
21.41
21.42  definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
21.43 -  "w >>> n == (sshiftr1 ^^ n) w"
21.44 +  "w >>> n = (sshiftr1 ^^ n) w"
21.45
21.46  definition mask :: "nat => 'a::len word" where
21.47 -  "mask n == (1 << n) - 1"
21.48 +  "mask n = (1 << n) - 1"
21.49
21.50  definition revcast :: "'a :: len0 word => 'b :: len0 word" where
21.51 -  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
21.52 +  "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
21.53
21.54  definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
21.55 -  "slice1 n w == of_bl (takefill False n (to_bl w))"
21.56 +  "slice1 n w = of_bl (takefill False n (to_bl w))"
21.57
21.58  definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
21.59 -  "slice n w == slice1 (size w - n) w"
21.60 +  "slice n w = slice1 (size w - n) w"
21.61
21.62
21.63  subsection "Rotation"
21.64
21.65  definition rotater1 :: "'a list => 'a list" where
21.66 -  "rotater1 ys ==
21.67 -    case ys of [] => [] | x # xs => last ys # butlast ys"
21.68 +  "rotater1 ys =
21.69 +    (case ys of [] => [] | x # xs => last ys # butlast ys)"
21.70
21.71  definition rotater :: "nat => 'a list => 'a list" where
21.72 -  "rotater n == rotater1 ^^ n"
21.73 +  "rotater n = rotater1 ^^ n"
21.74
21.75  definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
21.76 -  "word_rotr n w == of_bl (rotater n (to_bl w))"
21.77 +  "word_rotr n w = of_bl (rotater n (to_bl w))"
21.78
21.79  definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
21.80 -  "word_rotl n w == of_bl (rotate n (to_bl w))"
21.81 +  "word_rotl n w = of_bl (rotate n (to_bl w))"
21.82
21.83  definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
21.84 -  "word_roti i w == if i >= 0 then word_rotr (nat i) w
21.85 -                    else word_rotl (nat (- i)) w"
21.86 +  "word_roti i w = (if i >= 0 then word_rotr (nat i) w
21.87 +                    else word_rotl (nat (- i)) w)"
21.88
21.89
21.90  subsection "Split and cat operations"
21.91
21.92  definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
21.93 -  "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
21.94 +  "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
21.95
21.96  definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
21.97 -  "word_split a ==
21.98 -   case bin_split (len_of TYPE ('c)) (uint a) of
21.99 -     (u, v) => (word_of_int u, word_of_int v)"
21.100 +  "word_split a =
21.101 +   (case bin_split (len_of TYPE ('c)) (uint a) of
21.102 +     (u, v) => (word_of_int u, word_of_int v))"
21.103
21.104  definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
21.105 -  "word_rcat ws ==
21.106 +  "word_rcat ws =
21.107    word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
21.108
21.109  definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
21.110 -  "word_rsplit w ==
21.111 +  "word_rsplit w =
21.112    map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
21.113
21.114  definition max_word :: "'a::len word" -- "Largest representable machine integer." where
21.115 -  "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
21.116 +  "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
21.117
21.118  primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
21.119    "of_bool False = 0"
21.120 @@ -337,7 +337,7 @@
21.121  lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded
21.122    atLeast_def lessThan_def Collect_conj_eq [symmetric]]
21.123
21.124 -lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}"
21.125 +lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
21.126    unfolding atLeastLessThan_alt by auto
21.127
21.128  lemma
21.129 @@ -390,7 +390,7 @@
21.130    unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
21.131
21.132  lemma bintr_uint':
21.133 -  "n >= size w ==> bintrunc n (uint w) = uint w"
21.134 +  "n >= size w \<Longrightarrow> bintrunc n (uint w) = uint w"
21.135    apply (unfold word_size)
21.136    apply (subst word_ubin.norm_Rep [symmetric])
21.137    apply (simp only: bintrunc_bintrunc_min word_size)
21.138 @@ -398,7 +398,7 @@
21.139    done
21.140
21.141  lemma wi_bintr':
21.142 -  "wb = word_of_int bin ==> n >= size wb ==>
21.143 +  "wb = word_of_int bin \<Longrightarrow> n >= size wb \<Longrightarrow>
21.144      word_of_int (bintrunc n bin) = wb"
21.145    unfolding word_size
21.146    by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
21.147 @@ -446,8 +446,9 @@
21.148
21.149  lemmas td_sint = word_sint.td
21.150
21.151 -lemma word_number_of_alt: "number_of b == word_of_int (number_of b)"
21.152 -  unfolding word_number_of_def by (simp add: number_of_eq)
21.153 +lemma word_number_of_alt [code_unfold_post]:
21.154 +  "number_of b = word_of_int (number_of b)"
21.155 +  by (simp add: number_of_eq word_number_of_def)
21.156
21.157  lemma word_no_wi: "number_of = word_of_int"
21.158    by (auto simp: word_number_of_def intro: ext)
21.159 @@ -483,7 +484,7 @@
21.160    sint_sbintrunc [simp]
21.161    unat_bintrunc [simp]
21.162
21.163 -lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w"
21.164 +lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
21.165    apply (unfold word_size)
21.166    apply (rule word_uint.Rep_eqD)
21.167    apply (rule box_equals)
21.168 @@ -508,13 +509,13 @@
21.169    iffD2 [OF linorder_not_le uint_m2p_neg, standard]
21.170
21.171  lemma lt2p_lem:
21.172 -  "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n"
21.173 +  "len_of TYPE('a) <= n \<Longrightarrow> uint (w :: 'a :: len0 word) < 2 ^ n"
21.174    by (rule xtr8 [OF _ uint_lt2p]) simp
21.175
21.176  lemmas uint_le_0_iff [simp] =
21.177    uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard]
21.178
21.179 -lemma uint_nat: "uint w == int (unat w)"
21.180 +lemma uint_nat: "uint w = int (unat w)"
21.181    unfolding unat_def by auto
21.182
21.183  lemma uint_number_of:
21.184 @@ -523,7 +524,7 @@
21.185    by (simp only: int_word_uint)
21.186
21.187  lemma unat_number_of:
21.188 -  "bin_sign b = Int.Pls ==>
21.189 +  "bin_sign b = Int.Pls \<Longrightarrow>
21.190    unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
21.191    apply (unfold unat_def)
21.192    apply (clarsimp simp only: uint_number_of)
21.193 @@ -590,7 +591,7 @@
21.194
21.195  lemma word_eqI [rule_format] :
21.196    fixes u :: "'a::len0 word"
21.197 -  shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v"
21.198 +  shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
21.199    apply (rule test_bit_eq_iff [THEN iffD1])
21.200    apply (rule ext)
21.201    apply (erule allE)
21.202 @@ -645,7 +646,7 @@
21.203                    "{bl. length bl = len_of TYPE('a::len0)}"
21.204    by (rule td_bl)
21.205
21.206 -lemma word_size_bl: "size w == size (to_bl w)"
21.207 +lemma word_size_bl: "size w = size (to_bl w)"
21.208    unfolding word_size by auto
21.209
21.210  lemma to_bl_use_of_bl:
21.211 @@ -658,7 +659,7 @@
21.212  lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
21.213    unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
21.214
21.215 -lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
21.216 +lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
21.217    by auto
21.218
21.219  lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
21.220 @@ -675,7 +676,7 @@
21.221    done
21.222
21.223  lemma of_bl_drop':
21.224 -  "lend = length bl - len_of TYPE ('a :: len0) ==>
21.225 +  "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow>
21.226      of_bl (drop lend bl) = (of_bl bl :: 'a word)"
21.227    apply (unfold of_bl_def)
21.228    apply (clarsimp simp add : trunc_bl2bin [symmetric])
21.229 @@ -693,7 +694,7 @@
21.230    "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
21.231    unfolding word_size of_bl_no by (simp add : word_number_of_def)
21.232
21.233 -lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
21.234 +lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
21.235    unfolding word_size to_bl_def by auto
21.236
21.237  lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
21.238 @@ -742,14 +743,14 @@
21.239    may want these in reverse, but loop as simp rules, so use following *)
21.240
21.241  lemma num_of_bintr':
21.242 -  "bintrunc (len_of TYPE('a :: len0)) a = b ==>
21.243 +  "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow>
21.244      number_of a = (number_of b :: 'a word)"
21.245    apply safe
21.246    apply (rule_tac num_of_bintr [symmetric])
21.247    done
21.248
21.249  lemma num_of_sbintr':
21.250 -  "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==>
21.251 +  "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow>
21.252      number_of a = (number_of b :: 'a word)"
21.253    apply safe
21.254    apply (rule_tac num_of_sbintr [symmetric])
21.255 @@ -769,7 +770,7 @@
21.256  lemma scast_id: "scast w = w"
21.257    unfolding scast_def by auto
21.258
21.259 -lemma ucast_bl: "ucast w == of_bl (to_bl w)"
21.260 +lemma ucast_bl: "ucast w = of_bl (to_bl w)"
21.261    unfolding ucast_def of_bl_def uint_bl
21.262    by (auto simp add : word_size)
21.263
21.264 @@ -799,7 +800,7 @@
21.265
21.266  lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
21.267
21.268 -lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
21.269 +lemma down_cast_same': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"
21.270    apply (unfold is_down)
21.271    apply safe
21.272    apply (rule ext)
21.273 @@ -809,7 +810,7 @@
21.274    done
21.275
21.276  lemma word_rev_tf':
21.277 -  "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
21.278 +  "r = to_bl (of_bl bl) \<Longrightarrow> r = rev (takefill False (length r) (rev bl))"
21.279    unfolding of_bl_def uint_bl
21.280    by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
21.281
21.282 @@ -829,17 +830,17 @@
21.283    done
21.284
21.285  lemma ucast_up_app':
21.286 -  "uc = ucast ==> source_size uc + n = target_size uc ==>
21.287 +  "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow>
21.288      to_bl (uc w) = replicate n False @ (to_bl w)"
21.289    by (auto simp add : source_size target_size to_bl_ucast)
21.290
21.291  lemma ucast_down_drop':
21.292 -  "uc = ucast ==> source_size uc = target_size uc + n ==>
21.293 +  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
21.294      to_bl (uc w) = drop n (to_bl w)"
21.295    by (auto simp add : source_size target_size to_bl_ucast)
21.296
21.297  lemma scast_down_drop':
21.298 -  "sc = scast ==> source_size sc = target_size sc + n ==>
21.299 +  "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
21.300      to_bl (sc w) = drop n (to_bl w)"
21.301    apply (subgoal_tac "sc = ucast")
21.302     apply safe
21.303 @@ -850,7 +851,7 @@
21.304    done
21.305
21.306  lemma sint_up_scast':
21.307 -  "sc = scast ==> is_up sc ==> sint (sc w) = sint w"
21.308 +  "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
21.309    apply (unfold is_up)
21.310    apply safe
21.311    apply (simp add: scast_def word_sbin.eq_norm)
21.312 @@ -865,7 +866,7 @@
21.313    done
21.314
21.315  lemma uint_up_ucast':
21.316 -  "uc = ucast ==> is_up uc ==> uint (uc w) = uint w"
21.317 +  "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
21.318    apply (unfold is_up)
21.319    apply safe
21.320    apply (rule bin_eqI)
21.321 @@ -881,18 +882,18 @@
21.322  lemmas uint_up_ucast = refl [THEN uint_up_ucast']
21.323  lemmas sint_up_scast = refl [THEN sint_up_scast']
21.324
21.325 -lemma ucast_up_ucast': "uc = ucast ==> is_up uc ==> ucast (uc w) = ucast w"
21.326 +lemma ucast_up_ucast': "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
21.327    apply (simp (no_asm) add: ucast_def)
21.328    apply (clarsimp simp add: uint_up_ucast)
21.329    done
21.330
21.331 -lemma scast_up_scast': "sc = scast ==> is_up sc ==> scast (sc w) = scast w"
21.332 +lemma scast_up_scast': "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
21.333    apply (simp (no_asm) add: scast_def)
21.334    apply (clarsimp simp add: sint_up_scast)
21.335    done
21.336
21.337  lemma ucast_of_bl_up':
21.338 -  "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
21.339 +  "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"
21.340    by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
21.341
21.342  lemmas ucast_up_ucast = refl [THEN ucast_up_ucast']
21.343 @@ -908,22 +909,22 @@
21.344  lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
21.345
21.346  lemma up_ucast_surj:
21.347 -  "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==>
21.348 +  "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
21.349     surj (ucast :: 'a word => 'b word)"
21.350    by (rule surjI, erule ucast_up_ucast_id)
21.351
21.352  lemma up_scast_surj:
21.353 -  "is_up (scast :: 'b::len word => 'a::len word) ==>
21.354 +  "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
21.355     surj (scast :: 'a word => 'b word)"
21.356    by (rule surjI, erule scast_up_scast_id)
21.357
21.358  lemma down_scast_inj:
21.359 -  "is_down (scast :: 'b::len word => 'a::len word) ==>
21.360 +  "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
21.361     inj_on (ucast :: 'a word => 'b word) A"
21.362    by (rule inj_on_inverseI, erule scast_down_scast_id)
21.363
21.364  lemma down_ucast_inj:
21.365 -  "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==>
21.366 +  "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
21.367     inj_on (ucast :: 'a word => 'b word) A"
21.368    by (rule inj_on_inverseI, erule ucast_down_ucast_id)
21.369
21.370 @@ -931,7 +932,7 @@
21.371    by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
21.372
21.373  lemma ucast_down_no':
21.374 -  "uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
21.375 +  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
21.376    apply (unfold word_number_of_def is_down)
21.377    apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
21.378    apply (rule word_ubin.norm_eq_iff [THEN iffD1])
21.379 @@ -940,7 +941,7 @@
21.380
21.381  lemmas ucast_down_no = ucast_down_no' [OF refl]
21.382
21.383 -lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
21.384 +lemma ucast_down_bl': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
21.385    unfolding of_bl_no by clarify (erule ucast_down_no)
21.386
21.387  lemmas ucast_down_bl = ucast_down_bl' [OF refl]
21.388 @@ -984,7 +985,7 @@
21.389    word_succ_def word_pred_def word_0_wi word_1_wi
21.390
21.391  lemma udvdI:
21.392 -  "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
21.393 +  "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
21.394    by (auto simp: udvd_def)
21.395
21.396  lemmas word_div_no [simp] =
21.397 @@ -1015,14 +1016,14 @@
21.398  lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
21.399  lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
21.400
21.401 -lemma int_one_bin: "(1 :: int) == (Int.Pls BIT 1)"
21.402 +lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
21.403    unfolding Pls_def Bit_def by auto
21.404
21.405  lemma word_1_no:
21.406 -  "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT 1)"
21.407 +  "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
21.408    unfolding word_1_wi word_number_of_def int_one_bin by auto
21.409
21.410 -lemma word_m1_wi: "-1 == word_of_int -1"
21.411 +lemma word_m1_wi: "-1 = word_of_int -1"
21.412    by (rule word_number_of_alt)
21.413
21.414  lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
21.415 @@ -1056,7 +1057,7 @@
21.416  lemma unat_0 [simp]: "unat 0 = 0"
21.417    unfolding unat_def by auto
21.418
21.419 -lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
21.420 +lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
21.421    apply (unfold word_size)
21.422    apply (rule box_equals)
21.423      defer
21.424 @@ -1129,11 +1130,11 @@
21.425
21.426  lemmas wi_hom_syms = wi_homs [symmetric]
21.427
21.428 -lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
21.429 +lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
21.430    unfolding word_sub_wi diff_minus
21.431    by (simp only : word_uint.Rep_inverse wi_hom_syms)
21.432
21.433 -lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
21.434 +lemmas word_diff_minus = word_sub_def [standard]
21.435
21.436  lemma word_of_int_sub_hom:
21.437    "(word_of_int a) - word_of_int b = word_of_int (a - b)"
21.438 @@ -1265,13 +1266,13 @@
21.439
21.440  subsection "Order on fixed-length words"
21.441
21.442 -lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
21.443 +lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
21.444    unfolding word_le_def by auto
21.445
21.446  lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
21.447    unfolding word_le_def by auto
21.448
21.449 -lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
21.450 +lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
21.451    unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
21.452
21.453  lemma word_order_linear:
21.454 @@ -1307,7 +1308,7 @@
21.455
21.456  lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard]
21.457
21.458 -lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
21.459 +lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
21.460    unfolding word_sle_def word_sless_def
21.461    by (auto simp add: less_le)
21.462
21.463 @@ -1347,7 +1348,7 @@
21.464
21.465  lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
21.466
21.467 -lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
21.468 +lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1";
21.469    unfolding word_arith_wis
21.470    by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
21.471
21.472 @@ -1356,7 +1357,7 @@
21.473  lemma no_no [simp] : "number_of (number_of b) = number_of b"
21.475
21.476 -lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1"
21.477 +lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
21.478    apply (unfold unat_def)
21.479    apply (simp only: int_word_uint word_arith_alts rdmods)
21.480    apply (subgoal_tac "uint x >= 1")
21.481 @@ -1378,7 +1379,7 @@
21.482    apply simp
21.483    done
21.484
21.485 -lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p"
21.486 +lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
21.488
21.490 @@ -1423,7 +1424,7 @@
21.491  subsection {* Definition of uint\_arith *}
21.492
21.493  lemma word_of_int_inverse:
21.494 -  "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==>
21.495 +  "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
21.496     uint (a::'a::len0 word) = r"
21.497    apply (erule word_uint.Abs_inverse' [rotated])
21.499 @@ -1454,7 +1455,7 @@
21.500    uint_sub_if' uint_plus_if'
21.501
21.502  (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
21.503 -lemma power_False_cong: "False ==> a ^ b = c ^ d"
21.504 +lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
21.505    by auto
21.506
21.507  (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
21.508 @@ -1520,11 +1521,11 @@
21.509  lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
21.510
21.511  lemma word_less_sub1:
21.512 -  "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
21.513 +  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
21.514    by uint_arith
21.515
21.516  lemma word_le_sub1:
21.517 -  "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
21.518 +  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
21.519    by uint_arith
21.520
21.521  lemma sub_wrap_lt:
21.522 @@ -1536,19 +1537,19 @@
21.523    by uint_arith
21.524
21.525  lemma plus_minus_not_NULL_ab:
21.526 -  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
21.527 +  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
21.528    by uint_arith
21.529
21.530  lemma plus_minus_no_overflow_ab:
21.531 -  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c"
21.532 +  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
21.533    by uint_arith
21.534
21.535  lemma le_minus':
21.536 -  "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
21.537 +  "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
21.538    by uint_arith
21.539
21.540  lemma le_plus':
21.541 -  "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
21.542 +  "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
21.543    by uint_arith
21.544
21.545  lemmas le_plus = le_plus' [rotated]
21.546 @@ -1556,90 +1557,90 @@
21.547  lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
21.548
21.549  lemma word_plus_mono_right:
21.550 -  "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
21.551 +  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
21.552    by uint_arith
21.553
21.554  lemma word_less_minus_cancel:
21.555 -  "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
21.556 +  "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
21.557    by uint_arith
21.558
21.559  lemma word_less_minus_mono_left:
21.560 -  "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
21.561 +  "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
21.562    by uint_arith
21.563
21.564  lemma word_less_minus_mono:
21.565 -  "a < c ==> d < b ==> a - b < a ==> c - d < c
21.566 -  ==> a - b < c - (d::'a::len word)"
21.567 +  "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
21.568 +  \<Longrightarrow> a - b < c - (d::'a::len word)"
21.569    by uint_arith
21.570
21.571  lemma word_le_minus_cancel:
21.572 -  "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
21.573 +  "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
21.574    by uint_arith
21.575
21.576  lemma word_le_minus_mono_left:
21.577 -  "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
21.578 +  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
21.579    by uint_arith
21.580
21.581  lemma word_le_minus_mono:
21.582 -  "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c
21.583 -  ==> a - b <= c - (d::'a::len word)"
21.584 +  "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
21.585 +  \<Longrightarrow> a - b <= c - (d::'a::len word)"
21.586    by uint_arith
21.587
21.588  lemma plus_le_left_cancel_wrap:
21.589 -  "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
21.590 +  "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
21.591    by uint_arith
21.592
21.593  lemma plus_le_left_cancel_nowrap:
21.594 -  "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==>
21.595 +  "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
21.596      (x + y' < x + y) = (y' < y)"
21.597    by uint_arith
21.598
21.599  lemma word_plus_mono_right2:
21.600 -  "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
21.601 +  "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
21.602    by uint_arith
21.603
21.605 -  "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
21.606 +  "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
21.607    by uint_arith
21.608
21.609  lemma word_less_sub_right:
21.610 -  "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
21.611 +  "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
21.612    by uint_arith
21.613
21.614  lemma word_le_plus_either:
21.615 -  "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
21.616 +  "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
21.617    by uint_arith
21.618
21.619  lemma word_less_nowrapI:
21.620 -  "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
21.621 +  "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
21.622    by uint_arith
21.623
21.624 -lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
21.625 +lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
21.626    by uint_arith
21.627
21.628  lemma inc_i:
21.629 -  "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
21.630 +  "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
21.631    by uint_arith
21.632
21.633  lemma udvd_incr_lem:
21.634 -  "up < uq ==> up = ua + n * uint K ==>
21.635 -    uq = ua + n' * uint K ==> up + uint K <= uq"
21.636 +  "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
21.637 +    uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
21.638    apply clarsimp
21.639    apply (drule less_le_mult)
21.640    apply safe
21.641    done
21.642
21.643  lemma udvd_incr':
21.644 -  "p < q ==> uint p = ua + n * uint K ==>
21.645 -    uint q = ua + n' * uint K ==> p + K <= q"
21.646 +  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
21.647 +    uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
21.648    apply (unfold word_less_alt word_le_def)
21.649    apply (drule (2) udvd_incr_lem)
21.650    apply (erule uint_add_le [THEN order_trans])
21.651    done
21.652
21.653  lemma udvd_decr':
21.654 -  "p < q ==> uint p = ua + n * uint K ==>
21.655 -    uint q = ua + n' * uint K ==> p <= q - K"
21.656 +  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
21.657 +    uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
21.658    apply (unfold word_less_alt word_le_def)
21.659    apply (drule (2) udvd_incr_lem)
21.660    apply (drule le_diff_eq [THEN iffD2])
21.661 @@ -1652,7 +1653,7 @@
21.662  lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
21.663
21.664  lemma udvd_minus_le':
21.665 -  "xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z"
21.666 +  "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
21.667    apply (unfold udvd_def)
21.668    apply clarify
21.669    apply (erule (2) udvd_decr0)
21.670 @@ -1661,8 +1662,8 @@
21.671  ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
21.672
21.673  lemma udvd_incr2_K:
21.674 -  "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==>
21.675 -    0 < K ==> p <= p + K & p + K <= a + s"
21.676 +  "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
21.677 +    0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
21.678    apply (unfold udvd_def)
21.679    apply clarify
21.680    apply (simp add: uint_arith_simps split: split_if_asm)
21.681 @@ -1680,7 +1681,7 @@
21.682
21.683  (* links with rbl operations *)
21.684  lemma word_succ_rbl:
21.685 -  "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
21.686 +  "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
21.687    apply (unfold word_succ_def)
21.688    apply clarify
21.690 @@ -1688,7 +1689,7 @@
21.691    done
21.692
21.693  lemma word_pred_rbl:
21.694 -  "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
21.695 +  "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
21.696    apply (unfold word_pred_def)
21.697    apply clarify
21.699 @@ -1696,7 +1697,7 @@
21.700    done
21.701
21.703 -  "to_bl v = vbl ==> to_bl w = wbl ==>
21.704 +  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
21.705      to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
21.707    apply clarify
21.708 @@ -1705,7 +1706,7 @@
21.709    done
21.710
21.711  lemma word_mult_rbl:
21.712 -  "to_bl v = vbl ==> to_bl w = wbl ==>
21.713 +  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
21.714      to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
21.715    apply (unfold word_mult_def)
21.716    apply clarify
21.717 @@ -1715,14 +1716,9 @@
21.718
21.719  lemma rtb_rbl_ariths:
21.720    "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
21.721 -
21.722    "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
21.723 -
21.724 -  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
21.725 -  ==> rev (to_bl (v * w)) = rbl_mult ys xs"
21.726 -
21.727 -  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |]
21.728 -  ==> rev (to_bl (v + w)) = rbl_add ys xs"
21.729 +  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
21.730 +  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
21.731    by (auto simp: rev_swap [symmetric] word_succ_rbl
21.733
21.734 @@ -1784,7 +1780,7 @@
21.735    done
21.736
21.737  lemma word_of_int_nat:
21.738 -  "0 <= x ==> word_of_int x = of_nat (nat x)"
21.739 +  "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
21.740    by (simp add: of_nat_nat word_of_int)
21.741
21.742  lemma word_number_of_eq:
21.743 @@ -1806,7 +1802,7 @@
21.744  subsection "Word and nat"
21.745
21.746  lemma td_ext_unat':
21.747 -  "n = len_of TYPE ('a :: len) ==>
21.748 +  "n = len_of TYPE ('a :: len) \<Longrightarrow>
21.749      td_ext (unat :: 'a word => nat) of_nat
21.750      (unats n) (%i. i mod 2 ^ n)"
21.751    apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
21.752 @@ -1829,7 +1825,7 @@
21.753
21.754  lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
21.755
21.756 -lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
21.757 +lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
21.758    apply (unfold unats_def)
21.759    apply clarsimp
21.760    apply (rule xtrans, rule unat_lt2p, assumption)
21.761 @@ -1864,11 +1860,11 @@
21.762
21.763  lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
21.764
21.765 -lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k"
21.766 +lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
21.767    by (cases k) auto
21.768
21.769  lemma of_nat_neq_0:
21.770 -  "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
21.771 +  "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
21.772    by (clarsimp simp add : of_nat_0)
21.773
21.775 @@ -1943,7 +1939,7 @@
21.776    trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
21.777
21.778  lemma le_no_overflow:
21.779 -  "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
21.780 +  "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
21.781    apply (erule order_trans)
21.782    apply (erule olen_add_eqv [THEN iffD1])
21.783    done
21.784 @@ -2064,7 +2060,7 @@
21.786
21.787  lemma word_div_mult:
21.788 -  "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==>
21.789 +  "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
21.790      x * y div y = x"
21.791    apply unat_arith
21.792    apply clarsimp
21.793 @@ -2072,7 +2068,7 @@
21.794    apply auto
21.795    done
21.796
21.797 -lemma div_lt': "(i :: 'a :: len word) <= k div x ==>
21.798 +lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow>
21.799      unat i * unat x < 2 ^ len_of TYPE('a)"
21.800    apply unat_arith
21.801    apply clarsimp
21.802 @@ -2083,7 +2079,7 @@
21.803
21.804  lemmas div_lt'' = order_less_imp_le [THEN div_lt']
21.805
21.806 -lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
21.807 +lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
21.808    apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
21.810    apply (drule (1) mult_less_mono1)
21.811 @@ -2092,7 +2088,7 @@
21.812    done
21.813
21.814  lemma div_le_mult:
21.815 -  "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
21.816 +  "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
21.817    apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
21.819    apply (drule mult_le_mono1)
21.820 @@ -2101,7 +2097,7 @@
21.821    done
21.822
21.823  lemma div_lt_uint':
21.824 -  "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
21.825 +  "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
21.826    apply (unfold uint_nat)
21.827    apply (drule div_lt')
21.828    apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric]
21.829 @@ -2111,7 +2107,7 @@
21.830  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
21.831
21.832  lemma word_le_exists':
21.833 -  "(x :: 'a :: len0 word) <= y ==>
21.834 +  "(x :: 'a :: len0 word) <= y \<Longrightarrow>
21.835      (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
21.836    apply (rule exI)
21.837    apply (rule conjI)
21.838 @@ -2164,7 +2160,7 @@
21.839    apply simp
21.840    done
21.841
21.842 -lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
21.843 +lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
21.844    apply (simp only: word_less_nat_alt word_arith_nat_defs)
21.845    apply (clarsimp simp add : uno_simps)
21.846    done
21.847 @@ -2178,7 +2174,7 @@
21.848    by (simp add : word_of_int_power_hom [symmetric])
21.849
21.850  lemma of_bl_length_less:
21.851 -  "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
21.852 +  "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
21.853    apply (unfold of_bl_no [unfolded word_number_of_def]
21.854                  word_less_alt word_number_of_alt)
21.855    apply safe
21.856 @@ -2246,7 +2242,7 @@
21.857                  bin_trunc_ao(1) [symmetric])
21.858
21.859  lemma word_ops_nth_size:
21.860 -  "n < size (x::'a::len0 word) ==>
21.861 +  "n < size (x::'a::len0 word) \<Longrightarrow>
21.862      (x OR y) !! n = (x !! n | y !! n) &
21.863      (x AND y) !! n = (x !! n & y !! n) &
21.864      (x XOR y) !! n = (x !! n ~= y !! n) &
21.865 @@ -2392,10 +2388,10 @@
21.866
21.867  lemma leoa:
21.868    fixes x :: "'a::len0 word"
21.869 -  shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
21.870 +  shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
21.871  lemma leao:
21.872    fixes x' :: "'a::len0 word"
21.873 -  shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto
21.874 +  shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
21.875
21.876  lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
21.877
21.878 @@ -2447,7 +2443,7 @@
21.879    by (simp add : sign_Min_lt_0 number_of_is_id)
21.880
21.881  lemma word_msb_no':
21.882 -  "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
21.883 +  "w = number_of bin \<Longrightarrow> msb (w::'a::len word) = bin_nth bin (size w - 1)"
21.884    unfolding word_msb_def word_number_of_def
21.885    by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
21.886
21.887 @@ -2487,7 +2483,7 @@
21.888    unfolding to_bl_def word_test_bit_def word_size
21.889    by (rule bin_nth_uint)
21.890
21.891 -lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
21.892 +lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
21.893    apply (unfold test_bit_bl)
21.894    apply clarsimp
21.895    apply (rule trans)
21.896 @@ -2530,7 +2526,7 @@
21.897  lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
21.898
21.899  lemma td_ext_nth':
21.900 -  "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==>
21.901 +  "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
21.902      td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
21.903    apply (unfold word_size td_ext_def')
21.904    apply (safe del: subset_antisym)
21.905 @@ -2575,7 +2571,7 @@
21.906
21.907  lemma test_bit_no':
21.908    fixes w :: "'a::len0 word"
21.909 -  shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
21.910 +  shows "w = number_of bin \<Longrightarrow> test_bit w n = (n < size w & bin_nth bin n)"
21.911    unfolding word_test_bit_def word_number_of_def word_size
21.912    by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
21.913
21.914 @@ -2605,10 +2601,13 @@
21.915                          test_bit_no nth_bintr)
21.916    done
21.917
21.918 -lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
21.919 -  simplified if_simps, THEN eq_reflection, standard]
21.920 -lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
21.921 -  simplified if_simps, THEN eq_reflection, standard]
21.922 +lemma setBit_no:
21.923 +  "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
21.924 +  by (simp add: setBit_def word_set_no)
21.925 +
21.926 +lemma clearBit_no:
21.927 +  "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
21.928 +  by (simp add: clearBit_def word_set_no)
21.929
21.930  lemma to_bl_n1:
21.931    "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
21.932 @@ -2643,7 +2642,7 @@
21.933    done
21.934
21.935  lemma test_bit_2p':
21.936 -  "w = word_of_int (2 ^ n) ==>
21.937 +  "w = word_of_int (2 ^ n) \<Longrightarrow>
21.938      w !! m = (m = n & m < size (w :: 'a :: len word))"
21.939    unfolding word_test_bit_def word_size
21.940    by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
21.941 @@ -2656,7 +2655,7 @@
21.943
21.944  lemma uint_2p:
21.945 -  "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
21.946 +  "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
21.947    apply (unfold word_arith_power_alt)
21.948    apply (case_tac "len_of TYPE ('a)")
21.949     apply clarsimp
21.950 @@ -2682,7 +2681,7 @@
21.951    apply simp
21.952    done
21.953
21.954 -lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)"
21.955 +lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
21.956    apply (rule xtr3)
21.957    apply (rule_tac [2] y = "x" in le_word_or2)
21.958    apply (rule word_eqI)
21.959 @@ -2996,7 +2995,7 @@
21.960  lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
21.961  lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
21.962
21.963 -lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
21.964 +lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
21.965    by (auto intro: append_take_drop_id [symmetric])
21.966
21.967  lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
21.968 @@ -3022,7 +3021,7 @@
21.969
21.970  lemma shiftl_zero_size:
21.971    fixes x :: "'a::len0 word"
21.972 -  shows "size x <= n ==> x << n = 0"
21.973 +  shows "size x <= n \<Longrightarrow> x << n = 0"
21.974    apply (unfold word_size)
21.975    apply (rule word_eqI)
21.976    apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
21.977 @@ -3059,7 +3058,7 @@
21.978    by (simp add : word_sbin.eq_norm)
21.979
21.980  lemma shiftr_no':
21.981 -  "w = number_of bin ==>
21.982 +  "w = number_of bin \<Longrightarrow>
21.983    (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
21.984    apply clarsimp
21.985    apply (rule word_eqI)
21.986 @@ -3067,7 +3066,7 @@
21.987    done
21.988
21.989  lemma sshiftr_no':
21.990 -  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^^ n)
21.991 +  "w = number_of bin \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n)
21.992      (sbintrunc (size w - 1) bin))"
21.993    apply clarsimp
21.994    apply (rule word_eqI)
21.995 @@ -3082,7 +3081,7 @@
21.996    shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
21.997
21.998  lemma shiftr1_bl_of':
21.999 -  "us = shiftr1 (of_bl bl) ==> length bl <= size us ==>
21.1000 +  "us = shiftr1 (of_bl bl) \<Longrightarrow> length bl <= size us \<Longrightarrow>
21.1001      us = of_bl (butlast bl)"
21.1002    by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin
21.1003                       word_ubin.eq_norm trunc_bl2bin)
21.1004 @@ -3090,7 +3089,7 @@
21.1005  lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
21.1006
21.1007  lemma shiftr_bl_of' [rule_format]:
21.1008 -  "us = of_bl bl >> n ==> length bl <= size us -->
21.1009 +  "us = of_bl bl >> n \<Longrightarrow> length bl <= size us -->
21.1010     us = of_bl (take (length bl - n) bl)"
21.1011    apply (unfold shiftr_def)
21.1012    apply hypsubst
21.1013 @@ -3147,8 +3146,8 @@
21.1014    done
21.1015
21.1017 -  "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
21.1018 -    take m (to_bl y) = replicate m False ==>
21.1019 +  "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
21.1020 +    take m (to_bl y) = replicate m False \<Longrightarrow>
21.1021      to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
21.1022    apply (subgoal_tac "x AND y = 0")
21.1023     prefer 2
21.1024 @@ -3167,7 +3166,7 @@
21.1025
21.1027
21.1028 -lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
21.1029 +lemma nth_mask': "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
21.1031    apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
21.1032    apply (clarsimp simp add: word_size)
21.1033 @@ -3247,14 +3246,14 @@
21.1034    done
21.1035
21.1036  lemma word_2p_lem:
21.1037 -  "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
21.1038 +  "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
21.1039    apply (unfold word_size word_less_alt word_number_of_alt)
21.1040    apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
21.1041                              int_mod_eq'
21.1042                    simp del: word_of_int_bin)
21.1043    done
21.1044
21.1045 -lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
21.1046 +lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
21.1047    apply (unfold word_less_alt word_number_of_alt)
21.1049                              word_uint.eq_norm
21.1050 @@ -3270,11 +3269,11 @@
21.1052    iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
21.1053
21.1054 -lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
21.1055 +lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
21.1056    unfolding word_size by (erule and_mask_less')
21.1057
21.1059 -  "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n"
21.1060 +  "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n"
21.1062
21.1064 @@ -3317,7 +3316,7 @@
21.1065    done
21.1066
21.1067  lemma revcast_rev_ucast':
21.1068 -  "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==>
21.1069 +  "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
21.1070      rc = word_reverse uc"
21.1071    apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
21.1072    apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
21.1073 @@ -3338,7 +3337,7 @@
21.1074  lemmas wsst_TYs = source_size target_size word_size
21.1075
21.1076  lemma revcast_down_uu':
21.1077 -  "rc = revcast ==> source_size rc = target_size rc + n ==>
21.1078 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
21.1079      rc (w :: 'a :: len word) = ucast (w >> n)"
21.1081    apply (rule word_bl.Rep_inverse')
21.1082 @@ -3349,7 +3348,7 @@
21.1083    done
21.1084
21.1085  lemma revcast_down_us':
21.1086 -  "rc = revcast ==> source_size rc = target_size rc + n ==>
21.1087 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
21.1088      rc (w :: 'a :: len word) = ucast (w >>> n)"
21.1090    apply (rule word_bl.Rep_inverse')
21.1091 @@ -3360,7 +3359,7 @@
21.1092    done
21.1093
21.1094  lemma revcast_down_su':
21.1095 -  "rc = revcast ==> source_size rc = target_size rc + n ==>
21.1096 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
21.1097      rc (w :: 'a :: len word) = scast (w >> n)"
21.1099    apply (rule word_bl.Rep_inverse')
21.1100 @@ -3371,7 +3370,7 @@
21.1101    done
21.1102
21.1103  lemma revcast_down_ss':
21.1104 -  "rc = revcast ==> source_size rc = target_size rc + n ==>
21.1105 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
21.1106      rc (w :: 'a :: len word) = scast (w >>> n)"
21.1108    apply (rule word_bl.Rep_inverse')
21.1109 @@ -3387,7 +3386,7 @@
21.1110  lemmas revcast_down_ss = refl [THEN revcast_down_ss']
21.1111
21.1112  lemma cast_down_rev:
21.1113 -  "uc = ucast ==> source_size uc = target_size uc + n ==>
21.1114 +  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
21.1115      uc w = revcast ((w :: 'a :: len word) << n)"
21.1116    apply (unfold shiftl_rev)
21.1117    apply clarify
21.1118 @@ -3399,7 +3398,7 @@
21.1119    done
21.1120
21.1121  lemma revcast_up':
21.1122 -  "rc = revcast ==> source_size rc + n = target_size rc ==>
21.1123 +  "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
21.1124      rc w = (ucast w :: 'a :: len word) << n"
21.1126    apply (rule word_bl.Rep_inverse')
21.1127 @@ -3424,13 +3423,14 @@
21.1128
21.1129  subsubsection "Slices"
21.1130
21.1131 -lemmas slice1_no_bin [simp] =
21.1132 -  slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
21.1133 -
21.1134 -lemmas slice_no_bin [simp] =
21.1135 -   trans [OF slice_def [THEN meta_eq_to_obj_eq]
21.1136 -             slice1_no_bin [THEN meta_eq_to_obj_eq],
21.1137 -          unfolded word_size, standard]
21.1138 +lemma slice1_no_bin [simp]:
21.1139 +  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
21.1140 +  by (simp add: slice1_def)
21.1141 +
21.1142 +lemma slice_no_bin [simp]:
21.1143 +  "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
21.1144 +    (bin_to_bl (len_of TYPE('b :: len0)) w))"
21.1145 +  by (simp add: slice_def word_size)
21.1146
21.1147  lemma slice1_0 [simp] : "slice1 n 0 = 0"
21.1148    unfolding slice1_def by (simp add : to_bl_0)
21.1149 @@ -3462,13 +3462,13 @@
21.1150    by (simp add : nth_ucast nth_shiftr)
21.1151
21.1152  lemma slice1_down_alt':
21.1153 -  "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==>
21.1154 +  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
21.1155      to_bl sl = takefill False fs (drop k (to_bl w))"
21.1156    unfolding slice1_def word_size of_bl_def uint_bl
21.1157    by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
21.1158
21.1159  lemma slice1_up_alt':
21.1160 -  "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==>
21.1161 +  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
21.1162      to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
21.1163    apply (unfold slice1_def word_size of_bl_def uint_bl)
21.1164    apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
21.1165 @@ -3495,7 +3495,7 @@
21.1166  lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
21.1167
21.1168  lemma revcast_slice1':
21.1169 -  "rc = revcast w ==> slice1 (size rc) w = rc"
21.1170 +  "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
21.1171    unfolding slice1_def revcast_def' by (simp add : word_size)
21.1172
21.1173  lemmas revcast_slice1 = refl [THEN revcast_slice1']
21.1174 @@ -3522,7 +3522,7 @@
21.1175    done
21.1176
21.1177  lemma rev_slice':
21.1178 -  "res = slice n (word_reverse w) ==> n + k + size res = size w ==>
21.1179 +  "res = slice n (word_reverse w) \<Longrightarrow> n + k + size res = size w \<Longrightarrow>
21.1180      res = word_reverse (slice k w)"
21.1181    apply (unfold slice_def word_size)
21.1182    apply clarify
21.1183 @@ -3569,8 +3569,8 @@
21.1184
21.1185  subsection "Split and cat"
21.1186
21.1187 -lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
21.1188 -lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
21.1189 +lemmas word_split_bin' = word_split_def
21.1190 +lemmas word_cat_bin' = word_cat_def
21.1191
21.1192  lemma word_rsplit_no:
21.1193    "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) =
21.1194 @@ -3584,7 +3584,7 @@
21.1195    [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
21.1196
21.1197  lemma test_bit_cat:
21.1198 -  "wc = word_cat a b ==> wc !! n = (n < size wc &
21.1199 +  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
21.1200      (if n < size b then b !! n else a !! (n - size b)))"
21.1201    apply (unfold word_cat_bin' test_bit_bin)
21.1202    apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
21.1203 @@ -3617,7 +3617,7 @@
21.1204    "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
21.1205    by (cases x) (simp_all add: of_bl_True)
21.1206
21.1207 -lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==>
21.1208 +lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow>
21.1209    a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
21.1210    apply (frule word_ubin.norm_Rep [THEN ssubst])
21.1211    apply (drule bin_split_trunc1)
21.1212 @@ -3627,7 +3627,7 @@
21.1213    done
21.1214
21.1215  lemma word_split_bl':
21.1216 -  "std = size c - size b ==> (word_split c = (a, b)) ==>
21.1217 +  "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
21.1218      (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
21.1219    apply (unfold word_split_bin')
21.1220    apply safe
21.1221 @@ -3653,7 +3653,7 @@
21.1222    apply (simp add : word_ubin.norm_eq_iff [symmetric])
21.1223    done
21.1224
21.1225 -lemma word_split_bl: "std = size c - size b ==>
21.1226 +lemma word_split_bl: "std = size c - size b \<Longrightarrow>
21.1227      (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <->
21.1228      word_split c = (a, b)"
21.1229    apply (rule iffI)
21.1230 @@ -3714,7 +3714,7 @@
21.1231  -- "limited hom result"
21.1232  lemma word_cat_hom:
21.1233    "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
21.1234 -  ==>
21.1235 +  \<Longrightarrow>
21.1236    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
21.1237    word_of_int (bin_cat w (size b) (uint b))"
21.1238    apply (unfold word_cat_def word_size)
21.1239 @@ -3723,7 +3723,7 @@
21.1240    done
21.1241
21.1242  lemma word_cat_split_alt:
21.1243 -  "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
21.1244 +  "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
21.1245    apply (rule word_eqI)
21.1246    apply (drule test_bit_split)
21.1247    apply (clarsimp simp add : test_bit_cat word_size)
21.1248 @@ -3738,14 +3738,14 @@
21.1249  subsubsection "Split and slice"
21.1250
21.1251  lemma split_slices:
21.1252 -  "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
21.1253 +  "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
21.1254    apply (drule test_bit_split)
21.1255    apply (rule conjI)
21.1256     apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
21.1257    done
21.1258
21.1259  lemma slice_cat1':
21.1260 -  "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
21.1261 +  "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
21.1262    apply safe
21.1263    apply (rule word_eqI)
21.1264    apply (simp add: nth_slice test_bit_cat word_size)
21.1265 @@ -3755,8 +3755,8 @@
21.1266  lemmas slice_cat2 = trans [OF slice_id word_cat_id]
21.1267
21.1268  lemma cat_slices:
21.1269 -  "a = slice n c ==> b = slice 0 c ==> n = size b ==>
21.1270 -    size a + size b >= size c ==> word_cat a b = c"
21.1271 +  "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
21.1272 +    size a + size b >= size c \<Longrightarrow> word_cat a b = c"
21.1273    apply safe
21.1274    apply (rule word_eqI)
21.1275    apply (simp add: nth_slice test_bit_cat word_size)
21.1276 @@ -3765,7 +3765,7 @@
21.1277    done
21.1278
21.1279  lemma word_split_cat_alt:
21.1280 -  "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
21.1281 +  "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
21.1282    apply (case_tac "word_split ?w")
21.1283    apply (rule trans, assumption)
21.1284    apply (drule test_bit_split)
21.1285 @@ -3794,8 +3794,8 @@
21.1286    by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
21.1287
21.1288  lemma test_bit_rsplit:
21.1289 -  "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==>
21.1290 -    k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
21.1291 +  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>
21.1292 +    k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
21.1293    apply (unfold word_rsplit_def word_test_bit_def)
21.1294    apply (rule trans)
21.1295     apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
21.1296 @@ -3812,7 +3812,7 @@
21.1297    apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
21.1298    done
21.1299
21.1300 -lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
21.1301 +lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
21.1302    unfolding word_rcat_def to_bl_def' of_bl_def
21.1303    by (clarsimp simp add : bin_rcat_bl)
21.1304
21.1305 @@ -3825,7 +3825,7 @@
21.1306  lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
21.1307
21.1308  lemma nth_rcat_lem' [rule_format] :
21.1309 -  "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw -->
21.1310 +  "sw = size (hd wl  :: 'a :: len word) \<Longrightarrow> (ALL n. n < size wl * sw -->
21.1311      rev (concat (map to_bl wl)) ! n =
21.1312      rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
21.1313    apply (unfold word_size)
21.1314 @@ -3840,7 +3840,7 @@
21.1315  lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
21.1316
21.1317  lemma test_bit_rcat:
21.1318 -  "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n =
21.1319 +  "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
21.1320      (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
21.1321    apply (unfold word_rcat_bl word_size)
21.1322    apply (clarsimp simp add :
21.1323 @@ -3862,8 +3862,8 @@
21.1324
21.1325  -- "lazy way of expressing that u and v, and su and sv, have same types"
21.1326  lemma word_rsplit_len_indep':
21.1327 -  "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==>
21.1328 -    word_rsplit v = sv ==> length su = length sv"
21.1329 +  "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
21.1330 +    word_rsplit v = sv \<Longrightarrow> length su = length sv"
21.1331    apply (unfold word_rsplit_def)
21.1332    apply (auto simp add : bin_rsplit_len_indep)
21.1333    done
21.1334 @@ -3871,7 +3871,7 @@
21.1335  lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
21.1336
21.1337  lemma length_word_rsplit_size:
21.1338 -  "n = len_of TYPE ('a :: len) ==>
21.1339 +  "n = len_of TYPE ('a :: len) \<Longrightarrow>
21.1340      (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
21.1341    apply (unfold word_rsplit_def word_size)
21.1342    apply (clarsimp simp add : bin_rsplit_len_le)
21.1343 @@ -3881,12 +3881,12 @@
21.1344    length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
21.1345
21.1346  lemma length_word_rsplit_exp_size:
21.1347 -  "n = len_of TYPE ('a :: len) ==>
21.1348 +  "n = len_of TYPE ('a :: len) \<Longrightarrow>
21.1349      length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
21.1350    unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
21.1351
21.1352  lemma length_word_rsplit_even_size:
21.1353 -  "n = len_of TYPE ('a :: len) ==> size w = m * n ==>
21.1354 +  "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow>
21.1355      length (word_rsplit w :: 'a word list) = m"
21.1356    by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
21.1357
21.1358 @@ -3907,8 +3907,8 @@
21.1359    done
21.1360
21.1361  lemma size_word_rsplit_rcat_size':
21.1362 -  "word_rcat (ws :: 'a :: len word list) = frcw ==>
21.1363 -    size frcw = length ws * len_of TYPE ('a) ==>
21.1364 +  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
21.1365 +    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow>
21.1366      size (hd [word_rsplit frcw, ws]) = size ws"
21.1367    apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
21.1368    apply (fast intro: given_quot_alt)
21.1369 @@ -3924,8 +3924,8 @@
21.1371
21.1372  lemma word_rsplit_rcat_size':
21.1373 -  "word_rcat (ws :: 'a :: len word list) = frcw ==>
21.1374 -    size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws"
21.1375 +  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
21.1376 +    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws"
21.1377    apply (frule size_word_rsplit_rcat_size, assumption)
21.1378    apply (clarsimp simp add : word_size)
21.1379    apply (rule nth_equalityI, assumption)
21.1380 @@ -3957,7 +3957,7 @@
21.1381  lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
21.1382
21.1383  lemma rotate_eq_mod:
21.1384 -  "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
21.1385 +  "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
21.1386    apply (rule box_equals)
21.1387      defer
21.1388      apply (rule rotate_conv_mod [symmetric])+
21.1389 @@ -4049,11 +4049,11 @@
21.1390
21.1391  subsubsection "map, map2, commuting with rotate(r)"
21.1392
21.1393 -lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
21.1394 +lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
21.1395    by (induct xs) auto
21.1396
21.1397  lemma butlast_map:
21.1398 -  "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
21.1399 +  "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
21.1400    by (induct xs) auto
21.1401
21.1402  lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
21.1403 @@ -4085,7 +4085,7 @@
21.1404    done
21.1405
21.1406  lemma rotater1_zip:
21.1407 -  "length xs = length ys ==>
21.1408 +  "length xs = length ys \<Longrightarrow>
21.1409      rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
21.1410    apply (unfold rotater1_def)
21.1411    apply (cases "xs")
21.1412 @@ -4094,7 +4094,7 @@
21.1413    done
21.1414
21.1415  lemma rotater1_map2:
21.1416 -  "length xs = length ys ==>
21.1417 +  "length xs = length ys \<Longrightarrow>
21.1418      rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
21.1419    unfolding map2_def by (simp add: rotater1_map rotater1_zip)
21.1420
21.1421 @@ -4104,12 +4104,12 @@
21.1422                THEN rotater1_map2]
21.1423
21.1424  lemma rotater_map2:
21.1425 -  "length xs = length ys ==>
21.1426 +  "length xs = length ys \<Longrightarrow>
21.1427      rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
21.1428    by (induct n) (auto intro!: lrth)
21.1429
21.1430  lemma rotate1_map2:
21.1431 -  "length xs = length ys ==>
21.1432 +  "length xs = length ys \<Longrightarrow>
21.1433      rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
21.1434    apply (unfold map2_def)
21.1435    apply (cases xs)
21.1436 @@ -4120,7 +4120,7 @@
21.1437    length_rotate [symmetric], THEN rotate1_map2]
21.1438
21.1439  lemma rotate_map2:
21.1440 -  "length xs = length ys ==>
21.1441 +  "length xs = length ys \<Longrightarrow>
21.1442      rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
21.1443    by (induct n) (auto intro!: lth)
21.1444
21.1445 @@ -4177,11 +4177,11 @@
21.1446    "word_roti (m + n) w = word_roti m (word_roti n w)"
21.1447  proof -
21.1448    have rotater_eq_lem:
21.1449 -    "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
21.1450 +    "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
21.1451      by auto
21.1452
21.1453    have rotate_eq_lem:
21.1454 -    "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
21.1455 +    "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
21.1456      by auto
21.1457
21.1458    note rpts [symmetric, standard] =
21.1459 @@ -4271,7 +4271,7 @@
21.1460    simplified word_bl.Rep', standard]
21.1461
21.1462  lemma bl_word_roti_dt':
21.1463 -  "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==>
21.1464 +  "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>
21.1465      to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
21.1466    apply (unfold word_roti_def)
21.1467    apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
21.1468 @@ -4457,12 +4457,12 @@
21.1470
21.1471  lemma map_replicate_True:
21.1472 -  "n = length xs ==>
21.1473 +  "n = length xs \<Longrightarrow>
21.1474      map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
21.1475    by (induct xs arbitrary: n) auto
21.1476
21.1477  lemma map_replicate_False:
21.1478 -  "n = length xs ==> map (\<lambda>(x,y). x & y)
21.1479 +  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
21.1480      (zip xs (replicate n False)) = replicate n False"
21.1481    by (induct xs arbitrary: n) auto
21.1482
21.1483 @@ -4488,7 +4488,7 @@
21.1484  qed
21.1485
21.1486  lemma drop_rev_takefill:
21.1487 -  "length xs \<le> n ==>
21.1488 +  "length xs \<le> n \<Longrightarrow>
21.1489      drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
21.1490    by (simp add: takefill_alt rev_take)
21.1491
21.1492 @@ -4547,7 +4547,7 @@
21.1493                  word_size)
21.1494
21.1495  lemma unat_sub:
21.1496 -  "b <= a ==> unat (a - b) = unat a - unat b"
21.1497 +  "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
21.1498    by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
21.1499
21.1500  lemmas word_less_sub1_numberof [simp] =
21.1501 @@ -4633,7 +4633,7 @@
21.1502    done
21.1503
21.1504  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
21.1505 -  "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
21.1506 +  "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
21.1507
21.1508  lemma word_rec_0: "word_rec z s 0 = z"
```
```    22.1 --- a/src/HOL/ZF/Games.thy	Tue Nov 30 18:22:43 2010 +0100
22.2 +++ b/src/HOL/ZF/Games.thy	Tue Nov 30 21:54:15 2010 +0100
22.3 @@ -893,9 +893,9 @@
22.4    have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel"
22.6      apply (auto simp add: eq_game_rel_def eq_game_def)
22.7 -    apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
22.8 +    apply (rule_tac y="plus_game a ba" in ge_game_trans)
22.9      apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
22.10 -    apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
22.11 +    apply (rule_tac y="plus_game b aa" in ge_game_trans)
22.12      apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
22.13      done
22.14    then show ?thesis
```
```    23.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 18:22:43 2010 +0100
23.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 21:54:15 2010 +0100
23.3 @@ -1288,7 +1288,7 @@
23.4  proof -
23.5    have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
23.6          respects2 realrel"