--- 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
--- 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
--- 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
--- 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
--- 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
--- 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