tuned presentation;
authorwenzelm
Wed Aug 31 15:46:37 2005 +0200 (2005-08-31)
changeset 172003a4d03d1a31b
parent 17199 59c1bfc81d91
child 17201 3bdf1dfcdee4
tuned presentation;
src/HOL/Library/Char_ord.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:36 2005 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Aug 31 15:46:37 2005 +0200
     1.3 @@ -3,39 +3,39 @@
     1.4      Author:     Norbert Voelker
     1.5  *)
     1.6  
     1.7 -header {* Instantiation of order classes type char *}
     1.8 +header {* Order on characters *}
     1.9  
    1.10  theory Char_ord
    1.11  imports Product_ord
    1.12  begin
    1.13  
    1.14 -text {* Conversions between nibbles and integers in [0..15]. *} 
    1.15 +text {* Conversions between nibbles and integers in [0..15]. *}
    1.16  
    1.17 -consts 
    1.18 +consts
    1.19    nibble_to_int:: "nibble \<Rightarrow> int"
    1.20    int_to_nibble:: "int \<Rightarrow> nibble"
    1.21  
    1.22 -primrec 
    1.23 -  "nibble_to_int Nibble0 = 0"  
    1.24 -  "nibble_to_int Nibble1 = 1" 
    1.25 -  "nibble_to_int Nibble2 = 2" 
    1.26 -  "nibble_to_int Nibble3 = 3" 
    1.27 -  "nibble_to_int Nibble4 = 4" 
    1.28 -  "nibble_to_int Nibble5 = 5" 
    1.29 -  "nibble_to_int Nibble6 = 6" 
    1.30 -  "nibble_to_int Nibble7 = 7" 
    1.31 -  "nibble_to_int Nibble8 = 8" 
    1.32 -  "nibble_to_int Nibble9 = 9" 
    1.33 -  "nibble_to_int NibbleA = 10" 
    1.34 -  "nibble_to_int NibbleB = 11" 
    1.35 -  "nibble_to_int NibbleC = 12" 
    1.36 -  "nibble_to_int NibbleD = 13" 
    1.37 -  "nibble_to_int NibbleE = 14" 
    1.38 +primrec
    1.39 +  "nibble_to_int Nibble0 = 0"
    1.40 +  "nibble_to_int Nibble1 = 1"
    1.41 +  "nibble_to_int Nibble2 = 2"
    1.42 +  "nibble_to_int Nibble3 = 3"
    1.43 +  "nibble_to_int Nibble4 = 4"
    1.44 +  "nibble_to_int Nibble5 = 5"
    1.45 +  "nibble_to_int Nibble6 = 6"
    1.46 +  "nibble_to_int Nibble7 = 7"
    1.47 +  "nibble_to_int Nibble8 = 8"
    1.48 +  "nibble_to_int Nibble9 = 9"
    1.49 +  "nibble_to_int NibbleA = 10"
    1.50 +  "nibble_to_int NibbleB = 11"
    1.51 +  "nibble_to_int NibbleC = 12"
    1.52 +  "nibble_to_int NibbleD = 13"
    1.53 +  "nibble_to_int NibbleE = 14"
    1.54    "nibble_to_int NibbleF = 15"
    1.55  
    1.56 -defs 
    1.57 -  int_to_nibble_def:  
    1.58 -    "int_to_nibble x \<equiv> (let y = x mod 16 in 
    1.59 +defs
    1.60 +  int_to_nibble_def:
    1.61 +    "int_to_nibble x \<equiv> (let y = x mod 16 in
    1.62         if y = 0 then Nibble0 else
    1.63         if y = 1 then Nibble1 else
    1.64         if y = 2 then Nibble2 else
    1.65 @@ -54,46 +54,54 @@
    1.66         NibbleF)"
    1.67  
    1.68  lemma int_to_nibble_nibble_to_int: "int_to_nibble(nibble_to_int x) = x"
    1.69 -  by (case_tac x, auto simp: int_to_nibble_def Let_def)
    1.70 +  by (cases x) (auto simp: int_to_nibble_def Let_def)
    1.71  
    1.72  lemma inj_nibble_to_int: "inj nibble_to_int"
    1.73 -  by (rule inj_on_inverseI, rule int_to_nibble_nibble_to_int)
    1.74 +  by (rule inj_on_inverseI) (rule int_to_nibble_nibble_to_int)
    1.75  
    1.76  lemmas nibble_to_int_eq = inj_nibble_to_int [THEN inj_eq]
    1.77  
    1.78  lemma nibble_to_int_ge_0: "0 \<le> nibble_to_int x"
    1.79 -  by (case_tac x, auto)
    1.80 +  by (cases x) auto
    1.81  
    1.82  lemma nibble_to_int_less_16: "nibble_to_int x < 16"
    1.83 -  by (case_tac x, auto)
    1.84 +  by (cases x) auto
    1.85  
    1.86  text {* Conversion between chars and int pairs. *}
    1.87  
    1.88 -consts 
    1.89 +consts
    1.90    char_to_int_pair :: "char \<Rightarrow> int \<times> int"
    1.91  primrec
    1.92 -  "char_to_int_pair(Char a b) = (nibble_to_int a, nibble_to_int b)" 
    1.93 +  "char_to_int_pair (Char a b) = (nibble_to_int a, nibble_to_int b)"
    1.94  
    1.95  lemma inj_char_to_int_pair: "inj char_to_int_pair"
    1.96 -  by (rule inj_onI, case_tac x, case_tac y, auto simp: nibble_to_int_eq)
    1.97 +  apply (rule inj_onI)
    1.98 +  apply (case_tac x, case_tac y)
    1.99 +  apply (auto simp: nibble_to_int_eq)
   1.100 +  done
   1.101  
   1.102  lemmas char_to_int_pair_eq = inj_char_to_int_pair [THEN inj_eq]
   1.103  
   1.104 -text {* Instantiation of order classes *} 
   1.105 +text {* Instantiation of order classes *}
   1.106  
   1.107  instance char :: ord ..
   1.108  
   1.109  defs (overloaded)
   1.110 -  char_le_def:  "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)" 
   1.111 -  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)" 
   1.112 +  char_le_def: "c \<le> d \<equiv> (char_to_int_pair c \<le> char_to_int_pair d)"
   1.113 +  char_less_def: "c < d \<equiv> (char_to_int_pair c < char_to_int_pair d)"
   1.114  
   1.115  lemmas char_ord_defs = char_less_def char_le_def
   1.116  
   1.117 -instance char::order
   1.118 -  apply (intro_classes, unfold char_ord_defs)
   1.119 -  by (auto simp: char_to_int_pair_eq order_less_le)
   1.120 +instance char :: order
   1.121 +  apply intro_classes
   1.122 +     apply (unfold char_ord_defs)
   1.123 +     apply (auto simp: char_to_int_pair_eq order_less_le)
   1.124 +  done
   1.125  
   1.126  instance char::linorder
   1.127 -  by (intro_classes, unfold char_le_def, auto)
   1.128 +  apply intro_classes
   1.129 +  apply (unfold char_le_def)
   1.130 +  apply auto
   1.131 +  done
   1.132  
   1.133 -end
   1.134 \ No newline at end of file
   1.135 +end
     2.1 --- a/src/HOL/Library/List_lexord.thy	Wed Aug 31 15:46:36 2005 +0200
     2.2 +++ b/src/HOL/Library/List_lexord.thy	Wed Aug 31 15:46:37 2005 +0200
     2.3 @@ -3,51 +3,54 @@
     2.4      Author:     Norbert Voelker
     2.5  *)
     2.6  
     2.7 -header {* Instantiation of order classes for lexord on lists *}
     2.8 +header {* Lexicographic order on lists *}
     2.9  
    2.10  theory List_lexord
    2.11  imports Main
    2.12  begin
    2.13  
    2.14  instance list :: (ord) ord ..
    2.15 -defs(overloaded)
    2.16 -  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)" 
    2.17 -  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs,ys) \<in> lexord {(u,v). u < v}"
    2.18 +defs (overloaded)
    2.19 +  list_le_def:  "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
    2.20 +  list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}"
    2.21  
    2.22  lemmas list_ord_defs = list_less_def list_le_def
    2.23  
    2.24 -instance list::(order)order
    2.25 +instance list :: (order) order
    2.26    apply (intro_classes, unfold list_ord_defs)
    2.27 -  apply (rule disjI2, safe)
    2.28 -  apply (blast intro: lexord_trans transI order_less_trans)
    2.29 +     apply (rule disjI2, safe)
    2.30 +    apply (blast intro: lexord_trans transI order_less_trans)
    2.31 +   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    2.32 +    apply simp
    2.33 +   apply (blast intro: lexord_trans transI order_less_trans)
    2.34    apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    2.35    apply simp
    2.36 -  apply (blast intro: lexord_trans transI order_less_trans)
    2.37 -  apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])
    2.38 -  apply simp
    2.39 -  by assumption
    2.40 +  apply assumption
    2.41 +  done
    2.42  
    2.43  instance list::(linorder)linorder
    2.44    apply (intro_classes, unfold list_le_def list_less_def, safe)
    2.45 -  apply (cut_tac x="x" and y="y" and  r = "{(a,b). a < b}"  in lexord_linear)
    2.46 -  by (force, simp)
    2.47 +  apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    2.48 +   apply force
    2.49 +  apply simp
    2.50 +  done
    2.51  
    2.52 -lemma not_less_Nil[simp]: "~(x < [])";
    2.53 -  by (unfold list_less_def, simp);
    2.54 +lemma not_less_Nil[simp]: "~(x < [])"
    2.55 +  by (unfold list_less_def) simp
    2.56  
    2.57 -lemma Nil_less_Cons[simp]: "[] < a # x";
    2.58 -  by (unfold list_less_def, simp);
    2.59 +lemma Nil_less_Cons[simp]: "[] < a # x"
    2.60 +  by (unfold list_less_def) simp
    2.61  
    2.62 -lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)";
    2.63 -  by (unfold list_less_def, simp);
    2.64 +lemma Cons_less_Cons[simp]: "(a # x < b # y) = (a < b | a = b & x < y)"
    2.65 +  by (unfold list_less_def) simp
    2.66  
    2.67 -lemma le_Nil[simp]: "(x <= [])   = (x = [])";
    2.68 -  by (unfold list_ord_defs, case_tac x, auto);
    2.69 +lemma le_Nil[simp]: "(x <= []) = (x = [])"
    2.70 +  by (unfold list_ord_defs, cases x) auto
    2.71  
    2.72 -lemma Nil_le_Cons[simp]: "([] <= x)";
    2.73 -  by (unfold list_ord_defs, case_tac x, auto);
    2.74 +lemma Nil_le_Cons [simp]: "([] <= x)"
    2.75 +  by (unfold list_ord_defs, cases x) auto
    2.76  
    2.77 -lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)";
    2.78 -  by (unfold list_ord_defs, auto);
    2.79 +lemma Cons_le_Cons[simp]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
    2.80 +  by (unfold list_ord_defs) auto
    2.81  
    2.82 -end
    2.83 \ No newline at end of file
    2.84 +end
     3.1 --- a/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:36 2005 +0200
     3.2 +++ b/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:37 2005 +0200
     3.3 @@ -52,7 +52,7 @@
     3.4    Zero_multiset_def [simp]: "0 == {#}"
     3.5    size_def: "size M == setsum (count M) (set_of M)"
     3.6  
     3.7 -constdefs 
     3.8 +constdefs
     3.9   multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
    3.10   "multiset_inter A B \<equiv> A - (A - B)"
    3.11  
    3.12 @@ -109,7 +109,7 @@
    3.13  lemmas union_ac = union_assoc union_commute union_lcomm
    3.14  
    3.15  instance multiset :: (type) comm_monoid_add
    3.16 -proof 
    3.17 +proof
    3.18    fix a b c :: "'a multiset"
    3.19    show "(a + b) + c = a + (b + c)" by (rule union_assoc)
    3.20    show "a + b = b + a" by (rule union_commute)
    3.21 @@ -254,11 +254,11 @@
    3.22    by (simp add: multiset_inter_def min_def)
    3.23  
    3.24  lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
    3.25 -  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
    3.26 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
    3.27      min_max.below_inf.inf_commute)
    3.28  
    3.29  lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
    3.30 -  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
    3.31 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
    3.32      min_max.below_inf.inf_assoc)
    3.33  
    3.34  lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
    3.35 @@ -270,7 +270,7 @@
    3.36    multiset_inter_left_commute
    3.37  
    3.38  lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
    3.39 -  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def 
    3.40 +  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
    3.41      split: split_if_asm)
    3.42    apply clarsimp
    3.43    apply (erule_tac x = a in allE)
    3.44 @@ -345,7 +345,7 @@
    3.45       prefer 2
    3.46       apply (simp add: expand_fun_eq)
    3.47      apply (erule ssubst)
    3.48 -    apply (erule Abs_multiset_inverse [THEN subst]) 
    3.49 +    apply (erule Abs_multiset_inverse [THEN subst])
    3.50      apply (erule prem2 [unfolded defns, simplified])
    3.51      done
    3.52  qed
    3.53 @@ -728,7 +728,7 @@
    3.54  
    3.55  lemma union_upper1: "A <= A + (B::'a::order multiset)"
    3.56  proof -
    3.57 -  have "A + {#} <= A + B" by (blast intro: union_le_mono) 
    3.58 +  have "A + {#} <= A + B" by (blast intro: union_le_mono)
    3.59    thus ?thesis by simp
    3.60  qed
    3.61  
    3.62 @@ -736,63 +736,63 @@
    3.63  by (subst union_commute, rule union_upper1)
    3.64  
    3.65  
    3.66 -subsection {* Link with lists *} 
    3.67 +subsection {* Link with lists *}
    3.68  
    3.69 -consts 
    3.70 +consts
    3.71    multiset_of :: "'a list \<Rightarrow> 'a multiset"
    3.72  primrec
    3.73    "multiset_of [] = {#}"
    3.74    "multiset_of (a # x) = multiset_of x + {# a #}"
    3.75  
    3.76  lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
    3.77 -  by (induct_tac x, auto) 
    3.78 +  by (induct_tac x, auto)
    3.79  
    3.80  lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
    3.81    by (induct_tac x, auto)
    3.82  
    3.83  lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
    3.84 -  by (induct_tac x, auto) 
    3.85 +  by (induct_tac x, auto)
    3.86  
    3.87  lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
    3.88    by (induct xs) auto
    3.89  
    3.90 -lemma multiset_of_append[simp]: 
    3.91 +lemma multiset_of_append[simp]:
    3.92    "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
    3.93 -  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
    3.94 +  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac)
    3.95  
    3.96  lemma surj_multiset_of: "surj multiset_of"
    3.97 -  apply (unfold surj_def, rule allI) 
    3.98 -  apply (rule_tac M=y in multiset_induct, auto) 
    3.99 -  apply (rule_tac x = "x # xa" in exI, auto) 
   3.100 +  apply (unfold surj_def, rule allI)
   3.101 +  apply (rule_tac M=y in multiset_induct, auto)
   3.102 +  apply (rule_tac x = "x # xa" in exI, auto)
   3.103    done
   3.104  
   3.105  lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
   3.106 -  by (induct_tac x, auto)  
   3.107 +  by (induct_tac x, auto)
   3.108  
   3.109 -lemma distinct_count_atmost_1: 
   3.110 +lemma distinct_count_atmost_1:
   3.111     "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
   3.112     apply ( induct_tac x, simp, rule iffI, simp_all)
   3.113 -   apply (rule conjI)  
   3.114 -   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
   3.115 +   apply (rule conjI)
   3.116 +   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
   3.117     apply (erule_tac x=a in allE, simp, clarify)
   3.118 -   apply (erule_tac x=aa in allE, simp) 
   3.119 +   apply (erule_tac x=aa in allE, simp)
   3.120     done
   3.121  
   3.122 -lemma multiset_of_eq_setD: 
   3.123 +lemma multiset_of_eq_setD:
   3.124    "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
   3.125    by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
   3.126  
   3.127 -lemma set_eq_iff_multiset_of_eq_distinct: 
   3.128 -  "\<lbrakk>distinct x; distinct y\<rbrakk> 
   3.129 +lemma set_eq_iff_multiset_of_eq_distinct:
   3.130 +  "\<lbrakk>distinct x; distinct y\<rbrakk>
   3.131     \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
   3.132 -  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
   3.133 +  by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
   3.134  
   3.135 -lemma set_eq_iff_multiset_of_remdups_eq: 
   3.136 +lemma set_eq_iff_multiset_of_remdups_eq:
   3.137     "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   3.138 -  apply (rule iffI) 
   3.139 -  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
   3.140 -  apply (drule distinct_remdups[THEN distinct_remdups 
   3.141 -                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
   3.142 +  apply (rule iffI)
   3.143 +  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
   3.144 +  apply (drule distinct_remdups[THEN distinct_remdups
   3.145 +                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]])
   3.146    apply simp
   3.147    done
   3.148  
   3.149 @@ -800,61 +800,66 @@
   3.150   "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   3.151    by (induct xs) (auto simp: union_ac)
   3.152  
   3.153 -lemma count_filter: 
   3.154 +lemma count_filter:
   3.155    "count (multiset_of xs) x = length [y \<in> xs. y = x]"
   3.156    by (induct xs, auto)
   3.157  
   3.158  
   3.159  subsection {* Pointwise ordering induced by count *}
   3.160  
   3.161 -consts 
   3.162 +consts
   3.163    mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
   3.164  
   3.165 -syntax 
   3.166 -  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50) 
   3.167 -translations 
   3.168 +syntax
   3.169 +  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
   3.170 +translations
   3.171    "x \<le># y" == "mset_le x y"
   3.172  
   3.173 -defs 
   3.174 -  mset_le_def:   "xs \<le># ys  == (! a. count xs a \<le> count ys a)"
   3.175 +defs
   3.176 +  mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
   3.177  
   3.178  lemma mset_le_refl[simp]: "xs \<le># xs"
   3.179 -  by (unfold mset_le_def, auto) 
   3.180 +  by (unfold mset_le_def) auto
   3.181  
   3.182  lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
   3.183 -  by (unfold mset_le_def, fast intro: order_trans) 
   3.184 +  by (unfold mset_le_def) (fast intro: order_trans)
   3.185  
   3.186  lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
   3.187 -  apply (unfold mset_le_def) 
   3.188 -  apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 
   3.189 +  apply (unfold mset_le_def)
   3.190 +  apply (rule multiset_eq_conv_count_eq[THEN iffD2])
   3.191    apply (blast intro: order_antisym)
   3.192    done
   3.193  
   3.194 -lemma mset_le_exists_conv: 
   3.195 -  "(xs \<le># ys) = (? zs. ys = xs + zs)"
   3.196 -  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) 
   3.197 +lemma mset_le_exists_conv:
   3.198 +  "(xs \<le># ys) = (\<exists>zs. ys = xs + zs)"
   3.199 +  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI)
   3.200    apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   3.201    done
   3.202  
   3.203  lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
   3.204 -  by (unfold mset_le_def, auto) 
   3.205 +  by (unfold mset_le_def) auto
   3.206  
   3.207  lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
   3.208 -  by (unfold mset_le_def, auto) 
   3.209 +  by (unfold mset_le_def) auto
   3.210  
   3.211 -lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
   3.212 -  apply (unfold mset_le_def, auto) 
   3.213 +lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws"
   3.214 +  apply (unfold mset_le_def)
   3.215 +  apply auto
   3.216    apply (erule_tac x=a in allE)+
   3.217    apply auto
   3.218    done
   3.219  
   3.220  lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
   3.221 -  by (unfold mset_le_def, auto) 
   3.222 +  by (unfold mset_le_def) auto
   3.223  
   3.224  lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
   3.225 -  by (unfold mset_le_def, auto)
   3.226 +  by (unfold mset_le_def) auto
   3.227  
   3.228  lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
   3.229 -  by (induct_tac x, auto, rule mset_le_trans, auto)
   3.230 +  apply (induct x)
   3.231 +   apply auto
   3.232 +  apply (rule mset_le_trans)
   3.233 +   apply auto
   3.234 +  done
   3.235  
   3.236  end
     4.1 --- a/src/HOL/Library/Permutation.thy	Wed Aug 31 15:46:36 2005 +0200
     4.2 +++ b/src/HOL/Library/Permutation.thy	Wed Aug 31 15:46:37 2005 +0200
     4.3 @@ -24,20 +24,20 @@
     4.4      trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
     4.5  
     4.6  lemma perm_refl [iff]: "l <~~> l"
     4.7 -by (induct l, auto)
     4.8 +  by (induct l) auto
     4.9  
    4.10  
    4.11  subsection {* Some examples of rule induction on permutations *}
    4.12  
    4.13  lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
    4.14 -    -- {*the form of the premise lets the induction bind @{term xs} 
    4.15 +    -- {*the form of the premise lets the induction bind @{term xs}
    4.16           and @{term ys} *}
    4.17    apply (erule perm.induct)
    4.18       apply (simp_all (no_asm_simp))
    4.19    done
    4.20  
    4.21  lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    4.22 -by (insert xperm_empty_imp_aux, blast)
    4.23 +  using xperm_empty_imp_aux by blast
    4.24  
    4.25  
    4.26  text {*
    4.27 @@ -45,16 +45,16 @@
    4.28    *}
    4.29  
    4.30  lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    4.31 -by (erule perm.induct, simp_all)
    4.32 +  by (erule perm.induct) simp_all
    4.33  
    4.34  lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    4.35 -by (drule perm_length, auto)
    4.36 +  by (drule perm_length) auto
    4.37  
    4.38  lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    4.39 -by (erule perm.induct, auto)
    4.40 +  by (erule perm.induct) auto
    4.41  
    4.42  lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
    4.43 -by (erule perm.induct, auto)
    4.44 +  by (erule perm.induct) auto
    4.45  
    4.46  
    4.47  subsection {* Ways of making new permutations *}
    4.48 @@ -64,32 +64,34 @@
    4.49  *}
    4.50  
    4.51  lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
    4.52 -by (induct xs, auto)
    4.53 +  by (induct xs) auto
    4.54  
    4.55  lemma perm_append_swap: "xs @ ys <~~> ys @ xs"
    4.56 -  apply (induct xs, simp_all)
    4.57 +  apply (induct xs)
    4.58 +    apply simp_all
    4.59    apply (blast intro: perm_append_Cons)
    4.60    done
    4.61  
    4.62  lemma perm_append_single: "a # xs <~~> xs @ [a]"
    4.63 -  by (rule perm.trans [OF _ perm_append_swap], simp)
    4.64 +  by (rule perm.trans [OF _ perm_append_swap]) simp
    4.65  
    4.66  lemma perm_rev: "rev xs <~~> xs"
    4.67 -  apply (induct xs, simp_all)
    4.68 +  apply (induct xs)
    4.69 +   apply simp_all
    4.70    apply (blast intro!: perm_append_single intro: perm_sym)
    4.71    done
    4.72  
    4.73  lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"
    4.74 -by (induct l, auto)
    4.75 +  by (induct l) auto
    4.76  
    4.77  lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l"
    4.78 -by (blast intro!: perm_append_swap perm_append1)
    4.79 +  by (blast intro!: perm_append_swap perm_append1)
    4.80  
    4.81  
    4.82  subsection {* Further results *}
    4.83  
    4.84  lemma perm_empty [iff]: "([] <~~> xs) = (xs = [])"
    4.85 -by (blast intro: perm_empty_imp)
    4.86 +  by (blast intro: perm_empty_imp)
    4.87  
    4.88  lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    4.89    apply auto
    4.90 @@ -97,13 +99,13 @@
    4.91    done
    4.92  
    4.93  lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
    4.94 -by (erule perm.induct, auto)
    4.95 +  by (erule perm.induct) auto
    4.96  
    4.97  lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    4.98 -by (blast intro: perm_sing_imp)
    4.99 +  by (blast intro: perm_sing_imp)
   4.100  
   4.101  lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
   4.102 -by (blast dest: perm_sym)
   4.103 +  by (blast dest: perm_sym)
   4.104  
   4.105  
   4.106  subsection {* Removing elements *}
   4.107 @@ -115,29 +117,31 @@
   4.108    "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
   4.109  
   4.110  lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
   4.111 -by (induct ys, auto)
   4.112 +  by (induct ys) auto
   4.113  
   4.114  lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
   4.115 -by (induct l, auto)
   4.116 +  by (induct l) auto
   4.117  
   4.118 -lemma multiset_of_remove[simp]: 
   4.119 -  "multiset_of (remove a x) = multiset_of x - {#a#}"
   4.120 -  by (induct_tac x, auto simp: multiset_eq_conv_count_eq) 
   4.121 +lemma multiset_of_remove[simp]:
   4.122 +    "multiset_of (remove a x) = multiset_of x - {#a#}"
   4.123 +  apply (induct x)
   4.124 +   apply (auto simp: multiset_eq_conv_count_eq)
   4.125 +  done
   4.126  
   4.127  
   4.128  text {* \medskip Congruence rule *}
   4.129  
   4.130  lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
   4.131 -by (erule perm.induct, auto)
   4.132 +  by (erule perm.induct) auto
   4.133  
   4.134  lemma remove_hd [simp]: "remove z (z # xs) = xs"
   4.135    by auto
   4.136  
   4.137  lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
   4.138 -by (drule_tac z = z in perm_remove_perm, auto)
   4.139 +  by (drule_tac z = z in perm_remove_perm) auto
   4.140  
   4.141  lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   4.142 -by (blast intro: cons_perm_imp_perm)
   4.143 +  by (blast intro: cons_perm_imp_perm)
   4.144  
   4.145  lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   4.146    apply (induct zs rule: rev_induct)
   4.147 @@ -146,7 +150,7 @@
   4.148    done
   4.149  
   4.150  lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   4.151 -by (blast intro: append_perm_imp_perm perm_append1)
   4.152 +  by (blast intro: append_perm_imp_perm perm_append1)
   4.153  
   4.154  lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
   4.155    apply (safe intro!: perm_append2)
   4.156 @@ -157,20 +161,20 @@
   4.157    done
   4.158  
   4.159  lemma multiset_of_eq_perm: "(multiset_of xs = multiset_of ys) = (xs <~~> ys) "
   4.160 -  apply (rule iffI) 
   4.161 -  apply (erule_tac [2] perm.induct, simp_all add: union_ac) 
   4.162 -  apply (erule rev_mp, rule_tac x=ys in spec) 
   4.163 -  apply (induct_tac xs, auto) 
   4.164 -  apply (erule_tac x = "remove a x" in allE, drule sym, simp) 
   4.165 -  apply (subgoal_tac "a \<in> set x") 
   4.166 -  apply (drule_tac z=a in perm.Cons) 
   4.167 -  apply (erule perm.trans, rule perm_sym, erule perm_remove) 
   4.168 +  apply (rule iffI)
   4.169 +  apply (erule_tac [2] perm.induct, simp_all add: union_ac)
   4.170 +  apply (erule rev_mp, rule_tac x=ys in spec)
   4.171 +  apply (induct_tac xs, auto)
   4.172 +  apply (erule_tac x = "remove a x" in allE, drule sym, simp)
   4.173 +  apply (subgoal_tac "a \<in> set x")
   4.174 +  apply (drule_tac z=a in perm.Cons)
   4.175 +  apply (erule perm.trans, rule perm_sym, erule perm_remove)
   4.176    apply (drule_tac f=set_of in arg_cong, simp)
   4.177    done
   4.178  
   4.179 -lemma multiset_of_le_perm_append: 
   4.180 -  "(multiset_of xs \<le># multiset_of ys) = (\<exists> zs. xs @ zs <~~> ys)"; 
   4.181 -  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) 
   4.182 +lemma multiset_of_le_perm_append:
   4.183 +    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)";
   4.184 +  apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   4.185    apply (insert surj_multiset_of, drule surjD)
   4.186    apply (blast intro: sym)+
   4.187    done
     5.1 --- a/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:36 2005 +0200
     5.2 +++ b/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:37 2005 +0200
     5.3 @@ -3,7 +3,7 @@
     5.4      Author:     Norbert Voelker
     5.5  *)
     5.6  
     5.7 -header {* Instantiation of order classes for product types *}
     5.8 +header {* Order on product types *}
     5.9  
    5.10  theory Product_ord
    5.11  imports Main
     6.1 --- a/src/HOL/Library/Zorn.thy	Wed Aug 31 15:46:36 2005 +0200
     6.2 +++ b/src/HOL/Library/Zorn.thy	Wed Aug 31 15:46:37 2005 +0200
     6.3 @@ -42,18 +42,20 @@
     6.4  
     6.5  subsection{*Mathematical Preamble*}
     6.6  
     6.7 -lemma Union_lemma0: "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
     6.8 -by blast
     6.9 +lemma Union_lemma0:
    6.10 +    "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C)<=A | B \<subseteq> Union(C)"
    6.11 +  by blast
    6.12  
    6.13  
    6.14  text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
    6.15 +
    6.16  lemma Abrial_axiom1: "x \<subseteq> succ S x"
    6.17 -apply (unfold succ_def)
    6.18 -apply (rule split_if [THEN iffD2])
    6.19 -apply (auto simp add: super_def maxchain_def psubset_def)
    6.20 -apply (rule swap, assumption)
    6.21 -apply (rule someI2, blast+)
    6.22 -done
    6.23 +  apply (unfold succ_def)
    6.24 +  apply (rule split_if [THEN iffD2])
    6.25 +  apply (auto simp add: super_def maxchain_def psubset_def)
    6.26 +  apply (rule swap, assumption)
    6.27 +  apply (rule someI2, blast+)
    6.28 +  done
    6.29  
    6.30  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    6.31  
    6.32 @@ -62,79 +64,77 @@
    6.33               !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
    6.34               !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
    6.35            ==> P(n)"
    6.36 -apply (erule TFin.induct, blast+)
    6.37 -done
    6.38 +  apply (erule TFin.induct)
    6.39 +   apply blast+
    6.40 +  done
    6.41  
    6.42  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    6.43 -apply (erule subset_trans)
    6.44 -apply (rule Abrial_axiom1)
    6.45 -done
    6.46 +  apply (erule subset_trans)
    6.47 +  apply (rule Abrial_axiom1)
    6.48 +  done
    6.49  
    6.50  text{*Lemma 1 of section 3.1*}
    6.51  lemma TFin_linear_lemma1:
    6.52       "[| n \<in> TFin S;  m \<in> TFin S;
    6.53           \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
    6.54        |] ==> n \<subseteq> m | succ S m \<subseteq> n"
    6.55 -apply (erule TFin_induct)
    6.56 -apply (erule_tac [2] Union_lemma0) (*or just blast*)
    6.57 -apply (blast del: subsetI intro: succ_trans)
    6.58 -done
    6.59 +  apply (erule TFin_induct)
    6.60 +   apply (erule_tac [2] Union_lemma0)
    6.61 +  apply (blast del: subsetI intro: succ_trans)
    6.62 +  done
    6.63  
    6.64  text{* Lemma 2 of section 3.2 *}
    6.65  lemma TFin_linear_lemma2:
    6.66       "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
    6.67 -apply (erule TFin_induct)
    6.68 -apply (rule impI [THEN ballI])
    6.69 -txt{*case split using @{text TFin_linear_lemma1}*}
    6.70 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    6.71 -       assumption+)
    6.72 -apply (drule_tac x = n in bspec, assumption)
    6.73 -apply (blast del: subsetI intro: succ_trans, blast)
    6.74 -txt{*second induction step*}
    6.75 -apply (rule impI [THEN ballI])
    6.76 -apply (rule Union_lemma0 [THEN disjE])
    6.77 -apply (rule_tac [3] disjI2)
    6.78 - prefer 2 apply blast
    6.79 -apply (rule ballI)
    6.80 -apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    6.81 -       assumption+, auto)
    6.82 -apply (blast intro!: Abrial_axiom1 [THEN subsetD])
    6.83 -done
    6.84 +  apply (erule TFin_induct)
    6.85 +   apply (rule impI [THEN ballI])
    6.86 +   txt{*case split using @{text TFin_linear_lemma1}*}
    6.87 +   apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    6.88 +     assumption+)
    6.89 +    apply (drule_tac x = n in bspec, assumption)
    6.90 +    apply (blast del: subsetI intro: succ_trans, blast)
    6.91 +  txt{*second induction step*}
    6.92 +  apply (rule impI [THEN ballI])
    6.93 +  apply (rule Union_lemma0 [THEN disjE])
    6.94 +    apply (rule_tac [3] disjI2)
    6.95 +    prefer 2 apply blast
    6.96 +   apply (rule ballI)
    6.97 +   apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    6.98 +     assumption+, auto)
    6.99 +  apply (blast intro!: Abrial_axiom1 [THEN subsetD])
   6.100 +  done
   6.101  
   6.102  text{*Re-ordering the premises of Lemma 2*}
   6.103  lemma TFin_subsetD:
   6.104       "[| n \<subseteq> m;  m \<in> TFin S;  n \<in> TFin S |] ==> n=m | succ S n \<subseteq> m"
   6.105 -apply (rule TFin_linear_lemma2 [rule_format])
   6.106 -apply (assumption+)
   6.107 -done
   6.108 +  by (rule TFin_linear_lemma2 [rule_format])
   6.109  
   6.110  text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
   6.111  lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
   6.112 -apply (rule disjE)
   6.113 -apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   6.114 -apply (assumption+, erule disjI2)
   6.115 -apply (blast del: subsetI
   6.116 -             intro: subsetI Abrial_axiom1 [THEN subset_trans])
   6.117 -done
   6.118 +  apply (rule disjE)
   6.119 +    apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   6.120 +      apply (assumption+, erule disjI2)
   6.121 +  apply (blast del: subsetI
   6.122 +    intro: subsetI Abrial_axiom1 [THEN subset_trans])
   6.123 +  done
   6.124  
   6.125  text{*Lemma 3 of section 3.3*}
   6.126  lemma eq_succ_upper: "[| n \<in> TFin S;  m \<in> TFin S;  m = succ S m |] ==> n \<subseteq> m"
   6.127 -apply (erule TFin_induct)
   6.128 -apply (drule TFin_subsetD)
   6.129 -apply (assumption+, force, blast)
   6.130 -done
   6.131 +  apply (erule TFin_induct)
   6.132 +   apply (drule TFin_subsetD)
   6.133 +     apply (assumption+, force, blast)
   6.134 +  done
   6.135  
   6.136  text{*Property 3.3 of section 3.3*}
   6.137  lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
   6.138 -apply (rule iffI)
   6.139 -apply (rule Union_upper [THEN equalityI])
   6.140 -apply (rule_tac [2] eq_succ_upper [THEN Union_least])
   6.141 -apply (assumption+)
   6.142 -apply (erule ssubst)
   6.143 -apply (rule Abrial_axiom1 [THEN equalityI])
   6.144 -apply (blast del: subsetI
   6.145 -             intro: subsetI TFin_UnionI TFin.succI)
   6.146 -done
   6.147 +  apply (rule iffI)
   6.148 +   apply (rule Union_upper [THEN equalityI])
   6.149 +    apply (rule_tac [2] eq_succ_upper [THEN Union_least])
   6.150 +      apply (assumption+)
   6.151 +  apply (erule ssubst)
   6.152 +  apply (rule Abrial_axiom1 [THEN equalityI])
   6.153 +  apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI)
   6.154 +  done
   6.155  
   6.156  subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
   6.157  
   6.158 @@ -142,60 +142,58 @@
   6.159   the subset relation!*}
   6.160  
   6.161  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
   6.162 -by (unfold chain_def, auto)
   6.163 +  by (unfold chain_def) auto
   6.164  
   6.165  lemma super_subset_chain: "super S c \<subseteq> chain S"
   6.166 -by (unfold super_def, fast)
   6.167 +  by (unfold super_def) blast
   6.168  
   6.169  lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S"
   6.170 -by (unfold maxchain_def, fast)
   6.171 +  by (unfold maxchain_def) blast
   6.172  
   6.173  lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> ? d. d \<in> super S c"
   6.174 -by (unfold super_def maxchain_def, auto)
   6.175 +  by (unfold super_def maxchain_def) auto
   6.176  
   6.177  lemma select_super: "c \<in> chain S - maxchain S ==>
   6.178 -                          (@c'. c': super S c): super S c"
   6.179 -apply (erule mem_super_Ex [THEN exE])
   6.180 -apply (rule someI2, auto)
   6.181 -done
   6.182 +                          (\<some>c'. c': super S c): super S c"
   6.183 +  apply (erule mem_super_Ex [THEN exE])
   6.184 +  apply (rule someI2, auto)
   6.185 +  done
   6.186  
   6.187  lemma select_not_equals: "c \<in> chain S - maxchain S ==>
   6.188 -                          (@c'. c': super S c) \<noteq> c"
   6.189 -apply (rule notI)
   6.190 -apply (drule select_super)
   6.191 -apply (simp add: super_def psubset_def)
   6.192 -done
   6.193 +                          (\<some>c'. c': super S c) \<noteq> c"
   6.194 +  apply (rule notI)
   6.195 +  apply (drule select_super)
   6.196 +  apply (simp add: super_def psubset_def)
   6.197 +  done
   6.198  
   6.199 -lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (@c'. c': super S c)"
   6.200 -apply (unfold succ_def)
   6.201 -apply (fast intro!: if_not_P)
   6.202 -done
   6.203 +lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
   6.204 +  by (unfold succ_def) (blast intro!: if_not_P)
   6.205  
   6.206  lemma succ_not_equals: "c \<in> chain S - maxchain S ==> succ S c \<noteq> c"
   6.207 -apply (frule succI3)
   6.208 -apply (simp (no_asm_simp))
   6.209 -apply (rule select_not_equals, assumption)
   6.210 -done
   6.211 +  apply (frule succI3)
   6.212 +  apply (simp (no_asm_simp))
   6.213 +  apply (rule select_not_equals, assumption)
   6.214 +  done
   6.215  
   6.216  lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
   6.217 -apply (erule TFin_induct)
   6.218 -apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
   6.219 -apply (unfold chain_def)
   6.220 -apply (rule CollectI, safe)
   6.221 -apply (drule bspec, assumption)
   6.222 -apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
   6.223 -       blast+)
   6.224 -done
   6.225 +  apply (erule TFin_induct)
   6.226 +   apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
   6.227 +  apply (unfold chain_def)
   6.228 +  apply (rule CollectI, safe)
   6.229 +   apply (drule bspec, assumption)
   6.230 +   apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
   6.231 +     blast+)
   6.232 +  done
   6.233  
   6.234  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   6.235 -apply (rule_tac x = "Union (TFin S) " in exI)
   6.236 -apply (rule classical)
   6.237 -apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   6.238 - prefer 2
   6.239 - apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
   6.240 -apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   6.241 -apply (drule DiffI [THEN succ_not_equals], blast+)
   6.242 -done
   6.243 +  apply (rule_tac x = "Union (TFin S) " in exI)
   6.244 +  apply (rule classical)
   6.245 +  apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   6.246 +   prefer 2
   6.247 +   apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
   6.248 +  apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   6.249 +  apply (drule DiffI [THEN succ_not_equals], blast+)
   6.250 +  done
   6.251  
   6.252  
   6.253  subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
   6.254 @@ -204,61 +202,61 @@
   6.255  lemma chain_extend:
   6.256      "[| c \<in> chain S; z \<in> S;
   6.257          \<forall>x \<in> c. x<=(z:: 'a set) |] ==> {z} Un c \<in> chain S"
   6.258 -by (unfold chain_def, blast)
   6.259 +  by (unfold chain_def) blast
   6.260  
   6.261  lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
   6.262 -by (unfold chain_def, auto)
   6.263 +  by (unfold chain_def) auto
   6.264  
   6.265  lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
   6.266 -by (unfold chain_def, auto)
   6.267 +  by (unfold chain_def) auto
   6.268  
   6.269  lemma maxchain_Zorn:
   6.270       "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
   6.271 -apply (rule ccontr)
   6.272 -apply (simp add: maxchain_def)
   6.273 -apply (erule conjE)
   6.274 -apply (subgoal_tac " ({u} Un c) \<in> super S c")
   6.275 -apply simp
   6.276 -apply (unfold super_def psubset_def)
   6.277 -apply (blast intro: chain_extend dest: chain_Union_upper)
   6.278 -done
   6.279 +  apply (rule ccontr)
   6.280 +  apply (simp add: maxchain_def)
   6.281 +  apply (erule conjE)
   6.282 +  apply (subgoal_tac " ({u} Un c) \<in> super S c")
   6.283 +   apply simp
   6.284 +  apply (unfold super_def psubset_def)
   6.285 +  apply (blast intro: chain_extend dest: chain_Union_upper)
   6.286 +  done
   6.287  
   6.288  theorem Zorn_Lemma:
   6.289 -     "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
   6.290 -apply (cut_tac Hausdorff maxchain_subset_chain)
   6.291 -apply (erule exE)
   6.292 -apply (drule subsetD, assumption)
   6.293 -apply (drule bspec, assumption)
   6.294 -apply (rule_tac x = "Union (c) " in bexI)
   6.295 -apply (rule ballI, rule impI)
   6.296 -apply (blast dest!: maxchain_Zorn, assumption)
   6.297 -done
   6.298 +    "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
   6.299 +  apply (cut_tac Hausdorff maxchain_subset_chain)
   6.300 +  apply (erule exE)
   6.301 +  apply (drule subsetD, assumption)
   6.302 +  apply (drule bspec, assumption)
   6.303 +  apply (rule_tac x = "Union (c) " in bexI)
   6.304 +   apply (rule ballI, rule impI)
   6.305 +   apply (blast dest!: maxchain_Zorn, assumption)
   6.306 +  done
   6.307  
   6.308  subsection{*Alternative version of Zorn's Lemma*}
   6.309  
   6.310  lemma Zorn_Lemma2:
   6.311 -     "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   6.312 -      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   6.313 -apply (cut_tac Hausdorff maxchain_subset_chain)
   6.314 -apply (erule exE)
   6.315 -apply (drule subsetD, assumption)
   6.316 -apply (drule bspec, assumption, erule bexE)
   6.317 -apply (rule_tac x = y in bexI)
   6.318 - prefer 2 apply assumption
   6.319 -apply clarify
   6.320 -apply (rule ccontr)
   6.321 -apply (frule_tac z = x in chain_extend)
   6.322 -apply (assumption, blast)
   6.323 -apply (unfold maxchain_def super_def psubset_def)
   6.324 -apply (blast elim!: equalityCE)
   6.325 -done
   6.326 +  "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   6.327 +    ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   6.328 +  apply (cut_tac Hausdorff maxchain_subset_chain)
   6.329 +  apply (erule exE)
   6.330 +  apply (drule subsetD, assumption)
   6.331 +  apply (drule bspec, assumption, erule bexE)
   6.332 +  apply (rule_tac x = y in bexI)
   6.333 +   prefer 2 apply assumption
   6.334 +  apply clarify
   6.335 +  apply (rule ccontr)
   6.336 +  apply (frule_tac z = x in chain_extend)
   6.337 +    apply (assumption, blast)
   6.338 +  apply (unfold maxchain_def super_def psubset_def)
   6.339 +  apply (blast elim!: equalityCE)
   6.340 +  done
   6.341  
   6.342  text{*Various other lemmas*}
   6.343  
   6.344  lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   6.345 -by (unfold chain_def, blast)
   6.346 +  by (unfold chain_def) blast
   6.347  
   6.348  lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   6.349 -by (unfold chain_def, blast)
   6.350 +  by (unfold chain_def) blast
   6.351  
   6.352  end