merged
authorboehmes
Tue Nov 30 21:54:15 2010 +0100 (2010-11-30)
changeset 40829edd1e0764da1
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.22 +apply (simp add: lub_Cons)
    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.10 -apply (simp_all add: listrel.intros)
    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.19      by (simp add: add_int_def UN_UN_split_split_eq
    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.25 -    by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
    7.26 +    by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
    7.27              del: of_nat_add) 
    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.19 -  apply(simp add: fun_eq_iff)
    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.218    apply (simp add: fun_eq_iff)
   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.64 -  apply(simp add: split_option_all)
   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.76 -  apply(simp_all add: split_option_all)
   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.104    apply(simp add: fun_eq_iff)
  10.105    apply(simp add: Quotient_abs_rep[OF q])
  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.5    by (simp add: prod_rel_def)
    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.47 -  apply(simp add: split_paired_all)
   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.38 -  apply(simp_all add: split_sum_all)
   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.69 -  apply(simp add: split_sum_all)
   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.102    apply(simp add: Quotient_abs_rep[OF q1])
  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.111    apply(simp add: Quotient_abs_rep[OF q2])
  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.4  by (simp add: starrel_def)
    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.254 -  by (simp add:)
  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.263 -  by (simp add:)
  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.269    apply(simp add: in_respects fun_rel_def)
  15.270    apply(rule impI)
  15.271    using a equivp_reflp_symp_transp[of "R2"]
  15.272 -  apply(simp add: reflp_def)
  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.283 -  apply(simp add: reflp_def)
  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.40     apply (simp add: realrel_def)
   19.41    apply (subst real_case_1 [OF _ Y])
   19.42     apply (rule congruent2_implies_congruent [OF equiv_realrel f])
   19.43     apply (simp add: realrel_def)
   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.47    apply (simp add: Y)
   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.474    by (simp add: number_of_eq)
  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.487    by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
  21.488    
  21.489  lemmas uint_add_ge0 [simp] =
  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.498    apply (simp add: uints_num)
  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.604  lemma word_less_add_right: 
  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.689    apply (simp add: to_bl_of_bin)
  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.698    apply (simp add: to_bl_of_bin)
  21.699 @@ -1696,7 +1697,7 @@
  21.700    done
  21.701  
  21.702  lemma word_add_rbl:
  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.706    apply (unfold word_add_def)
  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.732                   word_pred_rbl word_mult_rbl word_add_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.774  lemma Abs_fnat_hom_add:
  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.785  lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
  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.809    apply (simp add: unat_arith_simps)
  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.818    apply (simp add: unat_arith_simps)
  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.942    by (simp add:  of_int_power)
  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.1016  lemma aligned_bl_add_size':
 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.1026  subsubsection "Mask"
 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.1030    apply (unfold mask_def test_bit_bl)
 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.1048    apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
 21.1049                              word_uint.eq_norm
 21.1050 @@ -3270,11 +3269,11 @@
 21.1051  lemmas and_mask_less' = 
 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.1058  lemma word_mod_2p_is_mask':
 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.1061    by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
 21.1062  
 21.1063  lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
 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.1080    apply (simp add: revcast_def')
 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.1089    apply (simp add: revcast_def')
 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.1098    apply (simp add: revcast_def')
 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.1107    apply (simp add: revcast_def')
 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.1125    apply (simp add: revcast_def')
 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.1370    by (auto simp: add_commute)
 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.1469    by (simp add: mask_bl word_rep_drop min_def)
 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"
 21.1509    by (simp add: word_rec_def)
    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.5      apply (simp add: congruent2_def)
    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"
    23.7 -    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
    23.8 +    by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
    23.9    thus ?thesis
   23.10      by (simp add: real_add_def UN_UN_split_split_eq
   23.11                    UN_equiv_class2 [OF equiv_realrel equiv_realrel])
   23.12 @@ -1297,7 +1297,7 @@
   23.13  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
   23.14  proof -
   23.15    have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
   23.16 -    by (simp add: congruent_def add_commute) 
   23.17 +    by (auto simp add: congruent_def add_commute) 
   23.18    thus ?thesis
   23.19      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
   23.20  qed