improved
authorhaftmann
Thu Jan 25 09:32:36 2007 +0100 (2007-01-25)
changeset 22177515021e98684
parent 22176 29ba33d58637
child 22178 29b95968272b
improved
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Product_ord.thy
     1.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu Jan 25 09:32:35 2007 +0100
     1.2 +++ b/src/HOL/Library/ExecutableSet.thy	Thu Jan 25 09:32:36 2007 +0100
     1.3 @@ -13,26 +13,6 @@
     1.4  
     1.5  instance set :: (eq) eq ..
     1.6  
     1.7 -definition
     1.8 -  minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     1.9 -  "minus_set xs ys = ys - xs"
    1.10 -
    1.11 -lemma [code inline]:
    1.12 -  "op - = (\<lambda>xs ys. minus_set ys xs)"
    1.13 -  unfolding minus_set_def ..
    1.14 -
    1.15 -definition
    1.16 -  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.17 -  "subset = op \<subseteq>"
    1.18 -
    1.19 -lemmas [symmetric, code inline] = subset_def
    1.20 -
    1.21 -definition
    1.22 -  strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where 
    1.23 -  "strict_subset = op \<subset>"
    1.24 -
    1.25 -lemmas [symmetric, code inline] = strict_subset_def
    1.26 -
    1.27  lemma [code target: Set]:
    1.28    "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.29    by blast
    1.30 @@ -42,12 +22,12 @@
    1.31    by blast
    1.32  
    1.33  lemma [code func]:
    1.34 -  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    1.35 -  unfolding subset_def Set.subset_def ..
    1.36 +  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    1.37 +  unfolding subset_def ..
    1.38  
    1.39  lemma [code func]:
    1.40 -  "strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B"
    1.41 -  unfolding subset_def strict_subset_def by blast
    1.42 +  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
    1.43 +  by blast
    1.44  
    1.45  lemma [code]:
    1.46    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    1.47 @@ -81,10 +61,8 @@
    1.48    and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
    1.49  unfolding member_def by (induct xs) simp_all
    1.50  
    1.51 -consts
    1.52 -  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.53 -
    1.54 -primrec
    1.55 +fun
    1.56 +  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.57    "drop_first f [] = []"
    1.58    "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    1.59  declare drop_first.simps [code del]
    1.60 @@ -215,12 +193,16 @@
    1.61    "set (intersect xs ys) = set xs \<inter> set ys"
    1.62    unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
    1.63  
    1.64 +definition
    1.65 +  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.66 +  "subtract' = flip subtract"
    1.67 +
    1.68  lemma iso_subtract:
    1.69    fixes ys
    1.70    assumes distnct: "distinct ys"
    1.71 -  shows "set (subtract xs ys) = minus_set (set xs) (set ys)"
    1.72 -  and "distinct (subtract xs ys)"
    1.73 -  unfolding subtract_def minus_set_def
    1.74 +  shows "set (subtract' ys xs) = set ys - set xs"
    1.75 +  and "distinct (subtract' ys xs)"
    1.76 +  unfolding subtract'_def flip_def subtract_def
    1.77    using distnct by (induct xs arbitrary: ys) auto
    1.78  
    1.79  lemma iso_map_distinct:
    1.80 @@ -299,7 +281,7 @@
    1.81    "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
    1.82  
    1.83  lemma [code func]:
    1.84 -  "minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" ..
    1.85 +  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
    1.86  
    1.87  lemma [code func]:
    1.88    "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
    1.89 @@ -324,7 +306,7 @@
    1.90    insert \<equiv> insertl
    1.91    "op \<union>" \<equiv> unionl
    1.92    "op \<inter>" \<equiv> intersect
    1.93 -  minus_set \<equiv> subtract
    1.94 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
    1.95    image \<equiv> map_distinct
    1.96    Union \<equiv> unions
    1.97    Inter \<equiv> intersects
    1.98 @@ -334,7 +316,7 @@
    1.99    Bex \<equiv> Blex
   1.100    filter_set \<equiv> filter
   1.101  
   1.102 -code_gen "{}" insert "op \<union>" "op \<inter>" minus_set
   1.103 +code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
   1.104    image Union Inter UNION INTER Ball Bex filter_set (SML -)
   1.105  
   1.106  
     2.1 --- a/src/HOL/Library/List_lexord.thy	Thu Jan 25 09:32:35 2007 +0100
     2.2 +++ b/src/HOL/Library/List_lexord.thy	Thu Jan 25 09:32:36 2007 +0100
     2.3 @@ -34,22 +34,34 @@
     2.4    apply simp
     2.5    done
     2.6  
     2.7 -lemma not_less_Nil [simp, code func]: "~(x < [])"
     2.8 +lemma not_less_Nil [simp]: "\<not> (x < [])"
     2.9    by (unfold list_less_def) simp
    2.10  
    2.11 -lemma Nil_less_Cons [simp, code func]: "[] < a # x"
    2.12 +lemma Nil_less_Cons [simp]: "[] < a # x"
    2.13    by (unfold list_less_def) simp
    2.14  
    2.15 -lemma Cons_less_Cons [simp, code func]: "(a # x < b # y) = (a < b | a = b & x < y)"
    2.16 +lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
    2.17    by (unfold list_less_def) simp
    2.18  
    2.19 -lemma le_Nil [simp, code func]: "(x <= []) = (x = [])"
    2.20 +lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
    2.21 +  by (unfold list_ord_defs, cases x) auto
    2.22 +
    2.23 +lemma Nil_le_Cons [simp]: "[] \<le> x"
    2.24    by (unfold list_ord_defs, cases x) auto
    2.25  
    2.26 -lemma Nil_le_Cons [simp, code func]: "([] <= x)"
    2.27 -  by (unfold list_ord_defs, cases x) auto
    2.28 -
    2.29 -lemma Cons_le_Cons [simp, code func]: "(a # x <= b # y) = (a < b | a = b & x <= y)"
    2.30 +lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    2.31    by (unfold list_ord_defs) auto
    2.32  
    2.33 +lemma less_code [code func]:
    2.34 +  "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    2.35 +  "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
    2.36 +  "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    2.37 +  by simp_all
    2.38 +
    2.39 +lemma less_eq_code [code func]:
    2.40 +  "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    2.41 +  "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
    2.42 +  "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
    2.43 +  by simp_all
    2.44 +
    2.45  end
     3.1 --- a/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:35 2007 +0100
     3.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:36 2007 +0100
     3.3 @@ -10,11 +10,16 @@
     3.4  begin
     3.5  
     3.6  instance "*" :: (ord, ord) ord
     3.7 -  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
     3.8 -  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
     3.9 +  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
    3.10 +  prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
    3.11  
    3.12  lemmas prod_ord_defs = prod_less_def prod_le_def
    3.13  
    3.14 +lemma [code func]:
    3.15 +  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    3.16 +  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    3.17 +  unfolding prod_ord_defs by simp_all
    3.18 +
    3.19  lemma [code]:
    3.20    "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    3.21    "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"