# HG changeset patch
# User haftmann
# Date 1174639582 -3600
# Node ID d284097414065c7fa90603f43010679551a88fb9
# Parent  c5929d4373a073c1b028ce64a483ad2f7ded0d7f
dropped

diff -r c5929d4373a0 -r d28409741406 src/HOL/ex/CodeCollections.thy
--- 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