--- a/src/HOL/IsaMakefile Wed Aug 30 08:30:09 2006 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 30 08:34:45 2006 +0200
@@ -640,7 +640,7 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \
- ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
+ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
ex/CodeOperationalEquality.thy ex/Codegenerator.thy ex/Commutative_RingEx.thy \
ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeCollections.thy Wed Aug 30 08:34:45 2006 +0200
@@ -0,0 +1,417 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Collection classes as examples for code generation *}
+
+theory CodeCollections
+imports CodeOperationalEquality
+begin
+
+section {* Collection classes as examples for code generation *}
+
+class ordered = eq +
+ constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65)
+ fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65)
+ assumes order_refl: "x \<^loc><<= x"
+ assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z"
+ assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y"
+
+declare order_refl [simp, intro]
+
+defs
+ lt_def: "x << y == (x <<= y \<and> x \<noteq> y)"
+
+lemma lt_intro [intro]:
+ assumes "x <<= y" and "x \<noteq> y"
+ shows "x << y"
+unfolding lt_def ..
+
+lemma lt_elim [elim]:
+ assumes "(x::'a::ordered) << y"
+ and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P"
+ shows P
+proof -
+ from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def)
+ show P by (rule Q [OF R1 R2])
+qed
+
+lemma lt_trans:
+ assumes "x << y" and "y << z"
+ shows "x << z"
+proof
+ from prems lt_def have prems': "x <<= y" "y <<= z" by auto
+ show "x <<= z" by (rule order_trans, auto intro: prems')
+next
+ show "x \<noteq> z"
+ proof
+ from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto
+ assume "x = z"
+ with prems' have "x <<= y" and "y <<= x" by auto
+ with order_antisym have "x = y" .
+ with prems' show False by auto
+ qed
+qed
+
+definition (in ordered)
+ min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ "min x y = (if x \<^loc><<= y then x else y)"
+ max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ "max x y = (if x \<^loc><<= y then y else x)"
+
+definition
+ min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+ "min x y = (if x <<= y then x else y)"
+ max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
+ "max x y = (if x <<= y then y else x)"
+
+consts
+ abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
+
+function
+ "abs_sorted cmp [] = True"
+ "abs_sorted cmp [x] = True"
+ "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
+by pat_completeness simp_all
+termination by (auto_term "measure (length o snd)")
+
+abbreviation (in ordered)
+ "sorted \<equiv> abs_sorted le"
+
+abbreviation
+ "sorted \<equiv> abs_sorted le"
+
+lemma (in ordered) 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(5) have "sorted (x # x' # xs)" .
+ then show "sorted (x' # xs)" by auto
+qed
+
+instance bool :: ordered
+ "p <<= q == (p --> q)"
+ by default (unfold ordered_bool_def, blast+)
+
+instance nat :: ordered
+ "m <<= n == m <= n"
+ by default (simp_all add: ordered_nat_def)
+
+instance int :: ordered
+ "k <<= l == k <= l"
+ by default (simp_all add: ordered_int_def)
+
+instance unit :: ordered
+ "u <<= v == True"
+ by default (simp_all add: ordered_unit_def)
+
+consts
+ le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
+
+function
+ "le_option' None y = True"
+ "le_option' (Some x) None = False"
+ "le_option' (Some x) (Some y) = x <<= y"
+ by pat_completeness simp_all
+termination by (auto_term "{}")
+
+instance (ordered) option :: ordered
+ "x <<= y == le_option' x y"
+proof (default, unfold ordered_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)
+ (erule order_trans, assumption)
+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)
+ (erule order_antisym, assumption)
+qed
+
+lemma [simp, code]:
+ "None <<= y = True"
+ "Some x <<= None = False"
+ "Some v <<= Some w = v <<= w"
+ unfolding ordered_option_def le_option'.simps by rule+
+
+consts
+ le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+
+function
+ "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
+ by pat_completeness simp_all
+termination by (auto_term "{}")
+
+instance (ordered, ordered) * :: ordered
+ "x <<= y == le_pair' x y"
+apply (default, unfold "ordered_*_def", unfold split_paired_all)
+apply simp_all
+apply (auto intro: lt_trans order_trans)[1]
+unfolding lt_def apply (auto intro: order_antisym)[1]
+done
+
+lemma [simp, code]:
+ "(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
+ unfolding "ordered_*_def" le_pair'.simps ..
+
+(* consts
+ le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
+
+function
+ "le_list' [] ys = True"
+ "le_list' (x#xs) [] = False"
+ "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
+ by pat_completeness simp_all
+termination by (auto_term "measure (length o fst)")
+
+instance (ordered) list :: ordered
+ "xs <<= ys == le_list' xs ys"
+proof (default, unfold "ordered_list_def")
+ fix xs
+ show "le_list' xs xs" by (induct xs) simp_all
+next
+ fix xs ys zs
+ assume "le_list' xs ys" and "le_list' ys zs"
+ then show "le_list' xs zs"
+ apply (induct xs zs rule: le_list'.induct)
+ apply simp_all
+ apply (cases ys) apply simp_all
+
+ apply (induct ys) apply simp_all
+ apply (induct ys)
+ apply simp_all
+ apply (induct zs)
+ apply simp_all
+next
+ fix xs ys
+ assume "le_list' xs ys" and "le_list' ys xs"
+ show "xs = ys" sorry
+qed
+
+lemma [simp, code]:
+ "[] <<= ys = True"
+ "(x#xs) <<= [] = False"
+ "(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)"
+ unfolding "ordered_list_def" le_list'.simps by rule+*)
+
+class infimum = ordered +
+ fixes inf
+ assumes inf: "inf \<^loc><<= x"
+
+lemma (in infimum)
+ assumes prem: "a \<^loc><<= inf"
+ shows no_smaller: "a = inf"
+using prem inf by (rule order_antisym)
+
+consts
+ abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
+
+ML {* set quick_and_dirty *}
+function
+ "abs_max_of cmp inff [] = inff"
+ "abs_max_of cmp inff [x] = x"
+ "abs_max_of cmp inff (x#xs) =
+ ordered.max cmp x (abs_max_of cmp inff xs)"
+apply pat_completeness sorry
+
+abbreviation (in infimum)
+ "max_of xs \<equiv> abs_max_of le inf"
+
+abbreviation
+ "max_of xs \<equiv> abs_max_of le inf"
+
+instance bool :: infimum
+ "inf == False"
+ by default (simp add: infimum_bool_def)
+
+instance nat :: infimum
+ "inf == 0"
+ by default (simp add: infimum_nat_def)
+
+instance unit :: infimum
+ "inf == ()"
+ by default (simp add: infimum_unit_def)
+
+instance (ordered) option :: infimum
+ "inf == None"
+ by default (simp add: infimum_option_def)
+
+instance (infimum, infimum) * :: infimum
+ "inf == (inf, inf)"
+ by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf)
+
+class enum = ordered +
+ fixes enum :: "'a list"
+ assumes member_enum: "x \<in> set enum"
+ and ordered_enum: "abs_sorted le enum"
+
+(*
+FIXME:
+- abbreviations must be propagated before locale introduction
+- then also now shadowing may occur
+*)
+(*abbreviation (in enum)
+ "local.sorted \<equiv> abs_sorted le"*)
+
+instance bool :: enum
+ (* FIXME: better name handling of definitions *)
+ "_1": "enum == [False, True]"
+ by default (simp_all add: enum_bool_def)
+
+instance unit :: enum
+ "_2": "enum == [()]"
+ by default (simp_all add: enum_unit_def)
+
+(*consts
+ product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
+
+primrec
+ "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
+
+lemma product_sorted:
+ assumes "sorted xs" "sorted ys"
+ shows "sorted (product xs ys)"
+using prems proof (induct xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons x xs)
+ from Cons ordered.sorted_weakening have "sorted xs" by auto
+ with Cons have "sorted (product xs ys)" by auto
+ then show ?case apply simp
+ proof -
+ assume
+apply simp
+
+ 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 (enum, enum) * :: enum
+ "_3": "enum == product enum enum"
+apply default
+apply (simp_all add: "enum_*_def")
+apply (unfold split_paired_all)
+apply (rule product_all)
+apply (rule member_enum)+
+sorry*)
+
+instance (enum) option :: enum
+ "_4": "enum == None # map Some enum"
+proof (default, unfold enum_option_def)
+ fix x :: "'a::enum option"
+ show "x \<in> set (None # map Some enum)"
+ proof (cases x)
+ case None then show ?thesis by auto
+ next
+ case (Some x) then show ?thesis by (auto intro: member_enum)
+ qed
+next
+ show "sorted (None # map Some (enum :: ('a::enum) list))"
+ sorry
+ (*proof (cases "enum :: 'a list")
+ case Nil then show ?thesis by simp
+ next
+ case (Cons x xs)
+ then have "sorted (None # map Some (x # xs))" sorry
+ then show ?thesis apply simp
+ apply simp_all
+ apply auto*)
+qed
+
+ML {* reset quick_and_dirty *}
+
+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"
+ "between x y = get_first (\<lambda>z. x << z & z << y) enum"
+
+definition
+ index :: "'a::enum \<Rightarrow> nat"
+ "index x = the (get_index (\<lambda>y. y = x) 0 enum)"
+
+definition
+ add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a"
+ "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]"
+ "test2 = (inf :: nat \<times> unit)"
+
+code_generate eq
+code_generate "op <<="
+code_generate "op <<"
+code_generate inf
+code_generate between
+code_generate index
+code_generate sum
+code_generate test1
+code_generate test2
+
+code_serialize ml (-)
+
+end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Wed Aug 30 08:30:09 2006 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Aug 30 08:34:45 2006 +0200
@@ -7,6 +7,7 @@
no_document time_use_thy "Classpackage";
no_document time_use_thy "Codegenerator";
no_document time_use_thy "CodeOperationalEquality";
+no_document time_use_thy "CodeCollections";
no_document time_use_thy "CodeEval";
no_document time_use_thy "CodeRandom";