# HG changeset patch
# User haftmann
# Date 1169713956 -3600
# Node ID 515021e98684dba8086914d2236fa97e107dd645
# Parent  29ba33d58637a71db7c4023b8d5b23e7043f7756
improved

diff -r 29ba33d58637 -r 515021e98684 src/HOL/Library/ExecutableSet.thy
--- 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 -)
 
 
diff -r 29ba33d58637 -r 515021e98684 src/HOL/Library/List_lexord.thy
--- 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
diff -r 29ba33d58637 -r 515021e98684 src/HOL/Library/Product_ord.thy
--- 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"