--- a/src/HOL/Library/ExecutableSet.thy Thu Jan 25 09:32:35 2007 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Thu Jan 25 09:32:36 2007 +0100
@@ -13,26 +13,6 @@
instance set :: (eq) eq ..
-definition
- minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "minus_set xs ys = ys - xs"
-
-lemma [code inline]:
- "op - = (\<lambda>xs ys. minus_set ys xs)"
- unfolding minus_set_def ..
-
-definition
- subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "subset = op \<subseteq>"
-
-lemmas [symmetric, code inline] = subset_def
-
-definition
- strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "strict_subset = op \<subset>"
-
-lemmas [symmetric, code inline] = strict_subset_def
-
lemma [code target: Set]:
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
by blast
@@ -42,12 +22,12 @@
by blast
lemma [code func]:
- "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- unfolding subset_def Set.subset_def ..
+ "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ unfolding subset_def ..
lemma [code func]:
- "strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B"
- unfolding subset_def strict_subset_def by blast
+ "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
+ by blast
lemma [code]:
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
@@ -81,10 +61,8 @@
and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
unfolding member_def by (induct xs) simp_all
-consts
- drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-primrec
+fun
+ drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"drop_first f [] = []"
"drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
declare drop_first.simps [code del]
@@ -215,12 +193,16 @@
"set (intersect xs ys) = set xs \<inter> set ys"
unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+definition
+ subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "subtract' = flip subtract"
+
lemma iso_subtract:
fixes ys
assumes distnct: "distinct ys"
- shows "set (subtract xs ys) = minus_set (set xs) (set ys)"
- and "distinct (subtract xs ys)"
- unfolding subtract_def minus_set_def
+ shows "set (subtract' ys xs) = set ys - set xs"
+ and "distinct (subtract' ys xs)"
+ unfolding subtract'_def flip_def subtract_def
using distnct by (induct xs arbitrary: ys) auto
lemma iso_map_distinct:
@@ -299,7 +281,7 @@
"(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
lemma [code func]:
- "minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" ..
+ "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
lemma [code func]:
"image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
@@ -324,7 +306,7 @@
insert \<equiv> insertl
"op \<union>" \<equiv> unionl
"op \<inter>" \<equiv> intersect
- minus_set \<equiv> subtract
+ "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
image \<equiv> map_distinct
Union \<equiv> unions
Inter \<equiv> intersects
@@ -334,7 +316,7 @@
Bex \<equiv> Blex
filter_set \<equiv> filter
-code_gen "{}" insert "op \<union>" "op \<inter>" minus_set
+code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
image Union Inter UNION INTER Ball Bex filter_set (SML -)
--- a/src/HOL/Library/List_lexord.thy Thu Jan 25 09:32:35 2007 +0100
+++ b/src/HOL/Library/List_lexord.thy Thu Jan 25 09:32:36 2007 +0100
@@ -34,22 +34,34 @@
apply simp
done
-lemma not_less_Nil [simp, code func]: "~(x < [])"
+lemma not_less_Nil [simp]: "\<not> (x < [])"
by (unfold list_less_def) simp
-lemma Nil_less_Cons [simp, code func]: "[] < a # x"
+lemma Nil_less_Cons [simp]: "[] < a # x"
by (unfold list_less_def) simp
-lemma Cons_less_Cons [simp, code func]: "(a # x < b # y) = (a < b | a = b & x < y)"
+lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
by (unfold list_less_def) simp
-lemma le_Nil [simp, code func]: "(x <= []) = (x = [])"
+lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
+ by (unfold list_ord_defs, cases x) auto
+
+lemma Nil_le_Cons [simp]: "[] \<le> x"
by (unfold list_ord_defs, cases x) auto
-lemma Nil_le_Cons [simp, code func]: "([] <= x)"
- by (unfold list_ord_defs, cases x) auto
-
-lemma Cons_le_Cons [simp, code func]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
+lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
by (unfold list_ord_defs) auto
+lemma less_code [code func]:
+ "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
+ "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
+ by simp_all
+
+lemma less_eq_code [code func]:
+ "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
+ "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
+ "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
+ by simp_all
+
end
--- a/src/HOL/Library/Product_ord.thy Thu Jan 25 09:32:35 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy Thu Jan 25 09:32:36 2007 +0100
@@ -10,11 +10,16 @@
begin
instance "*" :: (ord, ord) ord
- prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
- prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
+ prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
+ prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
lemmas prod_ord_defs = prod_less_def prod_le_def
+lemma [code func]:
+ "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+ "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+ unfolding prod_ord_defs by simp_all
+
lemma [code]:
"(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
"(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"