# HG changeset patch
# User boehmes
# Date 1291150455 -3600
# Node ID edd1e0764da1f4ae69c0063377823acd856a89ef
# Parent  47ff261431c46a91cca93df91aabe2da16ff617e# Parent  abbc05c20e243a99b78fba6c547abb6d0052f5dd
merged

diff -r 47ff261431c4 -r edd1e0764da1 NEWS
--- a/NEWS	Tue Nov 30 18:22:43 2010 +0100
+++ b/NEWS	Tue Nov 30 21:54:15 2010 +0100
@@ -92,6 +92,9 @@
 
 *** HOL ***
 
+* Abandoned locale equiv for equivalence relations.  INCOMPATIBILITY: use
+equivI rather than equiv_intro.
+
 * Code generator: globbing constant expressions "*" and "Theory.*" have been
 replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
 
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -606,7 +606,7 @@
 proof -
   interpret group G by fact
   show ?thesis
-  proof (intro equiv.intro)
+  proof (intro equivI)
     show "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def) 
   next
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -8,13 +8,19 @@
 imports Big_Operators Relation Plain
 begin
 
-subsection {* Equivalence relations *}
+subsection {* Equivalence relations -- set version *}
+
+definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
+  "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
 
-locale equiv =
-  fixes A and r
-  assumes refl_on: "refl_on A r"
-    and sym: "sym r"
-    and trans: "trans r"
+lemma equivI:
+  "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+  by (simp add: equiv_def)
+
+lemma equivE:
+  assumes "equiv A r"
+  obtains "refl_on A r" and "sym r" and "trans r"
+  using assms by (simp add: equiv_def)
 
 text {*
   Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
@@ -157,9 +163,17 @@
 subsection {* Defining unary operations upon equivalence classes *}
 
 text{*A congruence-preserving function*}
-locale congruent =
-  fixes r and f
-  assumes congruent: "(y,z) \<in> r ==> f y = f z"
+
+definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
+  "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
+
+lemma congruentI:
+  "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
+  by (auto simp add: congruent_def)
+
+lemma congruentD:
+  "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
+  by (auto simp add: congruent_def)
 
 abbreviation
   RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
@@ -214,10 +228,18 @@
 subsection {* Defining binary operations upon equivalence classes *}
 
 text{*A congruence-preserving function of two arguments*}
-locale congruent2 =
-  fixes r1 and r2 and f
-  assumes congruent2:
-    "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
+
+definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
+  "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
+
+lemma congruent2I':
+  assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
+  shows "congruent2 r1 r2 f"
+  using assms by (auto simp add: congruent2_def)
+
+lemma congruent2D:
+  "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
+  using assms by (auto simp add: congruent2_def)
 
 text{*Abbreviation for the common case where the relations are identical*}
 abbreviation
@@ -331,4 +353,99 @@
 apply simp
 done
 
+
+subsection {* Equivalence relations -- predicate version *}
+
+text {* Partial equivalences *}
+
+definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)"
+    -- {* John-Harrison-style characterization *}
+
+lemma part_equivpI:
+  "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
+  by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE)
+
+lemma part_equivpE:
+  assumes "part_equivp R"
+  obtains x where "R x x" and "symp R" and "transp R"
+proof -
+  from assms have 1: "\<exists>x. R x x"
+    and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y"
+    by (unfold part_equivp_def) blast+
+  from 1 obtain x where "R x x" ..
+  moreover have "symp R"
+  proof (rule sympI)
+    fix x y
+    assume "R x y"
+    with 2 [of x y] show "R y x" by auto
+  qed
+  moreover have "transp R"
+  proof (rule transpI)
+    fix x y z
+    assume "R x y" and "R y z"
+    with 2 [of x y] 2 [of y z] show "R x z" by auto
+  qed
+  ultimately show thesis by (rule that)
+qed
+
+lemma part_equivp_refl_symp_transp:
+  "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R"
+  by (auto intro: part_equivpI elim: part_equivpE)
+
+lemma part_equivp_symp:
+  "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (erule part_equivpE, erule sympE)
+
+lemma part_equivp_transp:
+  "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+  by (erule part_equivpE, erule transpE)
+
+lemma part_equivp_typedef:
+  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
+  by (auto elim: part_equivpE simp add: mem_def)
+
+
+text {* Total equivalences *}
+
+definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *}
+
+lemma equivpI:
+  "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
+  by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
+
+lemma equivpE:
+  assumes "equivp R"
+  obtains "reflp R" and "symp R" and "transp R"
+  using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)
+
+lemma equivp_implies_part_equivp:
+  "equivp R \<Longrightarrow> part_equivp R"
+  by (auto intro: part_equivpI elim: equivpE reflpE)
+
+lemma equivp_equiv:
+  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
+  by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def)
+
+lemma equivp_reflp_symp_transp:
+  shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
+  by (auto intro: equivpI elim: equivpE)
+
+lemma identity_equivp:
+  "equivp (op =)"
+  by (auto intro: equivpI reflpI sympI transpI)
+
+lemma equivp_reflp:
+  "equivp R \<Longrightarrow> R x x"
+  by (erule equivpE, erule reflpE)
+
+lemma equivp_symp:
+  "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
+  by (erule equivpE, erule sympE)
+
+lemma equivp_transp:
+  "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+  by (erule equivpE, erule transpE)
+
 end
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -237,6 +237,54 @@
 deserve to have continuity lemmas.  I'll add more as they are
 needed. *}
 
+subsection {* Lists are a discrete cpo *}
+
+instance list :: (discrete_cpo) discrete_cpo
+proof
+  fix xs ys :: "'a list"
+  show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys"
+    by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
+qed
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_Nil [simp]: "compact []"
+apply (rule compactI2)
+apply (erule list_chain_cases)
+apply simp
+apply (simp add: lub_Cons)
+done
+
+lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)"
+apply (rule compactI2)
+apply (erule list_chain_cases)
+apply (auto simp add: lub_Cons dest!: compactD2)
+apply (rename_tac i j, rule_tac x="max i j" in exI)
+apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI1]])
+apply (drule (1) below_trans [OF _ chain_mono [OF _ le_maxI2]])
+apply (erule (1) conjI)
+done
+
+lemma compact_Cons_iff [simp]:
+  "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs"
+apply (safe intro!: compact_Cons)
+apply (simp only: compact_def)
+apply (subgoal_tac "cont (\<lambda>x. x # xs)")
+apply (drule (1) adm_subst, simp, simp)
+apply (simp only: compact_def)
+apply (subgoal_tac "cont (\<lambda>xs. x # xs)")
+apply (drule (1) adm_subst, simp, simp)
+done
+
+instance list :: (chfin) chfin
+proof
+  fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y"
+  moreover have "\<And>(xs::'a list). compact xs"
+    by (induct_tac xs, simp_all)
+  ultimately show "\<exists>i. max_in_chain i Y"
+    by (rule compact_imp_max_in_chain)
+qed
+
 subsection {* Using lists with fixrec *}
 
 definition
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -176,7 +176,7 @@
               Abs_Msg (msgrel``{MPAIR U V})"
 proof -
   have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
-    by (simp add: congruent2_def msgrel.MPAIR)
+    by (auto simp add: congruent2_def msgrel.MPAIR)
   thus ?thesis
     by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
 qed
@@ -184,7 +184,7 @@
 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
 proof -
   have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
-    by (simp add: congruent_def msgrel.CRYPT)
+    by (auto simp add: congruent_def msgrel.CRYPT)
   thus ?thesis
     by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
 qed
@@ -193,7 +193,7 @@
      "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
 proof -
   have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
-    by (simp add: congruent_def msgrel.DECRYPT)
+    by (auto simp add: congruent_def msgrel.DECRYPT)
   thus ?thesis
     by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
 qed
@@ -221,7 +221,7 @@
    "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
 
 lemma nonces_congruent: "freenonces respects msgrel"
-by (simp add: congruent_def msgrel_imp_eq_freenonces) 
+by (auto simp add: congruent_def msgrel_imp_eq_freenonces) 
 
 
 text{*Now prove the four equations for @{term nonces}*}
@@ -256,7 +256,7 @@
    "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
 
 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
-by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
+by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) 
 
 text{*Now prove the four equations for @{term left}*}
 
@@ -290,7 +290,7 @@
    "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
 
 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
-by (simp add: congruent_def msgrel_imp_eqv_freeright) 
+by (auto simp add: congruent_def msgrel_imp_eqv_freeright) 
 
 text{*Now prove the four equations for @{term right}*}
 
@@ -425,7 +425,7 @@
    "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
 
 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
-by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
+by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) 
 
 text{*Now prove the four equations for @{term discrim}*}
 
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -125,14 +125,19 @@
 | "freeargs (FNCALL F Xs) = Xs"
 
 theorem exprel_imp_eqv_freeargs:
-     "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
-apply (induct set: exprel)
-apply (erule_tac [4] listrel.induct) 
-apply (simp_all add: listrel.intros)
-apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
-apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
-done
-
+  assumes "U \<sim> V"
+  shows "(freeargs U, freeargs V) \<in> listrel exprel"
+proof -
+  from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
+  from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
+  from assms show ?thesis
+    apply induct
+    apply (erule_tac [4] listrel.induct) 
+    apply (simp_all add: listrel.intros)
+    apply (blast intro: symD [OF sym])
+    apply (blast intro: transD [OF trans])
+    done
+qed
 
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
@@ -220,7 +225,7 @@
              Abs_Exp (exprel``{PLUS U V})"
 proof -
   have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
-    by (simp add: congruent2_def exprel.PLUS)
+    by (auto simp add: congruent2_def exprel.PLUS)
   thus ?thesis
     by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
 qed
@@ -236,13 +241,13 @@
 
 lemma FnCall_respects: 
      "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
-  by (simp add: congruent_def exprel.FNCALL)
+  by (auto simp add: congruent_def exprel.FNCALL)
 
 lemma FnCall_sing:
      "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
 proof -
   have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
-    by (simp add: congruent_def FNCALL_Cons listrel.intros)
+    by (auto simp add: congruent_def FNCALL_Cons listrel.intros)
   thus ?thesis
     by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
 qed
@@ -255,7 +260,7 @@
      "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
 proof -
   have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
-    by (simp add: congruent_def exprel.FNCALL)
+    by (auto simp add: congruent_def exprel.FNCALL)
   thus ?thesis
     by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
                   listset_Rep_Exp_Abs_Exp)
@@ -275,7 +280,7 @@
   "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
 
 lemma vars_respects: "freevars respects exprel"
-by (simp add: congruent_def exprel_imp_eq_freevars) 
+by (auto simp add: congruent_def exprel_imp_eq_freevars) 
 
 text{*The extension of the function @{term vars} to lists*}
 primrec vars_list :: "exp list \<Rightarrow> nat set" where
@@ -340,7 +345,7 @@
   "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
 
 lemma fun_respects: "(%U. {freefun U}) respects exprel"
-by (simp add: congruent_def exprel_imp_eq_freefun) 
+by (auto simp add: congruent_def exprel_imp_eq_freefun) 
 
 lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
 apply (cases Xs rule: eq_Abs_ExpList) 
@@ -358,7 +363,7 @@
   by (induct set: listrel) simp_all
 
 lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
-by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
+by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
 
 lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
 apply (cases Xs rule: eq_Abs_ExpList) 
@@ -387,7 +392,7 @@
   "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
 
 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
-by (simp add: congruent_def exprel_imp_eq_freediscrim) 
+by (auto simp add: congruent_def exprel_imp_eq_freediscrim) 
 
 text{*Now prove the four equations for @{term discrim}*}
 
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Int.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -102,7 +102,7 @@
 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
 proof -
   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
-    by (simp add: congruent_def) 
+    by (auto simp add: congruent_def)
   thus ?thesis
     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
 qed
@@ -113,7 +113,7 @@
 proof -
   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
         respects2 intrel"
-    by (simp add: congruent2_def)
+    by (auto simp add: congruent2_def)
   thus ?thesis
     by (simp add: add_int_def UN_UN_split_split_eq
                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
@@ -288,7 +288,7 @@
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
-    by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
+    by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
             del: of_nat_add) 
   thus ?thesis
     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
@@ -394,7 +394,7 @@
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
   have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (simp add: congruent_def) arith
+    by (auto simp add: congruent_def)
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -43,7 +43,7 @@
 qed
   
 lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
-  by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
+  by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
 
 lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
 lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
@@ -121,7 +121,7 @@
 lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
 proof -
   have "(\<lambda>x. fractrel `` {(- fst x, snd x :: 'a)}) respects fractrel"
-    by (simp add: congruent_def)
+    by (simp add: congruent_def split_paired_all)
   then show ?thesis by (simp add: Fract_def minus_fract_def UN_fractrel)
 qed
 
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -10,94 +10,96 @@
 
 declare [[map list = (map, list_all2)]]
 
-lemma split_list_all:
-  shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
-  apply(auto)
-  apply(case_tac x)
-  apply(simp_all)
-  done
+lemma map_id [id_simps]:
+  "map id = id"
+  by (simp add: id_def fun_eq_iff map.identity)
 
-lemma map_id[id_simps]:
-  shows "map id = id"
-  apply(simp add: fun_eq_iff)
-  apply(rule allI)
-  apply(induct_tac x)
-  apply(simp_all)
-  done
+lemma list_all2_map1:
+  "list_all2 R (map f xs) ys \<longleftrightarrow> list_all2 (\<lambda>x. R (f x)) xs ys"
+  by (induct xs ys rule: list_induct2') simp_all
+
+lemma list_all2_map2:
+  "list_all2 R xs (map f ys) \<longleftrightarrow> list_all2 (\<lambda>x y. R x (f y)) xs ys"
+  by (induct xs ys rule: list_induct2') simp_all
 
-lemma list_all2_reflp:
-  shows "equivp R \<Longrightarrow> list_all2 R xs xs"
-  by (induct xs, simp_all add: equivp_reflp)
+lemma list_all2_eq [id_simps]:
+  "list_all2 (op =) = (op =)"
+proof (rule ext)+
+  fix xs ys
+  show "list_all2 (op =) xs ys \<longleftrightarrow> xs = ys"
+    by (induct xs ys rule: list_induct2') simp_all
+qed
 
-lemma list_all2_symp:
-  assumes a: "equivp R"
-  and b: "list_all2 R xs ys"
-  shows "list_all2 R ys xs"
-  using list_all2_lengthD[OF b] b
-  apply(induct xs ys rule: list_induct2)
-  apply(simp_all)
-  apply(rule equivp_symp[OF a])
-  apply(simp)
-  done
+lemma list_reflp:
+  assumes "reflp R"
+  shows "reflp (list_all2 R)"
+proof (rule reflpI)
+  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
+  fix xs
+  show "list_all2 R xs xs"
+    by (induct xs) (simp_all add: *)
+qed
 
-lemma list_all2_transp:
-  assumes a: "equivp R"
-  and b: "list_all2 R xs1 xs2"
-  and c: "list_all2 R xs2 xs3"
-  shows "list_all2 R xs1 xs3"
-  using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
-  apply(induct rule: list_induct3)
-  apply(simp_all)
-  apply(auto intro: equivp_transp[OF a])
-  done
+lemma list_symp:
+  assumes "symp R"
+  shows "symp (list_all2 R)"
+proof (rule sympI)
+  from assms have *: "\<And>xs ys. R xs ys \<Longrightarrow> R ys xs" by (rule sympE)
+  fix xs ys
+  assume "list_all2 R xs ys"
+  then show "list_all2 R ys xs"
+    by (induct xs ys rule: list_induct2') (simp_all add: *)
+qed
 
-lemma list_equivp[quot_equiv]:
-  assumes a: "equivp R"
-  shows "equivp (list_all2 R)"
-  apply (intro equivpI)
-  unfolding reflp_def symp_def transp_def
-  apply(simp add: list_all2_reflp[OF a])
-  apply(blast intro: list_all2_symp[OF a])
-  apply(blast intro: list_all2_transp[OF a])
-  done
+lemma list_transp:
+  assumes "transp R"
+  shows "transp (list_all2 R)"
+proof (rule transpI)
+  from assms have *: "\<And>xs ys zs. R xs ys \<Longrightarrow> R ys zs \<Longrightarrow> R xs zs" by (rule transpE)
+  fix xs ys zs
+  assume A: "list_all2 R xs ys" "list_all2 R ys zs"
+  then have "length xs = length ys" "length ys = length zs" by (blast dest: list_all2_lengthD)+
+  then show "list_all2 R xs zs" using A
+    by (induct xs ys zs rule: list_induct3) (auto intro: *)
+qed
 
-lemma list_all2_rel:
-  assumes q: "Quotient R Abs Rep"
-  shows "list_all2 R r s = (list_all2 R r r \<and> list_all2 R s s \<and> (map Abs r = map Abs s))"
-  apply(induct r s rule: list_induct2')
-  apply(simp_all)
-  using Quotient_rel[OF q]
-  apply(metis)
-  done
+lemma list_equivp [quot_equiv]:
+  "equivp R \<Longrightarrow> equivp (list_all2 R)"
+  by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
 
-lemma list_quotient[quot_thm]:
-  assumes q: "Quotient R Abs Rep"
+lemma list_quotient [quot_thm]:
+  assumes "Quotient R Abs Rep"
   shows "Quotient (list_all2 R) (map Abs) (map Rep)"
-  unfolding Quotient_def
-  apply(subst split_list_all)
-  apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
-  apply(intro conjI allI)
-  apply(induct_tac a)
-  apply(simp_all add: Quotient_rep_reflp[OF q])
-  apply(rule list_all2_rel[OF q])
-  done
+proof (rule QuotientI)
+  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+  then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
+next
+  from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
+  then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
+    by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
+next
+  fix xs ys
+  from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel)
+  then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> map Abs xs = map Abs ys"
+    by (induct xs ys rule: list_induct2') auto
+qed
 
-lemma cons_prs[quot_preserve]:
+lemma cons_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
   by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
 
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
   by auto
 
-lemma nil_prs[quot_preserve]:
+lemma nil_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "map Abs [] = []"
   by simp
 
-lemma nil_rsp[quot_respect]:
+lemma nil_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "list_all2 R [] []"
   by simp
@@ -109,7 +111,7 @@
   by (induct l)
      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma map_prs[quot_preserve]:
+lemma map_prs [quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
@@ -117,8 +119,7 @@
   by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
     (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-
-lemma map_rsp[quot_respect]:
+lemma map_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
@@ -137,7 +138,7 @@
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
   by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma foldr_prs[quot_preserve]:
+lemma foldr_prs [quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
@@ -151,8 +152,7 @@
   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
   by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-
-lemma foldl_prs[quot_preserve]:
+lemma foldl_prs [quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
@@ -217,11 +217,11 @@
     qed
   qed
 
-lemma[quot_respect]:
+lemma [quot_respect]:
   "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
   by (simp add: list_all2_rsp fun_rel_def)
 
-lemma[quot_preserve]:
+lemma [quot_preserve]:
   assumes a: "Quotient R abs1 rep1"
   shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
   apply (simp add: fun_eq_iff)
@@ -230,19 +230,11 @@
   apply (simp_all add: Quotient_abs_rep[OF a])
   done
 
-lemma[quot_preserve]:
+lemma [quot_preserve]:
   assumes a: "Quotient R abs1 rep1"
   shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
   by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
 
-lemma list_all2_eq[id_simps]:
-  shows "(list_all2 (op =)) = (op =)"
-  unfolding fun_eq_iff
-  apply(rule allI)+
-  apply(induct_tac x xa rule: list_induct2')
-  apply(simp_all)
-  done
-
 lemma list_all2_find_element:
   assumes a: "x \<in> set a"
   and b: "list_all2 R a b"
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -18,64 +18,73 @@
 
 declare [[map option = (Option.map, option_rel)]]
 
-text {* should probably be in Option.thy *}
-lemma split_option_all:
-  shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
-  apply(auto)
-  apply(case_tac x)
-  apply(simp_all)
+lemma option_rel_unfold:
+  "option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
+    | (Some x, Some y) \<Rightarrow> R x y
+    | _ \<Rightarrow> False)"
+  by (cases x) (cases y, simp_all)+
+
+lemma option_rel_map1:
+  "option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f x)) x y"
+  by (simp add: option_rel_unfold split: option.split)
+
+lemma option_rel_map2:
+  "option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f y)) x y"
+  by (simp add: option_rel_unfold split: option.split)
+
+lemma option_map_id [id_simps]:
+  "Option.map id = id"
+  by (simp add: id_def Option.map.identity fun_eq_iff)
+
+lemma option_rel_eq [id_simps]:
+  "option_rel (op =) = (op =)"
+  by (simp add: option_rel_unfold fun_eq_iff split: option.split)
+
+lemma option_reflp:
+  "reflp R \<Longrightarrow> reflp (option_rel R)"
+  by (auto simp add: option_rel_unfold split: option.splits intro!: reflpI elim: reflpE)
+
+lemma option_symp:
+  "symp R \<Longrightarrow> symp (option_rel R)"
+  by (auto simp add: option_rel_unfold split: option.splits intro!: sympI elim: sympE)
+
+lemma option_transp:
+  "transp R \<Longrightarrow> transp (option_rel R)"
+  by (auto simp add: option_rel_unfold split: option.splits intro!: transpI elim: transpE)
+
+lemma option_equivp [quot_equiv]:
+  "equivp R \<Longrightarrow> equivp (option_rel R)"
+  by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
+
+lemma option_quotient [quot_thm]:
+  assumes "Quotient R Abs Rep"
+  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
+  apply (rule QuotientI)
+  apply (simp_all add: Option.map.compositionality Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
+  using Quotient_rel [OF assms]
+  apply (simp add: option_rel_unfold split: option.split)
   done
 
-lemma option_quotient[quot_thm]:
-  assumes q: "Quotient R Abs Rep"
-  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
-  unfolding Quotient_def
-  apply(simp add: split_option_all)
-  apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
-  using q
-  unfolding Quotient_def
-  apply(blast)
-  done
-
-lemma option_equivp[quot_equiv]:
-  assumes a: "equivp R"
-  shows "equivp (option_rel R)"
-  apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
-  apply(simp_all add: split_option_all)
-  apply(blast intro: equivp_reflp[OF a])
-  apply(blast intro: equivp_symp[OF a])
-  apply(blast intro: equivp_transp[OF a])
-  done
-
-lemma option_None_rsp[quot_respect]:
+lemma option_None_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "option_rel R None None"
   by simp
 
-lemma option_Some_rsp[quot_respect]:
+lemma option_Some_rsp [quot_respect]:
   assumes q: "Quotient R Abs Rep"
   shows "(R ===> option_rel R) Some Some"
   by auto
 
-lemma option_None_prs[quot_preserve]:
+lemma option_None_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "Option.map Abs None = None"
   by simp
 
-lemma option_Some_prs[quot_preserve]:
+lemma option_Some_prs [quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> Option.map Abs) Some = Some"
   apply(simp add: fun_eq_iff)
   apply(simp add: Quotient_abs_rep[OF q])
   done
 
-lemma option_map_id[id_simps]:
-  shows "Option.map id = id"
-  by (simp add: fun_eq_iff split_option_all)
-
-lemma option_rel_eq[id_simps]:
-  shows "option_rel (op =) = (op =)"
-  by (simp add: fun_eq_iff split_option_all)
-
 end
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -19,38 +19,39 @@
   "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
   by (simp add: prod_rel_def)
 
-lemma prod_equivp[quot_equiv]:
-  assumes a: "equivp R1"
-  assumes b: "equivp R2"
+lemma map_pair_id [id_simps]:
+  shows "map_pair id id = id"
+  by (simp add: fun_eq_iff)
+
+lemma prod_rel_eq [id_simps]:
+  shows "prod_rel (op =) (op =) = (op =)"
+  by (simp add: fun_eq_iff)
+
+lemma prod_equivp [quot_equiv]:
+  assumes "equivp R1"
+  assumes "equivp R2"
   shows "equivp (prod_rel R1 R2)"
-  apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
-  apply(simp_all add: split_paired_all prod_rel_def)
-  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
-  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
-  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
+  using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
+
+lemma prod_quotient [quot_thm]:
+  assumes "Quotient R1 Abs1 Rep1"
+  assumes "Quotient R2 Abs2 Rep2"
+  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
+  apply (rule QuotientI)
+  apply (simp add: map_pair.compositionality map_pair.identity
+     Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
+  apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
+  using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
+  apply (auto simp add: split_paired_all)
   done
 
-lemma prod_quotient[quot_thm]:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  assumes q2: "Quotient R2 Abs2 Rep2"
-  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
-  unfolding Quotient_def
-  apply(simp add: split_paired_all)
-  apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
-  apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
-  using q1 q2
-  unfolding Quotient_def
-  apply(blast)
-  done
-
-lemma Pair_rsp[quot_respect]:
+lemma Pair_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
   by (auto simp add: prod_rel_def)
 
-lemma Pair_prs[quot_preserve]:
+lemma Pair_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
@@ -58,35 +59,35 @@
   apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   done
 
-lemma fst_rsp[quot_respect]:
+lemma fst_rsp [quot_respect]:
   assumes "Quotient R1 Abs1 Rep1"
   assumes "Quotient R2 Abs2 Rep2"
   shows "(prod_rel R1 R2 ===> R1) fst fst"
   by auto
 
-lemma fst_prs[quot_preserve]:
+lemma fst_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
 
-lemma snd_rsp[quot_respect]:
+lemma snd_rsp [quot_respect]:
   assumes "Quotient R1 Abs1 Rep1"
   assumes "Quotient R2 Abs2 Rep2"
   shows "(prod_rel R1 R2 ===> R2) snd snd"
   by auto
 
-lemma snd_prs[quot_preserve]:
+lemma snd_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
 
-lemma split_rsp[quot_respect]:
+lemma split_rsp [quot_respect]:
   shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
   by (auto intro!: fun_relI elim!: fun_relE)
 
-lemma split_prs[quot_preserve]:
+lemma split_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
@@ -111,12 +112,4 @@
 
 declare Pair_eq[quot_preserve]
 
-lemma map_pair_id[id_simps]:
-  shows "map_pair id id = id"
-  by (simp add: fun_eq_iff)
-
-lemma prod_rel_eq[id_simps]:
-  shows "prod_rel (op =) (op =) = (op =)"
-  by (simp add: fun_eq_iff)
-
 end
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -18,53 +18,68 @@
 
 declare [[map sum = (sum_map, sum_rel)]]
 
+lemma sum_rel_unfold:
+  "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+    | (Inr x, Inr y) \<Rightarrow> R2 x y
+    | _ \<Rightarrow> False)"
+  by (cases x) (cases y, simp_all)+
 
-text {* should probably be in @{theory Sum_Type} *}
-lemma split_sum_all:
-  shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
-  apply(auto)
-  apply(case_tac x)
-  apply(simp_all)
-  done
+lemma sum_rel_map1:
+  "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
+  by (simp add: sum_rel_unfold split: sum.split)
+
+lemma sum_rel_map2:
+  "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
+  by (simp add: sum_rel_unfold split: sum.split)
+
+lemma sum_map_id [id_simps]:
+  "sum_map id id = id"
+  by (simp add: id_def sum_map.identity fun_eq_iff)
 
-lemma sum_equivp[quot_equiv]:
-  assumes a: "equivp R1"
-  assumes b: "equivp R2"
-  shows "equivp (sum_rel R1 R2)"
-  apply(rule equivpI)
-  unfolding reflp_def symp_def transp_def
-  apply(simp_all add: split_sum_all)
-  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
-  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
-  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
-  done
+lemma sum_rel_eq [id_simps]:
+  "sum_rel (op =) (op =) = (op =)"
+  by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
+
+lemma sum_reflp:
+  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
+  by (auto simp add: sum_rel_unfold split: sum.splits intro!: reflpI elim: reflpE)
 
-lemma sum_quotient[quot_thm]:
+lemma sum_symp:
+  "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
+  by (auto simp add: sum_rel_unfold split: sum.splits intro!: sympI elim: sympE)
+
+lemma sum_transp:
+  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
+  by (auto simp add: sum_rel_unfold split: sum.splits intro!: transpI elim: transpE)
+
+lemma sum_equivp [quot_equiv]:
+  "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
+  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
+  
+lemma sum_quotient [quot_thm]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
-  unfolding Quotient_def
-  apply(simp add: split_sum_all)
-  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
-  apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
-  using q1 q2
-  unfolding Quotient_def
-  apply(blast)+
+  apply (rule QuotientI)
+  apply (simp_all add: sum_map.compositionality sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
+    Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
+  using Quotient_rel [OF q1] Quotient_rel [OF q2]
+  apply (simp add: sum_rel_unfold split: sum.split)
   done
 
-lemma sum_Inl_rsp[quot_respect]:
+lemma sum_Inl_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> sum_rel R1 R2) Inl Inl"
   by auto
 
-lemma sum_Inr_rsp[quot_respect]:
+lemma sum_Inr_rsp [quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(R2 ===> sum_rel R1 R2) Inr Inr"
   by auto
 
-lemma sum_Inl_prs[quot_preserve]:
+lemma sum_Inl_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
@@ -72,7 +87,7 @@
   apply(simp add: Quotient_abs_rep[OF q1])
   done
 
-lemma sum_Inr_prs[quot_preserve]:
+lemma sum_Inr_prs [quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
@@ -80,12 +95,4 @@
   apply(simp add: Quotient_abs_rep[OF q2])
   done
 
-lemma sum_map_id[id_simps]:
-  shows "sum_map id id = id"
-  by (simp add: fun_eq_iff split_sum_all)
-
-lemma sum_rel_eq[id_simps]:
-  shows "sum_rel (op =) (op =) = (op =)"
-  by (simp add: fun_eq_iff split_sum_all)
-
 end
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -62,7 +62,7 @@
 by (simp add: starrel_def)
 
 lemma equiv_starrel: "equiv UNIV starrel"
-proof (rule equiv.intro)
+proof (rule equivI)
   show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
   show "trans starrel" by (auto intro: transI elim!: ultra)
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Predicate.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -363,6 +363,44 @@
 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   "single_valuedP r == single_valued {(x, y). r x y}"
 
+(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
+
+definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
+
+definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "symp r \<longleftrightarrow> sym {(x, y). r x y}"
+
+definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "transp r \<longleftrightarrow> trans {(x, y). r x y}"
+
+lemma reflpI:
+  "(\<And>x. r x x) \<Longrightarrow> reflp r"
+  by (auto intro: refl_onI simp add: reflp_def)
+
+lemma reflpE:
+  assumes "reflp r"
+  obtains "r x x"
+  using assms by (auto dest: refl_onD simp add: reflp_def)
+
+lemma sympI:
+  "(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r"
+  by (auto intro: symI simp add: symp_def)
+
+lemma sympE:
+  assumes "symp r" and "r x y"
+  obtains "r y x"
+  using assms by (auto dest: symD simp add: symp_def)
+
+lemma transpI:
+  "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
+  by (auto intro: transI simp add: transp_def)
+  
+lemma transpE:
+  assumes "transp r" and "r x y" and "r y z"
+  obtains "r x z"
+  using assms by (auto dest: transD simp add: transp_def)
+
 
 subsection {* Predicates as enumerations *}
 
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Quotient.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -14,131 +14,15 @@
   ("Tools/Quotient/quotient_tacs.ML")
 begin
 
-
 text {*
   Basic definition for equivalence relations
   that are represented by predicates.
 *}
 
-definition
-  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
-
-lemma refl_reflp:
-  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: refl_on_def reflp_def)
-
-definition
-  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
-
-lemma sym_symp:
-  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: sym_def symp_def)
-
-definition
-  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
-
-lemma trans_transp:
-  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
-  by (auto simp add: trans_def transp_def)
-
-definition
-  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
-
-lemma equivp_reflp_symp_transp:
-  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
-  unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
-  by blast
-
-lemma equiv_equivp:
-  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
-  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
-
-lemma equivp_reflp:
-  shows "equivp E \<Longrightarrow> E x x"
-  by (simp only: equivp_reflp_symp_transp reflp_def)
-
-lemma equivp_symp:
-  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
-  by (simp add: equivp_def)
-
-lemma equivp_transp:
-  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
-  by (simp add: equivp_def)
-
-lemma equivpI:
-  assumes "reflp R" "symp R" "transp R"
-  shows "equivp R"
-  using assms by (simp add: equivp_reflp_symp_transp)
-
-lemma identity_equivp:
-  shows "equivp (op =)"
-  unfolding equivp_def
-  by auto
-
-text {* Partial equivalences *}
-
-definition
-  "part_equivp E \<longleftrightarrow> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
-
-lemma equivp_implies_part_equivp:
-  assumes a: "equivp E"
-  shows "part_equivp E"
-  using a
-  unfolding equivp_def part_equivp_def
-  by auto
-
-lemma part_equivp_symp:
-  assumes e: "part_equivp R"
-  and a: "R x y"
-  shows "R y x"
-  using e[simplified part_equivp_def] a
-  by (metis)
-
-lemma part_equivp_typedef:
-  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
-  unfolding part_equivp_def mem_def
-  apply clarify
-  apply (intro exI)
-  apply (rule conjI)
-  apply assumption
-  apply (rule refl)
-  done
-
-lemma part_equivp_refl_symp_transp:
-  shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
-proof
-  assume "part_equivp E"
-  then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
-  unfolding part_equivp_def symp_def transp_def
-  by metis
-next
-  assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
-  then have b: "(\<forall>x y. E x y \<longrightarrow> E y x)" and c: "(\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
-    unfolding symp_def transp_def by (metis, metis)
-  have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
-  proof (intro allI iffI conjI)
-    fix x y
-    assume d: "E x y"
-    then show "E x x" using b c by metis
-    show "E y y" using b c d by metis
-    show "E x = E y" unfolding fun_eq_iff using b c d by metis
-  next
-    fix x y
-    assume "E x x \<and> E y y \<and> E x = E y"
-    then show "E x y" using b c by metis
-  qed
-  then show "part_equivp E" unfolding part_equivp_def using a by metis
-qed
-
-lemma part_equivpI:
-  assumes "\<exists>x. R x x" "symp R" "transp R"
-  shows "part_equivp R"
-  using assms by (simp add: part_equivp_refl_symp_transp)
-
 text {* Composition of Relations *}
 
 abbreviation
-  rel_conj (infixr "OOO" 75)
+  rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
 where
   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
 
@@ -169,16 +53,16 @@
 definition
   fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
 where
-  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 
 lemma fun_relI [intro]:
-  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
-  shows "(E1 ===> E2) f g"
+  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
   using assms by (simp add: fun_rel_def)
 
 lemma fun_relE:
-  assumes "(E1 ===> E2) f g" and "E1 x y"
-  obtains "E2 (f x) (g y)"
+  assumes "(R1 ===> R2) f g" and "R1 x y"
+  obtains "R2 (f x) (g y)"
   using assms by (simp add: fun_rel_def)
 
 lemma fun_rel_eq:
@@ -189,34 +73,41 @@
 subsection {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<longleftrightarrow>
-     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
-     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+  "Quotient R Abs Rep \<longleftrightarrow>
+     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
+     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
+
+lemma QuotientI:
+  assumes "\<And>a. Abs (Rep a) = a"
+    and "\<And>a. R (Rep a) (Rep a)"
+    and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
+  shows "Quotient R Abs Rep"
+  using assms unfolding Quotient_def by blast
 
 lemma Quotient_abs_rep:
-  assumes a: "Quotient E Abs Rep"
+  assumes a: "Quotient R Abs Rep"
   shows "Abs (Rep a) = a"
   using a
   unfolding Quotient_def
   by simp
 
 lemma Quotient_rep_reflp:
-  assumes a: "Quotient E Abs Rep"
-  shows "E (Rep a) (Rep a)"
+  assumes a: "Quotient R Abs Rep"
+  shows "R (Rep a) (Rep a)"
   using a
   unfolding Quotient_def
   by blast
 
 lemma Quotient_rel:
-  assumes a: "Quotient E Abs Rep"
-  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+  assumes a: "Quotient R Abs Rep"
+  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
   using a
   unfolding Quotient_def
   by blast
 
 lemma Quotient_rel_rep:
   assumes a: "Quotient R Abs Rep"
-  shows "R (Rep a) (Rep b) = (a = b)"
+  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
   using a
   unfolding Quotient_def
   by metis
@@ -228,22 +119,20 @@
   by blast
 
 lemma Quotient_rel_abs:
-  assumes a: "Quotient E Abs Rep"
-  shows "E r s \<Longrightarrow> Abs r = Abs s"
+  assumes a: "Quotient R Abs Rep"
+  shows "R r s \<Longrightarrow> Abs r = Abs s"
   using a unfolding Quotient_def
   by blast
 
 lemma Quotient_symp:
-  assumes a: "Quotient E Abs Rep"
-  shows "symp E"
-  using a unfolding Quotient_def symp_def
-  by metis
+  assumes a: "Quotient R Abs Rep"
+  shows "symp R"
+  using a unfolding Quotient_def using sympI by metis
 
 lemma Quotient_transp:
-  assumes a: "Quotient E Abs Rep"
-  shows "transp E"
-  using a unfolding Quotient_def transp_def
-  by metis
+  assumes a: "Quotient R Abs Rep"
+  shows "transp R"
+  using a unfolding Quotient_def using transpI by metis
 
 lemma identity_quotient:
   shows "Quotient (op =) id id"
@@ -291,8 +180,7 @@
   and     a: "R xa xb" "R ya yb"
   shows "R xa ya = R xb yb"
   using a Quotient_symp[OF q] Quotient_transp[OF q]
-  unfolding symp_def transp_def
-  by blast
+  by (blast elim: sympE transpE)
 
 lemma lambda_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -300,7 +188,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by (simp add:)
+  by simp
 
 lemma lambda_prs1:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -308,7 +196,7 @@
   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   unfolding fun_eq_iff
   using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-  by (simp add:)
+  by simp
 
 lemma rep_abs_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -392,9 +280,7 @@
   apply(simp add: in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
-  apply(simp add: reflp_def)
-  apply(simp)
-  apply(simp)
+  apply (auto elim: equivpE reflpE)
   done
 
 lemma bex_reg_eqv_range:
@@ -406,7 +292,7 @@
   apply(simp add: Respects_def in_respects fun_rel_def)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
-  apply(simp add: reflp_def)
+  apply (auto elim: equivpE reflpE)
   done
 
 (* Next four lemmas are unused *)
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -19,11 +19,21 @@
 where
   [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
 
+lemma list_eq_reflp:
+  "reflp list_eq"
+  by (auto intro: reflpI)
+
+lemma list_eq_symp:
+  "symp list_eq"
+  by (auto intro: sympI)
+
+lemma list_eq_transp:
+  "transp list_eq"
+  by (auto intro: transpI)
+
 lemma list_eq_equivp:
-  shows "equivp list_eq"
-  unfolding equivp_reflp_symp_transp
-  unfolding reflp_def symp_def transp_def
-  by auto
+  "equivp list_eq"
+  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)
 
 text {* The @{text fset} type *}
 
@@ -141,7 +151,7 @@
       \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
     then have s: "(list_all2 R OOO op \<approx>) s s" by simp
     have d: "map Abs r \<approx> map Abs s"
-      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
     have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
       by (rule map_list_eq_cong[OF d])
     have y: "list_all2 R (map Rep (map Abs s)) s"
@@ -267,8 +277,11 @@
 proof (rule fun_relI, elim pred_compE)
   fix a b ba bb
   assume a: "list_all2 op \<approx> a ba"
+  with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
   assume b: "ba \<approx> bb"
+  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
   assume c: "list_all2 op \<approx> bb b"
+  with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 
   proof
     fix x
@@ -278,9 +291,6 @@
       show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
     next
       assume e: "\<exists>xa\<in>set b. x \<in> set xa"
-      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
-      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
-      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
       show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
     qed
   qed
@@ -288,7 +298,6 @@
 qed
 
 
-
 section {* Quotient definitions for fsets *}
 
 
@@ -474,7 +483,7 @@
   assumes a: "reflp R"
   and b: "list_all2 R l r"
   shows "list_all2 R (z @ l) (z @ r)"
-  by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
+  using a b by (induct z) (auto elim: reflpE)
 
 lemma append_rsp2_pre0:
   assumes a:"list_all2 op \<approx> x x'"
@@ -489,23 +498,14 @@
   apply (rule list_all2_refl'[OF list_eq_equivp])
   apply (simp_all del: list_eq_def)
   apply (rule list_all2_app_l)
-  apply (simp_all add: reflp_def)
+  apply (simp_all add: reflpI)
   done
 
 lemma append_rsp2_pre:
-  assumes a:"list_all2 op \<approx> x x'"
-  and     b: "list_all2 op \<approx> z z'"
+  assumes "list_all2 op \<approx> x x'"
+    and "list_all2 op \<approx> z z'"
   shows "list_all2 op \<approx> (x @ z) (x' @ z')"
-  apply (rule list_all2_transp[OF fset_equivp])
-  apply (rule append_rsp2_pre0)
-  apply (rule a)
-  using b apply (induct z z' rule: list_induct2')
-  apply (simp_all only: append_Nil2)
-  apply (rule list_all2_refl'[OF list_eq_equivp])
-  apply simp_all
-  apply (rule append_rsp2_pre1)
-  apply simp
-  done
+  using assms by (rule list_all2_appendI)
 
 lemma append_rsp2 [quot_respect]:
   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Quotient_Examples/Quotient_Message.thy
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -36,16 +36,16 @@
 
 theorem equiv_msgrel: "equivp msgrel"
 proof (rule equivpI)
-  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
-  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
-  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+  show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
+  show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
+  show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
 qed
 
 subsection{*Some Functions on the Free Algebra*}
 
 subsubsection{*The Set of Nonces*}
 
-fun
+primrec
   freenonces :: "freemsg \<Rightarrow> nat set"
 where
   "freenonces (NONCE N) = {N}"
@@ -62,7 +62,7 @@
 
 text{*A function to return the left part of the top pair in a message.  It will
 be lifted to the initial algrebra, to serve as an example of that process.*}
-fun
+primrec
   freeleft :: "freemsg \<Rightarrow> freemsg"
 where
   "freeleft (NONCE N) = NONCE N"
@@ -75,7 +75,7 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeleft_aux:
   shows "freeleft U \<sim> freeleft U"
-  by (induct rule: freeleft.induct) (auto)
+  by (fact msgrel_refl)
 
 theorem msgrel_imp_eqv_freeleft:
   assumes a: "U \<sim> V"
@@ -86,7 +86,7 @@
 subsubsection{*The Right Projection*}
 
 text{*A function to return the right part of the top pair in a message.*}
-fun
+primrec
   freeright :: "freemsg \<Rightarrow> freemsg"
 where
   "freeright (NONCE N) = NONCE N"
@@ -99,7 +99,7 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeright_aux:
   shows "freeright U \<sim> freeright U"
-  by (induct rule: freeright.induct) (auto)
+  by (fact msgrel_refl)
 
 theorem msgrel_imp_eqv_freeright:
   assumes a: "U \<sim> V"
@@ -110,7 +110,7 @@
 subsubsection{*The Discriminator for Constructors*}
 
 text{*A function to distinguish nonces, mpairs and encryptions*}
-fun
+primrec
   freediscrim :: "freemsg \<Rightarrow> int"
 where
    "freediscrim (NONCE N) = 0"
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Rat.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -44,7 +44,7 @@
 qed
   
 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
-  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
+  by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
 
 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
@@ -146,7 +146,7 @@
 lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
 proof -
   have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
-    by (simp add: congruent_def)
+    by (simp add: congruent_def split_paired_all)
   then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
 qed
 
@@ -781,7 +781,7 @@
 
 lemma of_rat_congruent:
   "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
-apply (rule congruent.intro)
+apply (rule congruentI)
 apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
 apply (simp only: of_int_mult [symmetric])
 done
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/RealDef.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -14,8 +14,8 @@
 text {*
   This theory contains a formalization of the real numbers as
   equivalence classes of Cauchy sequences of rationals.  See
-  \url{HOL/ex/Dedekind_Real.thy} for an alternative construction
-  using Dedekind cuts.
+  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
+  construction using Dedekind cuts.
 *}
 
 subsection {* Preliminary lemmas *}
@@ -324,7 +324,7 @@
 
 lemma equiv_realrel: "equiv {X. cauchy X} realrel"
   using refl_realrel sym_realrel trans_realrel
-  by (rule equiv.intro)
+  by (rule equivI)
 
 subsection {* The field of real numbers *}
 
@@ -358,7 +358,7 @@
   apply (simp add: quotientI X)
   apply (rule the_equality)
   apply clarsimp
-  apply (erule congruent.congruent [OF f])
+  apply (erule congruentD [OF f])
   apply (erule bspec)
   apply simp
   apply (rule refl_onD [OF refl_realrel])
@@ -370,14 +370,14 @@
   assumes X: "cauchy X" and Y: "cauchy Y"
   shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
  apply (subst real_case_1 [OF _ X])
-  apply (rule congruent.intro)
+  apply (rule congruentI)
   apply (subst real_case_1 [OF _ Y])
    apply (rule congruent2_implies_congruent [OF equiv_realrel f])
    apply (simp add: realrel_def)
   apply (subst real_case_1 [OF _ Y])
    apply (rule congruent2_implies_congruent [OF equiv_realrel f])
    apply (simp add: realrel_def)
-  apply (erule congruent2.congruent2 [OF f])
+  apply (erule congruent2D [OF f])
   apply (rule refl_onD [OF refl_realrel])
   apply (simp add: Y)
   apply (rule real_case_1 [OF _ Y])
@@ -416,7 +416,7 @@
 
 lemma minus_respects_realrel:
   "(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
-proof (rule congruent.intro)
+proof (rule congruentI)
   fix X Y assume "(X, Y) \<in> realrel"
   hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
     unfolding realrel_def by simp_all
@@ -492,7 +492,7 @@
 lemma inverse_respects_realrel:
   "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
     (is "?inv respects realrel")
-proof (rule congruent.intro)
+proof (rule congruentI)
   fix X Y assume "(X, Y) \<in> realrel"
   hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
     unfolding realrel_def by simp_all
@@ -622,7 +622,7 @@
   assumes sym: "sym r"
   assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
   shows "P respects r"
-apply (rule congruent.intro)
+apply (rule congruentI)
 apply (rule iffI)
 apply (erule (1) P)
 apply (erule (1) P [OF symD [OF sym]])
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/SEQ.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -221,15 +221,7 @@
 lemma LIMSEQ_unique:
   fixes a b :: "'a::metric_space"
   shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
-apply (rule ccontr)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff)
-apply (clarify, rename_tac M N)
-apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp)
-apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b")
-apply (erule le_less_trans, rule add_strict_mono, simp, simp)
-apply (subst dist_commute, rule dist_triangle)
-done
+by (drule (1) tendsto_dist, simp add: LIMSEQ_const_iff)
 
 lemma (in bounded_linear) LIMSEQ:
   "X ----> a \<Longrightarrow> (\<lambda>n. f (X n)) ----> f a"
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/Word/Word.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -184,13 +184,13 @@
   "word_pred a = word_of_int (Int.pred (uint a))"
 
 definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
-  "a udvd b == EX n>=0. uint b = n * uint a"
+  "a udvd b = (EX n>=0. uint b = n * uint a)"
 
 definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
-  "a <=s b == sint a <= sint b"
+  "a <=s b = (sint a <= sint b)"
 
 definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
-  "(x <s y) == (x <=s y & x ~= y)"
+  "(x <s y) = (x <=s y & x ~= y)"
 
 
 
@@ -245,76 +245,76 @@
   by (simp only: word_msb_def Min_def)
 
 definition setBit :: "'a :: len0 word => nat => 'a word" where 
-  "setBit w n == set_bit w n True"
+  "setBit w n = set_bit w n True"
 
 definition clearBit :: "'a :: len0 word => nat => 'a word" where
-  "clearBit w n == set_bit w n False"
+  "clearBit w n = set_bit w n False"
 
 
 subsection "Shift operations"
 
 definition sshiftr1 :: "'a :: len word => 'a word" where 
-  "sshiftr1 w == word_of_int (bin_rest (sint w))"
+  "sshiftr1 w = word_of_int (bin_rest (sint w))"
 
 definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
-  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
+  "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
 
 definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
-  "w >>> n == (sshiftr1 ^^ n) w"
+  "w >>> n = (sshiftr1 ^^ n) w"
 
 definition mask :: "nat => 'a::len word" where
-  "mask n == (1 << n) - 1"
+  "mask n = (1 << n) - 1"
 
 definition revcast :: "'a :: len0 word => 'b :: len0 word" where
-  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+  "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
 
 definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
-  "slice1 n w == of_bl (takefill False n (to_bl w))"
+  "slice1 n w = of_bl (takefill False n (to_bl w))"
 
 definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
-  "slice n w == slice1 (size w - n) w"
+  "slice n w = slice1 (size w - n) w"
 
 
 subsection "Rotation"
 
 definition rotater1 :: "'a list => 'a list" where
-  "rotater1 ys == 
-    case ys of [] => [] | x # xs => last ys # butlast ys"
+  "rotater1 ys = 
+    (case ys of [] => [] | x # xs => last ys # butlast ys)"
 
 definition rotater :: "nat => 'a list => 'a list" where
-  "rotater n == rotater1 ^^ n"
+  "rotater n = rotater1 ^^ n"
 
 definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
-  "word_rotr n w == of_bl (rotater n (to_bl w))"
+  "word_rotr n w = of_bl (rotater n (to_bl w))"
 
 definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
-  "word_rotl n w == of_bl (rotate n (to_bl w))"
+  "word_rotl n w = of_bl (rotate n (to_bl w))"
 
 definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
-  "word_roti i w == if i >= 0 then word_rotr (nat i) w
-                    else word_rotl (nat (- i)) w"
+  "word_roti i w = (if i >= 0 then word_rotr (nat i) w
+                    else word_rotl (nat (- i)) w)"
 
 
 subsection "Split and cat operations"
 
 definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
-  "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
+  "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
 
 definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
-  "word_split a == 
-   case bin_split (len_of TYPE ('c)) (uint a) of 
-     (u, v) => (word_of_int u, word_of_int v)"
+  "word_split a = 
+   (case bin_split (len_of TYPE ('c)) (uint a) of 
+     (u, v) => (word_of_int u, word_of_int v))"
 
 definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
-  "word_rcat ws == 
+  "word_rcat ws = 
   word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
 
 definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
-  "word_rsplit w == 
+  "word_rsplit w = 
   map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
 
 definition max_word :: "'a::len word" -- "Largest representable machine integer." where
-  "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
+  "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
 
 primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
   "of_bool False = 0"
@@ -337,7 +337,7 @@
 lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded 
   atLeast_def lessThan_def Collect_conj_eq [symmetric]]
   
-lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}"
+lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
   unfolding atLeastLessThan_alt by auto
 
 lemma 
@@ -390,7 +390,7 @@
   unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
 
 lemma bintr_uint': 
-  "n >= size w ==> bintrunc n (uint w) = uint w"
+  "n >= size w \<Longrightarrow> bintrunc n (uint w) = uint w"
   apply (unfold word_size)
   apply (subst word_ubin.norm_Rep [symmetric]) 
   apply (simp only: bintrunc_bintrunc_min word_size)
@@ -398,7 +398,7 @@
   done
 
 lemma wi_bintr': 
-  "wb = word_of_int bin ==> n >= size wb ==> 
+  "wb = word_of_int bin \<Longrightarrow> n >= size wb \<Longrightarrow> 
     word_of_int (bintrunc n bin) = wb"
   unfolding word_size
   by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
@@ -446,8 +446,9 @@
 
 lemmas td_sint = word_sint.td
 
-lemma word_number_of_alt: "number_of b == word_of_int (number_of b)"
-  unfolding word_number_of_def by (simp add: number_of_eq)
+lemma word_number_of_alt [code_unfold_post]:
+  "number_of b = word_of_int (number_of b)"
+  by (simp add: number_of_eq word_number_of_def)
 
 lemma word_no_wi: "number_of = word_of_int"
   by (auto simp: word_number_of_def intro: ext)
@@ -483,7 +484,7 @@
   sint_sbintrunc [simp] 
   unat_bintrunc [simp]
 
-lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w"
+lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
   apply (unfold word_size)
   apply (rule word_uint.Rep_eqD)
   apply (rule box_equals)
@@ -508,13 +509,13 @@
   iffD2 [OF linorder_not_le uint_m2p_neg, standard]
 
 lemma lt2p_lem:
-  "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n"
+  "len_of TYPE('a) <= n \<Longrightarrow> uint (w :: 'a :: len0 word) < 2 ^ n"
   by (rule xtr8 [OF _ uint_lt2p]) simp
 
 lemmas uint_le_0_iff [simp] = 
   uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard]
 
-lemma uint_nat: "uint w == int (unat w)"
+lemma uint_nat: "uint w = int (unat w)"
   unfolding unat_def by auto
 
 lemma uint_number_of:
@@ -523,7 +524,7 @@
   by (simp only: int_word_uint)
 
 lemma unat_number_of: 
-  "bin_sign b = Int.Pls ==> 
+  "bin_sign b = Int.Pls \<Longrightarrow> 
   unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
   apply (unfold unat_def)
   apply (clarsimp simp only: uint_number_of)
@@ -590,7 +591,7 @@
 
 lemma word_eqI [rule_format] : 
   fixes u :: "'a::len0 word"
-  shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v"
+  shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
   apply (rule test_bit_eq_iff [THEN iffD1])
   apply (rule ext)
   apply (erule allE)
@@ -645,7 +646,7 @@
                   "{bl. length bl = len_of TYPE('a::len0)}"
   by (rule td_bl)
 
-lemma word_size_bl: "size w == size (to_bl w)"
+lemma word_size_bl: "size w = size (to_bl w)"
   unfolding word_size by auto
 
 lemma to_bl_use_of_bl:
@@ -658,7 +659,7 @@
 lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
   unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
 
-lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
+lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
   by auto
 
 lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
@@ -675,7 +676,7 @@
   done
 
 lemma of_bl_drop': 
-  "lend = length bl - len_of TYPE ('a :: len0) ==> 
+  "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow> 
     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   apply (unfold of_bl_def)
   apply (clarsimp simp add : trunc_bl2bin [symmetric])
@@ -693,7 +694,7 @@
   "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
   unfolding word_size of_bl_no by (simp add : word_number_of_def)
 
-lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
+lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   unfolding word_size to_bl_def by auto
 
 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
@@ -742,14 +743,14 @@
   may want these in reverse, but loop as simp rules, so use following *)
 
 lemma num_of_bintr':
-  "bintrunc (len_of TYPE('a :: len0)) a = b ==> 
+  "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow> 
     number_of a = (number_of b :: 'a word)"
   apply safe
   apply (rule_tac num_of_bintr [symmetric])
   done
 
 lemma num_of_sbintr':
-  "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==> 
+  "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow> 
     number_of a = (number_of b :: 'a word)"
   apply safe
   apply (rule_tac num_of_sbintr [symmetric])
@@ -769,7 +770,7 @@
 lemma scast_id: "scast w = w"
   unfolding scast_def by auto
 
-lemma ucast_bl: "ucast w == of_bl (to_bl w)"
+lemma ucast_bl: "ucast w = of_bl (to_bl w)"
   unfolding ucast_def of_bl_def uint_bl
   by (auto simp add : word_size)
 
@@ -799,7 +800,7 @@
 
 lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
 
-lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
+lemma down_cast_same': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"
   apply (unfold is_down)
   apply safe
   apply (rule ext)
@@ -809,7 +810,7 @@
   done
 
 lemma word_rev_tf': 
-  "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
+  "r = to_bl (of_bl bl) \<Longrightarrow> r = rev (takefill False (length r) (rev bl))"
   unfolding of_bl_def uint_bl
   by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
 
@@ -829,17 +830,17 @@
   done
 
 lemma ucast_up_app': 
-  "uc = ucast ==> source_size uc + n = target_size uc ==> 
+  "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow> 
     to_bl (uc w) = replicate n False @ (to_bl w)"
   by (auto simp add : source_size target_size to_bl_ucast)
 
 lemma ucast_down_drop': 
-  "uc = ucast ==> source_size uc = target_size uc + n ==> 
+  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
     to_bl (uc w) = drop n (to_bl w)"
   by (auto simp add : source_size target_size to_bl_ucast)
 
 lemma scast_down_drop': 
-  "sc = scast ==> source_size sc = target_size sc + n ==> 
+  "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> 
     to_bl (sc w) = drop n (to_bl w)"
   apply (subgoal_tac "sc = ucast")
    apply safe
@@ -850,7 +851,7 @@
   done
 
 lemma sint_up_scast': 
-  "sc = scast ==> is_up sc ==> sint (sc w) = sint w"
+  "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
   apply (unfold is_up)
   apply safe
   apply (simp add: scast_def word_sbin.eq_norm)
@@ -865,7 +866,7 @@
   done
 
 lemma uint_up_ucast':
-  "uc = ucast ==> is_up uc ==> uint (uc w) = uint w"
+  "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
   apply (unfold is_up)
   apply safe
   apply (rule bin_eqI)
@@ -881,18 +882,18 @@
 lemmas uint_up_ucast = refl [THEN uint_up_ucast']
 lemmas sint_up_scast = refl [THEN sint_up_scast']
 
-lemma ucast_up_ucast': "uc = ucast ==> is_up uc ==> ucast (uc w) = ucast w"
+lemma ucast_up_ucast': "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
   apply (simp (no_asm) add: ucast_def)
   apply (clarsimp simp add: uint_up_ucast)
   done
     
-lemma scast_up_scast': "sc = scast ==> is_up sc ==> scast (sc w) = scast w"
+lemma scast_up_scast': "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
   apply (simp (no_asm) add: scast_def)
   apply (clarsimp simp add: sint_up_scast)
   done
     
 lemma ucast_of_bl_up': 
-  "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
+  "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"
   by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
 
 lemmas ucast_up_ucast = refl [THEN ucast_up_ucast']
@@ -908,22 +909,22 @@
 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
 
 lemma up_ucast_surj:
-  "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==> 
+  "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 
    surj (ucast :: 'a word => 'b word)"
   by (rule surjI, erule ucast_up_ucast_id)
 
 lemma up_scast_surj:
-  "is_up (scast :: 'b::len word => 'a::len word) ==> 
+  "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 
    surj (scast :: 'a word => 'b word)"
   by (rule surjI, erule scast_up_scast_id)
 
 lemma down_scast_inj:
-  "is_down (scast :: 'b::len word => 'a::len word) ==> 
+  "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 
    inj_on (ucast :: 'a word => 'b word) A"
   by (rule inj_on_inverseI, erule scast_down_scast_id)
 
 lemma down_ucast_inj:
-  "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==> 
+  "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 
    inj_on (ucast :: 'a word => 'b word) A"
   by (rule inj_on_inverseI, erule ucast_down_ucast_id)
 
@@ -931,7 +932,7 @@
   by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
   
 lemma ucast_down_no': 
-  "uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
+  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
   apply (unfold word_number_of_def is_down)
   apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
@@ -940,7 +941,7 @@
     
 lemmas ucast_down_no = ucast_down_no' [OF refl]
 
-lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
+lemma ucast_down_bl': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
   unfolding of_bl_no by clarify (erule ucast_down_no)
     
 lemmas ucast_down_bl = ucast_down_bl' [OF refl]
@@ -984,7 +985,7 @@
   word_succ_def word_pred_def word_0_wi word_1_wi
 
 lemma udvdI: 
-  "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
+  "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
   by (auto simp: udvd_def)
 
 lemmas word_div_no [simp] = 
@@ -1015,14 +1016,14 @@
 lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
 lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
 
-lemma int_one_bin: "(1 :: int) == (Int.Pls BIT 1)"
+lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
   unfolding Pls_def Bit_def by auto
 
 lemma word_1_no: 
-  "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT 1)"
+  "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
   unfolding word_1_wi word_number_of_def int_one_bin by auto
 
-lemma word_m1_wi: "-1 == word_of_int -1" 
+lemma word_m1_wi: "-1 = word_of_int -1" 
   by (rule word_number_of_alt)
 
 lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
@@ -1056,7 +1057,7 @@
 lemma unat_0 [simp]: "unat 0 = 0"
   unfolding unat_def by auto
 
-lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
+lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
   apply (unfold word_size)
   apply (rule box_equals)
     defer
@@ -1129,11 +1130,11 @@
 
 lemmas wi_hom_syms = wi_homs [symmetric]
 
-lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
+lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
   unfolding word_sub_wi diff_minus
   by (simp only : word_uint.Rep_inverse wi_hom_syms)
     
-lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
+lemmas word_diff_minus = word_sub_def [standard]
 
 lemma word_of_int_sub_hom:
   "(word_of_int a) - word_of_int b = word_of_int (a - b)"
@@ -1265,13 +1266,13 @@
 
 subsection "Order on fixed-length words"
 
-lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
+lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
   unfolding word_le_def by auto
 
 lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
   unfolding word_le_def by auto
 
-lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
+lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
   unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
 
 lemma word_order_linear:
@@ -1307,7 +1308,7 @@
 
 lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard]
 
-lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
+lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
   unfolding word_sle_def word_sless_def
   by (auto simp add: less_le)
 
@@ -1347,7 +1348,7 @@
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
 
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1";
   unfolding word_arith_wis
   by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
 
@@ -1356,7 +1357,7 @@
 lemma no_no [simp] : "number_of (number_of b) = number_of b"
   by (simp add: number_of_eq)
 
-lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1"
+lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
   apply (unfold unat_def)
   apply (simp only: int_word_uint word_arith_alts rdmods)
   apply (subgoal_tac "uint x >= 1")
@@ -1378,7 +1379,7 @@
   apply simp
   done
     
-lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p"
+lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
   
 lemmas uint_add_ge0 [simp] =
@@ -1423,7 +1424,7 @@
 subsection {* Definition of uint\_arith *}
 
 lemma word_of_int_inverse:
-  "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
+  "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> 
    uint (a::'a::len0 word) = r"
   apply (erule word_uint.Abs_inverse' [rotated])
   apply (simp add: uints_num)
@@ -1454,7 +1455,7 @@
   uint_sub_if' uint_plus_if'
 
 (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
-lemma power_False_cong: "False ==> a ^ b = c ^ d" 
+lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" 
   by auto
 
 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
@@ -1520,11 +1521,11 @@
 lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
 
 lemma word_less_sub1: 
-  "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
+  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
   by uint_arith
 
 lemma word_le_sub1: 
-  "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
+  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
   by uint_arith
 
 lemma sub_wrap_lt: 
@@ -1536,19 +1537,19 @@
   by uint_arith
 
 lemma plus_minus_not_NULL_ab: 
-  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
+  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
   by uint_arith
 
 lemma plus_minus_no_overflow_ab: 
-  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c" 
+  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c" 
   by uint_arith
 
 lemma le_minus': 
-  "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
+  "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
   by uint_arith
 
 lemma le_plus': 
-  "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
+  "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
   by uint_arith
 
 lemmas le_plus = le_plus' [rotated]
@@ -1556,90 +1557,90 @@
 lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
 
 lemma word_plus_mono_right: 
-  "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
+  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
   by uint_arith
 
 lemma word_less_minus_cancel: 
-  "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
+  "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
   by uint_arith
 
 lemma word_less_minus_mono_left: 
-  "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
+  "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
   by uint_arith
 
 lemma word_less_minus_mono:  
-  "a < c ==> d < b ==> a - b < a ==> c - d < c 
-  ==> a - b < c - (d::'a::len word)"
+  "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c 
+  \<Longrightarrow> a - b < c - (d::'a::len word)"
   by uint_arith
 
 lemma word_le_minus_cancel: 
-  "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
+  "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
   by uint_arith
 
 lemma word_le_minus_mono_left: 
-  "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
+  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
   by uint_arith
 
 lemma word_le_minus_mono:  
-  "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c 
-  ==> a - b <= c - (d::'a::len word)"
+  "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c 
+  \<Longrightarrow> a - b <= c - (d::'a::len word)"
   by uint_arith
 
 lemma plus_le_left_cancel_wrap: 
-  "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
+  "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
   by uint_arith
 
 lemma plus_le_left_cancel_nowrap: 
-  "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> 
+  "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow> 
     (x + y' < x + y) = (y' < y)" 
   by uint_arith
 
 lemma word_plus_mono_right2: 
-  "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
+  "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
   by uint_arith
 
 lemma word_less_add_right: 
-  "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
+  "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
   by uint_arith
 
 lemma word_less_sub_right: 
-  "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
+  "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
   by uint_arith
 
 lemma word_le_plus_either: 
-  "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
+  "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
   by uint_arith
 
 lemma word_less_nowrapI: 
-  "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
+  "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
   by uint_arith
 
-lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
+lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
   by uint_arith
 
 lemma inc_i: 
-  "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
+  "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
   by uint_arith
 
 lemma udvd_incr_lem:
-  "up < uq ==> up = ua + n * uint K ==> 
-    uq = ua + n' * uint K ==> up + uint K <= uq"
+  "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 
+    uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
   apply clarsimp
   apply (drule less_le_mult)
   apply safe
   done
 
 lemma udvd_incr': 
-  "p < q ==> uint p = ua + n * uint K ==> 
-    uint q = ua + n' * uint K ==> p + K <= q" 
+  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
+    uint q = ua + n' * uint K \<Longrightarrow> p + K <= q" 
   apply (unfold word_less_alt word_le_def)
   apply (drule (2) udvd_incr_lem)
   apply (erule uint_add_le [THEN order_trans])
   done
 
 lemma udvd_decr': 
-  "p < q ==> uint p = ua + n * uint K ==> 
-    uint q = ua + n' * uint K ==> p <= q - K"
+  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
+    uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
   apply (unfold word_less_alt word_le_def)
   apply (drule (2) udvd_incr_lem)
   apply (drule le_diff_eq [THEN iffD2])
@@ -1652,7 +1653,7 @@
 lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
 
 lemma udvd_minus_le': 
-  "xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z"
+  "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
   apply (unfold udvd_def)
   apply clarify
   apply (erule (2) udvd_decr0)
@@ -1661,8 +1662,8 @@
 ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
 
 lemma udvd_incr2_K: 
-  "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
-    0 < K ==> p <= p + K & p + K <= a + s"
+  "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
+    0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
   apply (unfold udvd_def)
   apply clarify
   apply (simp add: uint_arith_simps split: split_if_asm)
@@ -1680,7 +1681,7 @@
 
 (* links with rbl operations *)
 lemma word_succ_rbl:
-  "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
+  "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
   apply (unfold word_succ_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
@@ -1688,7 +1689,7 @@
   done
 
 lemma word_pred_rbl:
-  "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
+  "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
   apply (unfold word_pred_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
@@ -1696,7 +1697,7 @@
   done
 
 lemma word_add_rbl:
-  "to_bl v = vbl ==> to_bl w = wbl ==> 
+  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
     to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
   apply (unfold word_add_def)
   apply clarify
@@ -1705,7 +1706,7 @@
   done
 
 lemma word_mult_rbl:
-  "to_bl v = vbl ==> to_bl w = wbl ==> 
+  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
     to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
   apply (unfold word_mult_def)
   apply clarify
@@ -1715,14 +1716,9 @@
 
 lemma rtb_rbl_ariths:
   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
-
   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
-
-  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
-  ==> rev (to_bl (v * w)) = rbl_mult ys xs"
-
-  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
-  ==> rev (to_bl (v + w)) = rbl_add ys xs"
+  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
+  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
   by (auto simp: rev_swap [symmetric] word_succ_rbl 
                  word_pred_rbl word_mult_rbl word_add_rbl)
 
@@ -1784,7 +1780,7 @@
   done
 
 lemma word_of_int_nat: 
-  "0 <= x ==> word_of_int x = of_nat (nat x)"
+  "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: of_nat_nat word_of_int)
 
 lemma word_number_of_eq: 
@@ -1806,7 +1802,7 @@
 subsection "Word and nat"
 
 lemma td_ext_unat':
-  "n = len_of TYPE ('a :: len) ==> 
+  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
     td_ext (unat :: 'a word => nat) of_nat 
     (unats n) (%i. i mod 2 ^ n)"
   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
@@ -1829,7 +1825,7 @@
 
 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
 
-lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
+lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
   apply (unfold unats_def)
   apply clarsimp
   apply (rule xtrans, rule unat_lt2p, assumption) 
@@ -1864,11 +1860,11 @@
 
 lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
 
-lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k"
+lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
   by (cases k) auto
 
 lemma of_nat_neq_0: 
-  "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
+  "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
   by (clarsimp simp add : of_nat_0)
 
 lemma Abs_fnat_hom_add:
@@ -1943,7 +1939,7 @@
   trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
 
 lemma le_no_overflow: 
-  "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
+  "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
   apply (erule order_trans)
   apply (erule olen_add_eqv [THEN iffD1])
   done
@@ -2064,7 +2060,7 @@
 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
 
 lemma word_div_mult: 
-  "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> 
+  "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> 
     x * y div y = x"
   apply unat_arith
   apply clarsimp
@@ -2072,7 +2068,7 @@
   apply auto
   done
 
-lemma div_lt': "(i :: 'a :: len word) <= k div x ==> 
+lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow> 
     unat i * unat x < 2 ^ len_of TYPE('a)"
   apply unat_arith
   apply clarsimp
@@ -2083,7 +2079,7 @@
 
 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
 
-lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
+lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
   apply (simp add: unat_arith_simps)
   apply (drule (1) mult_less_mono1)
@@ -2092,7 +2088,7 @@
   done
 
 lemma div_le_mult: 
-  "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
+  "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
   apply (simp add: unat_arith_simps)
   apply (drule mult_le_mono1)
@@ -2101,7 +2097,7 @@
   done
 
 lemma div_lt_uint': 
-  "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
+  "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
   apply (unfold uint_nat)
   apply (drule div_lt')
   apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
@@ -2111,7 +2107,7 @@
 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
 
 lemma word_le_exists': 
-  "(x :: 'a :: len0 word) <= y ==> 
+  "(x :: 'a :: len0 word) <= y \<Longrightarrow> 
     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
   apply (rule exI)
   apply (rule conjI)
@@ -2164,7 +2160,7 @@
   apply simp
   done
 
-lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
+lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
   apply (simp only: word_less_nat_alt word_arith_nat_defs)
   apply (clarsimp simp add : uno_simps)
   done
@@ -2178,7 +2174,7 @@
   by (simp add : word_of_int_power_hom [symmetric])
 
 lemma of_bl_length_less: 
-  "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
+  "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
   apply (unfold of_bl_no [unfolded word_number_of_def]
                 word_less_alt word_number_of_alt)
   apply safe
@@ -2246,7 +2242,7 @@
                 bin_trunc_ao(1) [symmetric]) 
 
 lemma word_ops_nth_size:
-  "n < size (x::'a::len0 word) ==> 
+  "n < size (x::'a::len0 word) \<Longrightarrow> 
     (x OR y) !! n = (x !! n | y !! n) & 
     (x AND y) !! n = (x !! n & y !! n) & 
     (x XOR y) !! n = (x !! n ~= y !! n) & 
@@ -2392,10 +2388,10 @@
 
 lemma leoa:   
   fixes x :: "'a::len0 word"
-  shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
+  shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
 lemma leao: 
   fixes x' :: "'a::len0 word"
-  shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto 
+  shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
 
 lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
 
@@ -2447,7 +2443,7 @@
   by (simp add : sign_Min_lt_0 number_of_is_id)
   
 lemma word_msb_no': 
-  "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
+  "w = number_of bin \<Longrightarrow> msb (w::'a::len word) = bin_nth bin (size w - 1)"
   unfolding word_msb_def word_number_of_def
   by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
 
@@ -2487,7 +2483,7 @@
   unfolding to_bl_def word_test_bit_def word_size
   by (rule bin_nth_uint)
 
-lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
+lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
   apply (unfold test_bit_bl)
   apply clarsimp
   apply (rule trans)
@@ -2530,7 +2526,7 @@
 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
 
 lemma td_ext_nth':
-  "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> 
+  "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 
     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
   apply (unfold word_size td_ext_def')
   apply (safe del: subset_antisym)
@@ -2575,7 +2571,7 @@
     
 lemma test_bit_no': 
   fixes w :: "'a::len0 word"
-  shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
+  shows "w = number_of bin \<Longrightarrow> test_bit w n = (n < size w & bin_nth bin n)"
   unfolding word_test_bit_def word_number_of_def word_size
   by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
 
@@ -2605,10 +2601,13 @@
                         test_bit_no nth_bintr)
   done
 
-lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
-  simplified if_simps, THEN eq_reflection, standard]
-lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
-  simplified if_simps, THEN eq_reflection, standard]
+lemma setBit_no:
+  "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
+  by (simp add: setBit_def word_set_no)
+
+lemma clearBit_no:
+  "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
+  by (simp add: clearBit_def word_set_no)
 
 lemma to_bl_n1: 
   "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
@@ -2643,7 +2642,7 @@
   done
 
 lemma test_bit_2p': 
-  "w = word_of_int (2 ^ n) ==> 
+  "w = word_of_int (2 ^ n) \<Longrightarrow> 
     w !! m = (m = n & m < size (w :: 'a :: len word))"
   unfolding word_test_bit_def word_size
   by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
@@ -2656,7 +2655,7 @@
   by (simp add:  of_int_power)
 
 lemma uint_2p: 
-  "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
+  "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
   apply (unfold word_arith_power_alt)
   apply (case_tac "len_of TYPE ('a)")
    apply clarsimp
@@ -2682,7 +2681,7 @@
   apply simp 
   done
 
-lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)" 
+lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
   apply (rule xtr3) 
   apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
@@ -2996,7 +2995,7 @@
 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
 
-lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
+lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
   by (auto intro: append_take_drop_id [symmetric])
 
 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
@@ -3022,7 +3021,7 @@
 
 lemma shiftl_zero_size: 
   fixes x :: "'a::len0 word"
-  shows "size x <= n ==> x << n = 0"
+  shows "size x <= n \<Longrightarrow> x << n = 0"
   apply (unfold word_size)
   apply (rule word_eqI)
   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
@@ -3059,7 +3058,7 @@
   by (simp add : word_sbin.eq_norm)
 
 lemma shiftr_no': 
-  "w = number_of bin ==> 
+  "w = number_of bin \<Longrightarrow> 
   (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
   apply clarsimp
   apply (rule word_eqI)
@@ -3067,7 +3066,7 @@
   done
 
 lemma sshiftr_no': 
-  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^^ n) 
+  "w = number_of bin \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n) 
     (sbintrunc (size w - 1) bin))"
   apply clarsimp
   apply (rule word_eqI)
@@ -3082,7 +3081,7 @@
   shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
 
 lemma shiftr1_bl_of': 
-  "us = shiftr1 (of_bl bl) ==> length bl <= size us ==> 
+  "us = shiftr1 (of_bl bl) \<Longrightarrow> length bl <= size us \<Longrightarrow> 
     us = of_bl (butlast bl)"
   by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin 
                      word_ubin.eq_norm trunc_bl2bin)
@@ -3090,7 +3089,7 @@
 lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
 
 lemma shiftr_bl_of' [rule_format]: 
-  "us = of_bl bl >> n ==> length bl <= size us --> 
+  "us = of_bl bl >> n \<Longrightarrow> length bl <= size us --> 
    us = of_bl (take (length bl - n) bl)"
   apply (unfold shiftr_def)
   apply hypsubst
@@ -3147,8 +3146,8 @@
   done
 
 lemma aligned_bl_add_size':
-  "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
-    take m (to_bl y) = replicate m False ==> 
+  "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
+    take m (to_bl y) = replicate m False \<Longrightarrow> 
     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
   apply (subgoal_tac "x AND y = 0")
    prefer 2
@@ -3167,7 +3166,7 @@
 
 subsubsection "Mask"
 
-lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
+lemma nth_mask': "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
   apply (unfold mask_def test_bit_bl)
   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
   apply (clarsimp simp add: word_size)
@@ -3247,14 +3246,14 @@
   done
 
 lemma word_2p_lem: 
-  "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
+  "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
   apply (unfold word_size word_less_alt word_number_of_alt)
   apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
                             int_mod_eq'
                   simp del: word_of_int_bin)
   done
 
-lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
+lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
   apply (unfold word_less_alt word_number_of_alt)
   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
                             word_uint.eq_norm
@@ -3270,11 +3269,11 @@
 lemmas and_mask_less' = 
   iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
 
-lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
+lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
   unfolding word_size by (erule and_mask_less')
 
 lemma word_mod_2p_is_mask':
-  "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" 
+  "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n" 
   by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
 
 lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
@@ -3317,7 +3316,7 @@
   done
 
 lemma revcast_rev_ucast': 
-  "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==> 
+  "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 
     rc = word_reverse uc"
   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
   apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
@@ -3338,7 +3337,7 @@
 lemmas wsst_TYs = source_size target_size word_size
 
 lemma revcast_down_uu': 
-  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
     rc (w :: 'a :: len word) = ucast (w >> n)"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
@@ -3349,7 +3348,7 @@
   done
 
 lemma revcast_down_us': 
-  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
     rc (w :: 'a :: len word) = ucast (w >>> n)"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
@@ -3360,7 +3359,7 @@
   done
 
 lemma revcast_down_su': 
-  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
     rc (w :: 'a :: len word) = scast (w >> n)"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
@@ -3371,7 +3370,7 @@
   done
 
 lemma revcast_down_ss': 
-  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
     rc (w :: 'a :: len word) = scast (w >>> n)"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
@@ -3387,7 +3386,7 @@
 lemmas revcast_down_ss = refl [THEN revcast_down_ss']
 
 lemma cast_down_rev: 
-  "uc = ucast ==> source_size uc = target_size uc + n ==> 
+  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
     uc w = revcast ((w :: 'a :: len word) << n)"
   apply (unfold shiftl_rev)
   apply clarify
@@ -3399,7 +3398,7 @@
   done
 
 lemma revcast_up': 
-  "rc = revcast ==> source_size rc + n = target_size rc ==> 
+  "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 
     rc w = (ucast w :: 'a :: len word) << n" 
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
@@ -3424,13 +3423,14 @@
 
 subsubsection "Slices"
 
-lemmas slice1_no_bin [simp] =
-  slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
-
-lemmas slice_no_bin [simp] = 
-   trans [OF slice_def [THEN meta_eq_to_obj_eq] 
-             slice1_no_bin [THEN meta_eq_to_obj_eq], 
-          unfolded word_size, standard]
+lemma slice1_no_bin [simp]:
+  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
+  by (simp add: slice1_def)
+
+lemma slice_no_bin [simp]:
+  "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
+    (bin_to_bl (len_of TYPE('b :: len0)) w))"
+  by (simp add: slice_def word_size)
 
 lemma slice1_0 [simp] : "slice1 n 0 = 0"
   unfolding slice1_def by (simp add : to_bl_0)
@@ -3462,13 +3462,13 @@
   by (simp add : nth_ucast nth_shiftr)
 
 lemma slice1_down_alt': 
-  "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==> 
+  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 
     to_bl sl = takefill False fs (drop k (to_bl w))"
   unfolding slice1_def word_size of_bl_def uint_bl
   by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
 
 lemma slice1_up_alt': 
-  "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==> 
+  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 
     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
   apply (unfold slice1_def word_size of_bl_def uint_bl)
   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
@@ -3495,7 +3495,7 @@
 lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
 
 lemma revcast_slice1': 
-  "rc = revcast w ==> slice1 (size rc) w = rc"
+  "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
   unfolding slice1_def revcast_def' by (simp add : word_size)
 
 lemmas revcast_slice1 = refl [THEN revcast_slice1']
@@ -3522,7 +3522,7 @@
   done
 
 lemma rev_slice': 
-  "res = slice n (word_reverse w) ==> n + k + size res = size w ==> 
+  "res = slice n (word_reverse w) \<Longrightarrow> n + k + size res = size w \<Longrightarrow> 
     res = word_reverse (slice k w)"
   apply (unfold slice_def word_size)
   apply clarify
@@ -3569,8 +3569,8 @@
 
 subsection "Split and cat"
 
-lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
-lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
+lemmas word_split_bin' = word_split_def
+lemmas word_cat_bin' = word_cat_def
 
 lemma word_rsplit_no:
   "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
@@ -3584,7 +3584,7 @@
   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
 
 lemma test_bit_cat:
-  "wc = word_cat a b ==> wc !! n = (n < size wc & 
+  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc & 
     (if n < size b then b !! n else a !! (n - size b)))"
   apply (unfold word_cat_bin' test_bit_bin)
   apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
@@ -3617,7 +3617,7 @@
   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   by (cases x) (simp_all add: of_bl_True)
 
-lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> 
+lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow> 
   a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
   apply (frule word_ubin.norm_Rep [THEN ssubst])
   apply (drule bin_split_trunc1)
@@ -3627,7 +3627,7 @@
   done
 
 lemma word_split_bl': 
-  "std = size c - size b ==> (word_split c = (a, b)) ==> 
+  "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 
     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
   apply (unfold word_split_bin')
   apply safe
@@ -3653,7 +3653,7 @@
   apply (simp add : word_ubin.norm_eq_iff [symmetric])
   done
 
-lemma word_split_bl: "std = size c - size b ==> 
+lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
     word_split c = (a, b)"
   apply (rule iffI)
@@ -3714,7 +3714,7 @@
 -- "limited hom result"
 lemma word_cat_hom:
   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
-  ==>
+  \<Longrightarrow>
   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
@@ -3723,7 +3723,7 @@
   done
 
 lemma word_cat_split_alt:
-  "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
+  "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
   apply (rule word_eqI)
   apply (drule test_bit_split)
   apply (clarsimp simp add : test_bit_cat word_size)
@@ -3738,14 +3738,14 @@
 subsubsection "Split and slice"
 
 lemma split_slices: 
-  "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
+  "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
   apply (drule test_bit_split)
   apply (rule conjI)
    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
   done
 
 lemma slice_cat1':
-  "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
+  "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
   apply safe
   apply (rule word_eqI)
   apply (simp add: nth_slice test_bit_cat word_size)
@@ -3755,8 +3755,8 @@
 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
 
 lemma cat_slices:
-  "a = slice n c ==> b = slice 0 c ==> n = size b ==>
-    size a + size b >= size c ==> word_cat a b = c"
+  "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
+    size a + size b >= size c \<Longrightarrow> word_cat a b = c"
   apply safe
   apply (rule word_eqI)
   apply (simp add: nth_slice test_bit_cat word_size)
@@ -3765,7 +3765,7 @@
   done
 
 lemma word_split_cat_alt:
-  "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
+  "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
   apply (case_tac "word_split ?w")
   apply (rule trans, assumption)
   apply (drule test_bit_split)
@@ -3794,8 +3794,8 @@
   by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
 
 lemma test_bit_rsplit:
-  "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
-    k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
+  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
+    k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
   apply (unfold word_rsplit_def word_test_bit_def)
   apply (rule trans)
    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
@@ -3812,7 +3812,7 @@
   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
   done
 
-lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
+lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
   unfolding word_rcat_def to_bl_def' of_bl_def
   by (clarsimp simp add : bin_rcat_bl)
 
@@ -3825,7 +3825,7 @@
 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
 
 lemma nth_rcat_lem' [rule_format] :
-  "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw --> 
+  "sw = size (hd wl  :: 'a :: len word) \<Longrightarrow> (ALL n. n < size wl * sw --> 
     rev (concat (map to_bl wl)) ! n = 
     rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
   apply (unfold word_size)
@@ -3840,7 +3840,7 @@
 lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
 
 lemma test_bit_rcat:
-  "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = 
+  "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
   apply (unfold word_rcat_bl word_size)
   apply (clarsimp simp add : 
@@ -3862,8 +3862,8 @@
 
 -- "lazy way of expressing that u and v, and su and sv, have same types"
 lemma word_rsplit_len_indep':
-  "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==> 
-    word_rsplit v = sv ==> length su = length sv"
+  "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
+    word_rsplit v = sv \<Longrightarrow> length su = length sv"
   apply (unfold word_rsplit_def)
   apply (auto simp add : bin_rsplit_len_indep)
   done
@@ -3871,7 +3871,7 @@
 lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
 
 lemma length_word_rsplit_size: 
-  "n = len_of TYPE ('a :: len) ==> 
+  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
   apply (unfold word_rsplit_def word_size)
   apply (clarsimp simp add : bin_rsplit_len_le)
@@ -3881,12 +3881,12 @@
   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
 
 lemma length_word_rsplit_exp_size: 
-  "n = len_of TYPE ('a :: len) ==> 
+  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
 
 lemma length_word_rsplit_even_size: 
-  "n = len_of TYPE ('a :: len) ==> size w = m * n ==> 
+  "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow> 
     length (word_rsplit w :: 'a word list) = m"
   by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
 
@@ -3907,8 +3907,8 @@
   done
 
 lemma size_word_rsplit_rcat_size':
-  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
-    size frcw = length ws * len_of TYPE ('a) ==> 
+  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
+    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> 
     size (hd [word_rsplit frcw, ws]) = size ws" 
   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
   apply (fast intro: given_quot_alt)
@@ -3924,8 +3924,8 @@
   by (auto simp: add_commute)
 
 lemma word_rsplit_rcat_size':
-  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
-    size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws" 
+  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
+    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
   apply (frule size_word_rsplit_rcat_size, assumption)
   apply (clarsimp simp add : word_size)
   apply (rule nth_equalityI, assumption)
@@ -3957,7 +3957,7 @@
 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
 
 lemma rotate_eq_mod: 
-  "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
+  "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   apply (rule box_equals)
     defer
     apply (rule rotate_conv_mod [symmetric])+
@@ -4049,11 +4049,11 @@
 
 subsubsection "map, map2, commuting with rotate(r)"
 
-lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
+lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
   by (induct xs) auto
 
 lemma butlast_map:
-  "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
+  "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   by (induct xs) auto
 
 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
@@ -4085,7 +4085,7 @@
   done
 
 lemma rotater1_zip:
-  "length xs = length ys ==> 
+  "length xs = length ys \<Longrightarrow> 
     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
   apply (unfold rotater1_def)
   apply (cases "xs")
@@ -4094,7 +4094,7 @@
   done
 
 lemma rotater1_map2:
-  "length xs = length ys ==> 
+  "length xs = length ys \<Longrightarrow> 
     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
   unfolding map2_def by (simp add: rotater1_map rotater1_zip)
 
@@ -4104,12 +4104,12 @@
               THEN rotater1_map2]
 
 lemma rotater_map2: 
-  "length xs = length ys ==> 
+  "length xs = length ys \<Longrightarrow> 
     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
   by (induct n) (auto intro!: lrth)
 
 lemma rotate1_map2:
-  "length xs = length ys ==> 
+  "length xs = length ys \<Longrightarrow> 
     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
   apply (unfold map2_def)
   apply (cases xs)
@@ -4120,7 +4120,7 @@
   length_rotate [symmetric], THEN rotate1_map2]
 
 lemma rotate_map2: 
-  "length xs = length ys ==> 
+  "length xs = length ys \<Longrightarrow> 
     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
   by (induct n) (auto intro!: lth)
 
@@ -4177,11 +4177,11 @@
   "word_roti (m + n) w = word_roti m (word_roti n w)"
 proof -
   have rotater_eq_lem: 
-    "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
+    "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
     by auto
 
   have rotate_eq_lem: 
-    "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
+    "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
     by auto
 
   note rpts [symmetric, standard] = 
@@ -4271,7 +4271,7 @@
   simplified word_bl.Rep', standard]
 
 lemma bl_word_roti_dt': 
-  "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==> 
+  "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow> 
     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
   apply (unfold word_roti_def)
   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
@@ -4457,12 +4457,12 @@
   by (simp add: mask_bl word_rep_drop min_def)
 
 lemma map_replicate_True:
-  "n = length xs ==>
+  "n = length xs \<Longrightarrow>
     map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
   by (induct xs arbitrary: n) auto
 
 lemma map_replicate_False:
-  "n = length xs ==> map (\<lambda>(x,y). x & y)
+  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
     (zip xs (replicate n False)) = replicate n False"
   by (induct xs arbitrary: n) auto
 
@@ -4488,7 +4488,7 @@
 qed
 
 lemma drop_rev_takefill:
-  "length xs \<le> n ==>
+  "length xs \<le> n \<Longrightarrow>
     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
   by (simp add: takefill_alt rev_take)
 
@@ -4547,7 +4547,7 @@
                 word_size)
 
 lemma unat_sub:
-  "b <= a ==> unat (a - b) = unat a - unat b"
+  "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
 
 lemmas word_less_sub1_numberof [simp] =
@@ -4633,7 +4633,7 @@
   done
 
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
-  "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
+  "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
 
 lemma word_rec_0: "word_rec z s 0 = z"
   by (simp add: word_rec_def)
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/ZF/Games.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -893,9 +893,9 @@
   have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel" 
     apply (simp add: congruent2_def)
     apply (auto simp add: eq_game_rel_def eq_game_def)
-    apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
+    apply (rule_tac y="plus_game a ba" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
-    apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
+    apply (rule_tac y="plus_game b aa" in ge_game_trans)
     apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
     done
   then show ?thesis
diff -r 47ff261431c4 -r edd1e0764da1 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 18:22:43 2010 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 21:54:15 2010 +0100
@@ -1288,7 +1288,7 @@
 proof -
   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
         respects2 realrel"
-    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
+    by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
   thus ?thesis
     by (simp add: real_add_def UN_UN_split_split_eq
                   UN_equiv_class2 [OF equiv_realrel equiv_realrel])
@@ -1297,7 +1297,7 @@
 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
 proof -
   have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
-    by (simp add: congruent_def add_commute) 
+    by (auto simp add: congruent_def add_commute) 
   thus ?thesis
     by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
 qed