# HG changeset patch
# User wenzelm
# Date 1125495997 -7200
# Node ID 3a4d03d1a31bb609bc70ea351cfed745c94d9955
# Parent  59c1bfc81d918fd85a81360593eca2329de9b4b7
tuned presentation;

diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -3,39 +3,39 @@
     Author:     Norbert Voelker
 *)
 
-header {* Instantiation of order classes type char *}
+header {* Order on characters *}
 
 theory Char_ord
 imports Product_ord
 begin
 
-text {* Conversions between nibbles and integers in [0..15]. *} 
+text {* Conversions between nibbles and integers in [0..15]. *}
 
-consts 
+consts
   nibble_to_int:: "nibble \<Rightarrow> int"
   int_to_nibble:: "int \<Rightarrow> nibble"
 
-primrec 
-  "nibble_to_int Nibble0 = 0"  
-  "nibble_to_int Nibble1 = 1" 
-  "nibble_to_int Nibble2 = 2" 
-  "nibble_to_int Nibble3 = 3" 
-  "nibble_to_int Nibble4 = 4" 
-  "nibble_to_int Nibble5 = 5" 
-  "nibble_to_int Nibble6 = 6" 
-  "nibble_to_int Nibble7 = 7" 
-  "nibble_to_int Nibble8 = 8" 
-  "nibble_to_int Nibble9 = 9" 
-  "nibble_to_int NibbleA = 10" 
-  "nibble_to_int NibbleB = 11" 
-  "nibble_to_int NibbleC = 12" 
-  "nibble_to_int NibbleD = 13" 
-  "nibble_to_int NibbleE = 14" 
+primrec
+  "nibble_to_int Nibble0 = 0"
+  "nibble_to_int Nibble1 = 1"
+  "nibble_to_int Nibble2 = 2"
+  "nibble_to_int Nibble3 = 3"
+  "nibble_to_int Nibble4 = 4"
+  "nibble_to_int Nibble5 = 5"
+  "nibble_to_int Nibble6 = 6"
+  "nibble_to_int Nibble7 = 7"
+  "nibble_to_int Nibble8 = 8"
+  "nibble_to_int Nibble9 = 9"
+  "nibble_to_int NibbleA = 10"
+  "nibble_to_int NibbleB = 11"
+  "nibble_to_int NibbleC = 12"
+  "nibble_to_int NibbleD = 13"
+  "nibble_to_int NibbleE = 14"
   "nibble_to_int NibbleF = 15"
 
-defs 
-  int_to_nibble_def:  
-    "int_to_nibble x \<equiv> (let y = x mod 16 in 
+defs
+  int_to_nibble_def:
+    "int_to_nibble x \<equiv> (let y = x mod 16 in
        if y = 0 then Nibble0 else
        if y = 1 then Nibble1 else
        if y = 2 then Nibble2 else
@@ -54,46 +54,54 @@
        NibbleF)"
 
 lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
-  by (case_tac x, auto simp: int_to_nibble_def Let_def)
+  by (cases x) (auto simp: int_to_nibble_def Let_def)
 
 lemma inj_nibble_to_int: "inj nibble_to_int"
-  by (rule inj_on_inverseI, rule int_to_nibble_nibble_to_int)
+  by (rule inj_on_inverseI) (rule int_to_nibble_nibble_to_int)
 
 lemmas nibble_to_int_eq = inj_nibble_to_int [THEN inj_eq]
 
 lemma nibble_to_int_ge_0: "0 \<le> nibble_to_int x"
-  by (case_tac x, auto)
+  by (cases x) auto
 
 lemma nibble_to_int_less_16: "nibble_to_int x < 16"
-  by (case_tac x, auto)
+  by (cases x) auto
 
 text {* Conversion between chars and int pairs. *}
 
-consts 
+consts
   char_to_int_pair :: "char \<Rightarrow> int \<times> int"
 primrec
-  "char_to_int_pair(Char a b) = (nibble_to_int a, nibble_to_int b)" 
+  "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
 
 lemma inj_char_to_int_pair: "inj char_to_int_pair"
-  by (rule inj_onI, case_tac x, case_tac y, auto simp: nibble_to_int_eq)
+  apply (rule inj_onI)
+  apply (case_tac x, case_tac y)
+  apply (auto simp: nibble_to_int_eq)
+  done
 
 lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
 
-text {* Instantiation of order classes *} 
+text {* Instantiation of order classes *}
 
 instance char :: ord ..
 
 defs (overloaded)
-  char_le_def:  "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)" 
-  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" 
+  char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
+  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
 
 lemmas char_ord_defs = char_less_def char_le_def
 
-instance char::order
-  apply (intro_classes, unfold char_ord_defs)
-  by (auto simp: char_to_int_pair_eq order_less_le)
+instance char :: order
+  apply intro_classes
+     apply (unfold char_ord_defs)
+     apply (auto simp: char_to_int_pair_eq order_less_le)
+  done
 
 instance char::linorder
-  by (intro_classes, unfold char_le_def, auto)
+  apply intro_classes
+  apply (unfold char_le_def)
+  apply auto
+  done
 
-end
\ No newline at end of file
+end
diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/List_lexord.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -3,51 +3,54 @@
     Author:     Norbert Voelker
 *)
 
-header {* Instantiation of order classes for lexord on lists *}
+header {* Lexicographic order on lists *}
 
 theory List_lexord
 imports Main
 begin
 
 instance list :: (ord) ord ..
-defs(overloaded)
-  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)" 
-  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs,ys) \<in> lexord {(u,v). u < v}"
+defs (overloaded)
+  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
+  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}"
 
 lemmas list_ord_defs = list_less_def list_le_def
 
-instance list::(order)order
+instance list :: (order) order
   apply (intro_classes, unfold list_ord_defs)
-  apply (rule disjI2, safe)
-  apply (blast intro: lexord_trans transI order_less_trans)
+     apply (rule disjI2, safe)
+    apply (blast intro: lexord_trans transI order_less_trans)
+   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
+    apply simp
+   apply (blast intro: lexord_trans transI order_less_trans)
   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
   apply simp
-  apply (blast intro: lexord_trans transI order_less_trans)
-  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
-  apply simp
-  by assumption
+  apply assumption
+  done
 
 instance list::(linorder)linorder
   apply (intro_classes, unfold list_le_def list_less_def, safe)
-  apply (cut_tac x="x" and y="y" and  r = "{(a,b). a < b}"  in lexord_linear)
-  by (force, simp)
+  apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
+   apply force
+  apply simp
+  done
 
-lemma not_less_Nil[simp]: "~(x < [])";
-  by (unfold list_less_def, simp);
+lemma not_less_Nil[simp]: "~(x < [])"
+  by (unfold list_less_def) simp
 
-lemma Nil_less_Cons[simp]: "[] < a # x";
-  by (unfold list_less_def, simp);
+lemma Nil_less_Cons[simp]: "[] < a # x"
+  by (unfold list_less_def) simp
 
-lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)";
-  by (unfold list_less_def, simp);
+lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)"
+  by (unfold list_less_def) simp
 
-lemma le_Nil[simp]: "(x <= [])   = (x = [])";
-  by (unfold list_ord_defs, case_tac x, auto);
+lemma le_Nil[simp]: "(x <= []) = (x = [])"
+  by (unfold list_ord_defs, cases x) auto
 
-lemma Nil_le_Cons[simp]: "([] <= x)";
-  by (unfold list_ord_defs, case_tac x, auto);
+lemma Nil_le_Cons [simp]: "([] <= x)"
+  by (unfold list_ord_defs, cases x) auto
 
-lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)";
-  by (unfold list_ord_defs, auto);
+lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
+  by (unfold list_ord_defs) auto
 
-end
\ No newline at end of file
+end
diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -52,7 +52,7 @@
   Zero_multiset_def [simp]: "0 == {#}"
   size_def: "size M == setsum (count M) (set_of M)"
 
-constdefs 
+constdefs
  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
  "multiset_inter A B \<equiv> A - (A - B)"
 
@@ -109,7 +109,7 @@
 lemmas union_ac = union_assoc union_commute union_lcomm
 
 instance multiset :: (type) comm_monoid_add
-proof 
+proof
   fix a b c :: "'a multiset"
   show "(a + b) + c = a + (b + c)" by (rule union_assoc)
   show "a + b = b + a" by (rule union_commute)
@@ -254,11 +254,11 @@
   by (simp add: multiset_inter_def min_def)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
+  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.below_inf.inf_commute)
 
 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
+  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.below_inf.inf_assoc)
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
@@ -270,7 +270,7 @@
   multiset_inter_left_commute
 
 lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
-  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def 
+  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
     split: split_if_asm)
   apply clarsimp
   apply (erule_tac x = a in allE)
@@ -345,7 +345,7 @@
      prefer 2
      apply (simp add: expand_fun_eq)
     apply (erule ssubst)
-    apply (erule Abs_multiset_inverse [THEN subst]) 
+    apply (erule Abs_multiset_inverse [THEN subst])
     apply (erule prem2 [unfolded defns, simplified])
     done
 qed
@@ -728,7 +728,7 @@
 
 lemma union_upper1: "A <= A + (B::'a::order multiset)"
 proof -
-  have "A + {#} <= A + B" by (blast intro: union_le_mono) 
+  have "A + {#} <= A + B" by (blast intro: union_le_mono)
   thus ?thesis by simp
 qed
 
@@ -736,63 +736,63 @@
 by (subst union_commute, rule union_upper1)
 
 
-subsection {* Link with lists *} 
+subsection {* Link with lists *}
 
-consts 
+consts
   multiset_of :: "'a list \<Rightarrow> 'a multiset"
 primrec
   "multiset_of [] = {#}"
   "multiset_of (a # x) = multiset_of x + {# a #}"
 
 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
-  by (induct_tac x, auto) 
+  by (induct_tac x, auto)
 
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   by (induct_tac x, auto)
 
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
-  by (induct_tac x, auto) 
+  by (induct_tac x, auto)
 
 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   by (induct xs) auto
 
-lemma multiset_of_append[simp]: 
+lemma multiset_of_append[simp]:
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
-  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
+  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac)
 
 lemma surj_multiset_of: "surj multiset_of"
-  apply (unfold surj_def, rule allI) 
-  apply (rule_tac M=y in multiset_induct, auto) 
-  apply (rule_tac x = "x # xa" in exI, auto) 
+  apply (unfold surj_def, rule allI)
+  apply (rule_tac M=y in multiset_induct, auto)
+  apply (rule_tac x = "x # xa" in exI, auto)
   done
 
 lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
-  by (induct_tac x, auto)  
+  by (induct_tac x, auto)
 
-lemma distinct_count_atmost_1: 
+lemma distinct_count_atmost_1:
    "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
    apply ( induct_tac x, simp, rule iffI, simp_all)
-   apply (rule conjI)  
-   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
+   apply (rule conjI)
+   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
    apply (erule_tac x=a in allE, simp, clarify)
-   apply (erule_tac x=aa in allE, simp) 
+   apply (erule_tac x=aa in allE, simp)
    done
 
-lemma multiset_of_eq_setD: 
+lemma multiset_of_eq_setD:
   "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
   by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
 
-lemma set_eq_iff_multiset_of_eq_distinct: 
-  "\<lbrakk>distinct x; distinct y\<rbrakk> 
+lemma set_eq_iff_multiset_of_eq_distinct:
+  "\<lbrakk>distinct x; distinct y\<rbrakk>
    \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
-  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
+  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
 
-lemma set_eq_iff_multiset_of_remdups_eq: 
+lemma set_eq_iff_multiset_of_remdups_eq:
    "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
-  apply (rule iffI) 
-  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
-  apply (drule distinct_remdups[THEN distinct_remdups 
-                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
+  apply (rule iffI)
+  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
+  apply (drule distinct_remdups[THEN distinct_remdups
+                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]])
   apply simp
   done
 
@@ -800,61 +800,66 @@
  "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   by (induct xs) (auto simp: union_ac)
 
-lemma count_filter: 
+lemma count_filter:
   "count (multiset_of xs) x = length [y \<in> xs. y = x]"
   by (induct xs, auto)
 
 
 subsection {* Pointwise ordering induced by count *}
 
-consts 
+consts
   mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
 
-syntax 
-  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50) 
-translations 
+syntax
+  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
+translations
   "x \<le># y" == "mset_le x y"
 
-defs 
-  mset_le_def:   "xs \<le># ys  == (! a. count xs a \<le> count ys a)"
+defs
+  mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
 
 lemma mset_le_refl[simp]: "xs \<le># xs"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
-  by (unfold mset_le_def, fast intro: order_trans) 
+  by (unfold mset_le_def) (fast intro: order_trans)
 
 lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
-  apply (unfold mset_le_def) 
-  apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 
+  apply (unfold mset_le_def)
+  apply (rule multiset_eq_conv_count_eq[THEN iffD2])
   apply (blast intro: order_antisym)
   done
 
-lemma mset_le_exists_conv: 
-  "(xs \<le># ys) = (? zs. ys = xs + zs)"
-  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) 
+lemma mset_le_exists_conv:
+  "(xs \<le># ys) = (\<exists>zs. ys = xs + zs)"
+  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI)
   apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   done
 
 lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
-lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
-  apply (unfold mset_le_def, auto) 
+lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws"
+  apply (unfold mset_le_def)
+  apply auto
   apply (erule_tac x=a in allE)+
   apply auto
   done
 
 lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
-  by (unfold mset_le_def, auto)
+  by (unfold mset_le_def) auto
 
 lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
-  by (induct_tac x, auto, rule mset_le_trans, auto)
+  apply (induct x)
+   apply auto
+  apply (rule mset_le_trans)
+   apply auto
+  done
 
 end
diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -24,20 +24,20 @@
     trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
 
 lemma perm_refl [iff]: "l <~~> l"
-by (induct l, auto)
+  by (induct l) auto
 
 
 subsection {* Some examples of rule induction on permutations *}
 
 lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
-    -- {*the form of the premise lets the induction bind @{term xs} 
+    -- {*the form of the premise lets the induction bind @{term xs}
          and @{term ys} *}
   apply (erule perm.induct)
      apply (simp_all (no_asm_simp))
   done
 
 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
-by (insert xperm_empty_imp_aux, blast)
+  using xperm_empty_imp_aux by blast
 
 
 text {*
@@ -45,16 +45,16 @@
   *}
 
 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
-by (erule perm.induct, simp_all)
+  by (erule perm.induct) simp_all
 
 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
-by (drule perm_length, auto)
+  by (drule perm_length) auto
 
 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
-by (erule perm.induct, auto)
+  by (erule perm.induct) auto
 
 lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
-by (erule perm.induct, auto)
+  by (erule perm.induct) auto
 
 
 subsection {* Ways of making new permutations *}
@@ -64,32 +64,34 @@
 *}
 
 lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
-by (induct xs, auto)
+  by (induct xs) auto
 
 lemma perm_append_swap: "xs @ ys <~~> ys @ xs"
-  apply (induct xs, simp_all)
+  apply (induct xs)
+    apply simp_all
   apply (blast intro: perm_append_Cons)
   done
 
 lemma perm_append_single: "a # xs <~~> xs @ [a]"
-  by (rule perm.trans [OF _ perm_append_swap], simp)
+  by (rule perm.trans [OF _ perm_append_swap]) simp
 
 lemma perm_rev: "rev xs <~~> xs"
-  apply (induct xs, simp_all)
+  apply (induct xs)
+   apply simp_all
   apply (blast intro!: perm_append_single intro: perm_sym)
   done
 
 lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"
-by (induct l, auto)
+  by (induct l) auto
 
 lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l"
-by (blast intro!: perm_append_swap perm_append1)
+  by (blast intro!: perm_append_swap perm_append1)
 
 
 subsection {* Further results *}
 
 lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
-by (blast intro: perm_empty_imp)
+  by (blast intro: perm_empty_imp)
 
 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
   apply auto
@@ -97,13 +99,13 @@
   done
 
 lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
-by (erule perm.induct, auto)
+  by (erule perm.induct) auto
 
 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
-by (blast intro: perm_sing_imp)
+  by (blast intro: perm_sing_imp)
 
 lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
-by (blast dest: perm_sym)
+  by (blast dest: perm_sym)
 
 
 subsection {* Removing elements *}
@@ -115,29 +117,31 @@
   "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
 
 lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
-by (induct ys, auto)
+  by (induct ys) auto
 
 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
-by (induct l, auto)
+  by (induct l) auto
 
-lemma multiset_of_remove[simp]: 
-  "multiset_of (remove a x) = multiset_of x - {#a#}"
-  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
+lemma multiset_of_remove[simp]:
+    "multiset_of (remove a x) = multiset_of x - {#a#}"
+  apply (induct x)
+   apply (auto simp: multiset_eq_conv_count_eq)
+  done
 
 
 text {* \medskip Congruence rule *}
 
 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
-by (erule perm.induct, auto)
+  by (erule perm.induct) auto
 
 lemma remove_hd [simp]: "remove z (z # xs) = xs"
   by auto
 
 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
-by (drule_tac z = z in perm_remove_perm, auto)
+  by (drule_tac z = z in perm_remove_perm) auto
 
 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
-by (blast intro: cons_perm_imp_perm)
+  by (blast intro: cons_perm_imp_perm)
 
 lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   apply (induct zs rule: rev_induct)
@@ -146,7 +150,7 @@
   done
 
 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
-by (blast intro: append_perm_imp_perm perm_append1)
+  by (blast intro: append_perm_imp_perm perm_append1)
 
 lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
   apply (safe intro!: perm_append2)
@@ -157,20 +161,20 @@
   done
 
 lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
-  apply (rule iffI) 
-  apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
-  apply (erule rev_mp, rule_tac x=ys in spec) 
-  apply (induct_tac xs, auto) 
-  apply (erule_tac x = "remove a x" in allE, drule sym, simp) 
-  apply (subgoal_tac "a \<in> set x") 
-  apply (drule_tac z=a in perm.Cons) 
-  apply (erule perm.trans, rule perm_sym, erule perm_remove) 
+  apply (rule iffI)
+  apply (erule_tac [2] perm.induct, simp_all add: union_ac)
+  apply (erule rev_mp, rule_tac x=ys in spec)
+  apply (induct_tac xs, auto)
+  apply (erule_tac x = "remove a x" in allE, drule sym, simp)
+  apply (subgoal_tac "a \<in> set x")
+  apply (drule_tac z=a in perm.Cons)
+  apply (erule perm.trans, rule perm_sym, erule perm_remove)
   apply (drule_tac f=set_of in arg_cong, simp)
   done
 
-lemma multiset_of_le_perm_append: 
-  "(multiset_of xs \<le># multiset_of ys) = (\<exists> zs. xs @ zs <~~> ys)"; 
-  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
+lemma multiset_of_le_perm_append:
+    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)";
+  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   apply (insert surj_multiset_of, drule surjD)
   apply (blast intro: sym)+
   done
diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Norbert Voelker
 *)
 
-header {* Instantiation of order classes for product types *}
+header {* Order on product types *}
 
 theory Product_ord
 imports Main
diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Zorn.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -42,18 +42,20 @@
 
 subsection{*Mathematical Preamble*}
 
-lemma Union_lemma0: "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
-by blast
+lemma Union_lemma0:
+    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
+  by blast
 
 
 text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
+
 lemma Abrial_axiom1: "x \<subseteq> succ S x"
-apply (unfold succ_def)
-apply (rule split_if [THEN iffD2])
-apply (auto simp add: super_def maxchain_def psubset_def)
-apply (rule swap, assumption)
-apply (rule someI2, blast+)
-done
+  apply (unfold succ_def)
+  apply (rule split_if [THEN iffD2])
+  apply (auto simp add: super_def maxchain_def psubset_def)
+  apply (rule swap, assumption)
+  apply (rule someI2, blast+)
+  done
 
 lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
 
@@ -62,79 +64,77 @@
              !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
              !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
           ==> P(n)"
-apply (erule TFin.induct, blast+)
-done
+  apply (erule TFin.induct)
+   apply blast+
+  done
 
 lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
-apply (erule subset_trans)
-apply (rule Abrial_axiom1)
-done
+  apply (erule subset_trans)
+  apply (rule Abrial_axiom1)
+  done
 
 text{*Lemma 1 of section 3.1*}
 lemma TFin_linear_lemma1:
      "[| n \<in> TFin S;  m \<in> TFin S;
          \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
       |] ==> n \<subseteq> m | succ S m \<subseteq> n"
-apply (erule TFin_induct)
-apply (erule_tac [2] Union_lemma0) (*or just blast*)
-apply (blast del: subsetI intro: succ_trans)
-done
+  apply (erule TFin_induct)
+   apply (erule_tac [2] Union_lemma0)
+  apply (blast del: subsetI intro: succ_trans)
+  done
 
 text{* Lemma 2 of section 3.2 *}
 lemma TFin_linear_lemma2:
      "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
-apply (erule TFin_induct)
-apply (rule impI [THEN ballI])
-txt{*case split using @{text TFin_linear_lemma1}*}
-apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
-       assumption+)
-apply (drule_tac x = n in bspec, assumption)
-apply (blast del: subsetI intro: succ_trans, blast)
-txt{*second induction step*}
-apply (rule impI [THEN ballI])
-apply (rule Union_lemma0 [THEN disjE])
-apply (rule_tac [3] disjI2)
- prefer 2 apply blast
-apply (rule ballI)
-apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
-       assumption+, auto)
-apply (blast intro!: Abrial_axiom1 [THEN subsetD])
-done
+  apply (erule TFin_induct)
+   apply (rule impI [THEN ballI])
+   txt{*case split using @{text TFin_linear_lemma1}*}
+   apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
+     assumption+)
+    apply (drule_tac x = n in bspec, assumption)
+    apply (blast del: subsetI intro: succ_trans, blast)
+  txt{*second induction step*}
+  apply (rule impI [THEN ballI])
+  apply (rule Union_lemma0 [THEN disjE])
+    apply (rule_tac [3] disjI2)
+    prefer 2 apply blast
+   apply (rule ballI)
+   apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
+     assumption+, auto)
+  apply (blast intro!: Abrial_axiom1 [THEN subsetD])
+  done
 
 text{*Re-ordering the premises of Lemma 2*}
 lemma TFin_subsetD:
      "[| n \<subseteq> m;  m \<in> TFin S;  n \<in> TFin S |] ==> n=m | succ S n \<subseteq> m"
-apply (rule TFin_linear_lemma2 [rule_format])
-apply (assumption+)
-done
+  by (rule TFin_linear_lemma2 [rule_format])
 
 text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
 lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
-apply (rule disjE)
-apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
-apply (assumption+, erule disjI2)
-apply (blast del: subsetI
-             intro: subsetI Abrial_axiom1 [THEN subset_trans])
-done
+  apply (rule disjE)
+    apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
+      apply (assumption+, erule disjI2)
+  apply (blast del: subsetI
+    intro: subsetI Abrial_axiom1 [THEN subset_trans])
+  done
 
 text{*Lemma 3 of section 3.3*}
 lemma eq_succ_upper: "[| n \<in> TFin S;  m \<in> TFin S;  m = succ S m |] ==> n \<subseteq> m"
-apply (erule TFin_induct)
-apply (drule TFin_subsetD)
-apply (assumption+, force, blast)
-done
+  apply (erule TFin_induct)
+   apply (drule TFin_subsetD)
+     apply (assumption+, force, blast)
+  done
 
 text{*Property 3.3 of section 3.3*}
 lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
-apply (rule iffI)
-apply (rule Union_upper [THEN equalityI])
-apply (rule_tac [2] eq_succ_upper [THEN Union_least])
-apply (assumption+)
-apply (erule ssubst)
-apply (rule Abrial_axiom1 [THEN equalityI])
-apply (blast del: subsetI
-             intro: subsetI TFin_UnionI TFin.succI)
-done
+  apply (rule iffI)
+   apply (rule Union_upper [THEN equalityI])
+    apply (rule_tac [2] eq_succ_upper [THEN Union_least])
+      apply (assumption+)
+  apply (erule ssubst)
+  apply (rule Abrial_axiom1 [THEN equalityI])
+  apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI)
+  done
 
 subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
 
@@ -142,60 +142,58 @@
  the subset relation!*}
 
 lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
-by (unfold chain_def, auto)
+  by (unfold chain_def) auto
 
 lemma super_subset_chain: "super S c \<subseteq> chain S"
-by (unfold super_def, fast)
+  by (unfold super_def) blast
 
 lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S"
-by (unfold maxchain_def, fast)
+  by (unfold maxchain_def) blast
 
 lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
-by (unfold super_def maxchain_def, auto)
+  by (unfold super_def maxchain_def) auto
 
 lemma select_super: "c \<in> chain S - maxchain S ==>
-                          (@c'. c': super S c): super S c"
-apply (erule mem_super_Ex [THEN exE])
-apply (rule someI2, auto)
-done
+                          (\<some>c'. c': super S c): super S c"
+  apply (erule mem_super_Ex [THEN exE])
+  apply (rule someI2, auto)
+  done
 
 lemma select_not_equals: "c \<in> chain S - maxchain S ==>
-                          (@c'. c': super S c) \<noteq> c"
-apply (rule notI)
-apply (drule select_super)
-apply (simp add: super_def psubset_def)
-done
+                          (\<some>c'. c': super S c) \<noteq> c"
+  apply (rule notI)
+  apply (drule select_super)
+  apply (simp add: super_def psubset_def)
+  done
 
-lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (@c'. c': super S c)"
-apply (unfold succ_def)
-apply (fast intro!: if_not_P)
-done
+lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
+  by (unfold succ_def) (blast intro!: if_not_P)
 
 lemma succ_not_equals: "c \<in> chain S - maxchain S ==> succ S c \<noteq> c"
-apply (frule succI3)
-apply (simp (no_asm_simp))
-apply (rule select_not_equals, assumption)
-done
+  apply (frule succI3)
+  apply (simp (no_asm_simp))
+  apply (rule select_not_equals, assumption)
+  done
 
 lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
-apply (erule TFin_induct)
-apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
-apply (unfold chain_def)
-apply (rule CollectI, safe)
-apply (drule bspec, assumption)
-apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
-       blast+)
-done
+  apply (erule TFin_induct)
+   apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
+  apply (unfold chain_def)
+  apply (rule CollectI, safe)
+   apply (drule bspec, assumption)
+   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
+     blast+)
+  done
 
 theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
-apply (rule_tac x = "Union (TFin S) " in exI)
-apply (rule classical)
-apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
- prefer 2
- apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
-apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
-apply (drule DiffI [THEN succ_not_equals], blast+)
-done
+  apply (rule_tac x = "Union (TFin S) " in exI)
+  apply (rule classical)
+  apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
+   prefer 2
+   apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
+  apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
+  apply (drule DiffI [THEN succ_not_equals], blast+)
+  done
 
 
 subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
@@ -204,61 +202,61 @@
 lemma chain_extend:
     "[| c \<in> chain S; z \<in> S;
         \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
-by (unfold chain_def, blast)
+  by (unfold chain_def) blast
 
 lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
-by (unfold chain_def, auto)
+  by (unfold chain_def) auto
 
 lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
-by (unfold chain_def, auto)
+  by (unfold chain_def) auto
 
 lemma maxchain_Zorn:
      "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
-apply (rule ccontr)
-apply (simp add: maxchain_def)
-apply (erule conjE)
-apply (subgoal_tac " ({u} Un c) \<in> super S c")
-apply simp
-apply (unfold super_def psubset_def)
-apply (blast intro: chain_extend dest: chain_Union_upper)
-done
+  apply (rule ccontr)
+  apply (simp add: maxchain_def)
+  apply (erule conjE)
+  apply (subgoal_tac " ({u} Un c) \<in> super S c")
+   apply simp
+  apply (unfold super_def psubset_def)
+  apply (blast intro: chain_extend dest: chain_Union_upper)
+  done
 
 theorem Zorn_Lemma:
-     "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
-apply (cut_tac Hausdorff maxchain_subset_chain)
-apply (erule exE)
-apply (drule subsetD, assumption)
-apply (drule bspec, assumption)
-apply (rule_tac x = "Union (c) " in bexI)
-apply (rule ballI, rule impI)
-apply (blast dest!: maxchain_Zorn, assumption)
-done
+    "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
+  apply (cut_tac Hausdorff maxchain_subset_chain)
+  apply (erule exE)
+  apply (drule subsetD, assumption)
+  apply (drule bspec, assumption)
+  apply (rule_tac x = "Union (c) " in bexI)
+   apply (rule ballI, rule impI)
+   apply (blast dest!: maxchain_Zorn, assumption)
+  done
 
 subsection{*Alternative version of Zorn's Lemma*}
 
 lemma Zorn_Lemma2:
-     "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
-      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
-apply (cut_tac Hausdorff maxchain_subset_chain)
-apply (erule exE)
-apply (drule subsetD, assumption)
-apply (drule bspec, assumption, erule bexE)
-apply (rule_tac x = y in bexI)
- prefer 2 apply assumption
-apply clarify
-apply (rule ccontr)
-apply (frule_tac z = x in chain_extend)
-apply (assumption, blast)
-apply (unfold maxchain_def super_def psubset_def)
-apply (blast elim!: equalityCE)
-done
+  "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
+    ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
+  apply (cut_tac Hausdorff maxchain_subset_chain)
+  apply (erule exE)
+  apply (drule subsetD, assumption)
+  apply (drule bspec, assumption, erule bexE)
+  apply (rule_tac x = y in bexI)
+   prefer 2 apply assumption
+  apply clarify
+  apply (rule ccontr)
+  apply (frule_tac z = x in chain_extend)
+    apply (assumption, blast)
+  apply (unfold maxchain_def super_def psubset_def)
+  apply (blast elim!: equalityCE)
+  done
 
 text{*Various other lemmas*}
 
 lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
-by (unfold chain_def, blast)
+  by (unfold chain_def) blast
 
 lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
-by (unfold chain_def, blast)
+  by (unfold chain_def) blast
 
 end