--- a/src/HOL/ex/CodeCollections.thy Fri Mar 23 09:40:57 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Collection classes as examples for code generation *}
-
-theory CodeCollections
-imports Main Product_ord List_lexord
-begin
-
-fun
- abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
- "abs_sorted cmp [] \<longleftrightarrow> True"
-| "abs_sorted cmp [x] \<longleftrightarrow> True"
-| "abs_sorted cmp (x#y#xs) \<longleftrightarrow> cmp x y \<and> abs_sorted cmp (y#xs)"
-
-abbreviation (in ord)
- "sorted \<equiv> abs_sorted less_eq"
-
-lemma (in order) sorted_weakening:
- assumes "sorted (x # xs)"
- shows "sorted xs"
-using prems proof (induct xs)
- case Nil show ?case by simp
-next
- case (Cons x' xs)
- from this have "sorted (x # x' # xs)" by auto
- then show "sorted (x' # xs)"
- by auto
-qed
-
-instance unit :: order
- "u \<le> v \<equiv> True"
- "u < v \<equiv> False"
- by default (simp_all add: less_eq_unit_def less_unit_def)
-
-fun le_option' :: "'a\<Colon>order option \<Rightarrow> 'a option \<Rightarrow> bool"
- where "le_option' None y \<longleftrightarrow> True"
- | "le_option' (Some x) None \<longleftrightarrow> False"
- | "le_option' (Some x) (Some y) \<longleftrightarrow> x \<le> y"
-
-instance option :: (order) order
- "x \<le> y \<equiv> le_option' x y"
- "x < y \<equiv> x \<le> y \<and> x \<noteq> y"
-proof (default, unfold less_eq_option_def less_option_def)
- fix x
- show "le_option' x x" by (cases x) simp_all
-next
- fix x y z
- assume "le_option' x y" "le_option' y z"
- then show "le_option' x z"
- by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
-next
- fix x y
- assume "le_option' x y" "le_option' y x"
- then show "x = y"
- by (cases x, simp_all, cases y, simp_all, cases y, simp_all)
-next
- fix x y
- show "le_option' x y \<and> x \<noteq> y \<longleftrightarrow> le_option' x y \<and> x \<noteq> y" ..
-qed
-
-lemma [simp, code]:
- "None \<le> y \<longleftrightarrow> True"
- "Some x \<le> None \<longleftrightarrow> False"
- "Some v \<le> Some w \<longleftrightarrow> v \<le> w"
- unfolding less_eq_option_def less_option_def le_option'.simps by rule+
-
-lemma forall_all [simp]:
- "list_all P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
- by (induct xs) auto
-
-lemma exists_ex [simp]:
- "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
- by (induct xs) auto
-
-class finite = type +
- fixes fin :: "'a list"
- assumes member_fin: "x \<in> set fin"
-begin
-
-lemma set_enum_UNIV:
- "set fin = UNIV"
- using member_fin by auto
-
-lemma all_forall [code func, code inline]:
- "(\<forall>x. P x) \<longleftrightarrow> list_all P fin"
- using set_enum_UNIV by simp_all
-
-lemma ex_exists [code func, code inline]:
- "(\<exists>x. P x) \<longleftrightarrow> list_ex P fin"
- using set_enum_UNIV by simp_all
-
-end
-
-instance bool :: finite
- "fin == [False, True]"
- by default (simp_all add: fin_bool_def)
-
-instance unit :: finite
- "fin == [()]"
- by default (simp_all add: fin_unit_def)
-
-fun
- product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
- where
- "product [] ys = []"
-| "product (x#xs) ys = map (Pair x) ys @ product xs ys"
-
-lemma product_all:
- assumes "x \<in> set xs" "y \<in> set ys"
- shows "(x, y) \<in> set (product xs ys)"
-using prems proof (induct xs)
- case Nil
- then have False by auto
- then show ?case ..
-next
- case (Cons z xs)
- then show ?case
- proof (cases "x = z")
- case True
- with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp
- with True show ?thesis by simp
- next
- case False
- with Cons have "x \<in> set xs" by auto
- with Cons have "(x, y) \<in> set (product xs ys)" by auto
- then show "(x, y) \<in> set (product (z#xs) ys)" by auto
- qed
-qed
-
-instance * :: (finite, finite) finite
- "fin == product fin fin"
-apply default
-apply (simp_all add: "fin_*_def")
-apply (unfold split_paired_all)
-apply (rule product_all)
-apply (rule member_fin)+
-done
-
-instance option :: (finite) finite
- "fin == None # map Some fin"
-proof (default, unfold fin_option_def)
- fix x :: "'a::finite option"
- show "x \<in> set (None # map Some fin)"
- proof (cases x)
- case None then show ?thesis by auto
- next
- case (Some x) then show ?thesis by (auto intro: member_fin)
- qed
-qed
-
-consts
- get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"
-
-primrec
- "get_first p [] = None"
- "get_first p (x#xs) = (if p x then Some x else get_first p xs)"
-
-consts
- get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option"
-
-primrec
- "get_index p n [] = None"
- "get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)"
-
-(*definition
- between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" where
- "between x y = get_first (\<lambda>z. x << z & z << y) enum"
-
-definition
- index :: "'a::enum \<Rightarrow> nat" where
- "index x = the (get_index (\<lambda>y. y = x) 0 enum)"
-
-definition
- add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" where
- "add x y =
- (let
- enm = enum
- in enm ! ((index x + index y) mod length enm))"
-
-consts
- sum :: "'a::{enum, infimum} list \<Rightarrow> 'a"
-
-primrec
- "sum [] = inf"
- "sum (x#xs) = add x (sum xs)"*)
-
-(*definition "test1 = sum [None, Some True, None, Some False]"*)
-(*definition "test2 = (inf :: nat \<times> unit)"*)
-definition "test3 \<longleftrightarrow> (\<exists>x \<Colon> bool option. case x of Some P \<Rightarrow> P | None \<Rightarrow> False)"
-
-code_gen test3 (SML #) (OCaml -) (Haskell -)
-
-end
\ No newline at end of file