--- a/src/HOL/IsaMakefile Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 21 11:02:39 2006 +0200
@@ -202,6 +202,7 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
+ Library/MLString.thy \
Library/FuncSet.thy Library/Library.thy \
Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
@@ -638,7 +639,9 @@
$(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/Commutative_RingEx.thy \
+ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
+ ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
+ ex/Codegenerator.thy ex/Commutative_RingEx.thy \
ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy \
ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
--- a/src/HOL/Library/Library.thy Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/Library/Library.thy Mon Aug 21 11:02:39 2006 +0200
@@ -6,6 +6,7 @@
EfficientNat
ExecutableSet
ExecutableRat
+ MLString
FuncSet
Multiset
NatPair
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/MLString.thy Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,88 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Monolithic strings for ML *}
+
+theory MLString
+imports Main
+begin
+
+section {* Monolithic strings for ML *}
+
+subsection {* Motivation *}
+
+text {*
+ Strings are represented in HOL as list of characters.
+ For code generation to Haskell, this is no problem
+ since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
+ On the other hand, in ML all strings have to
+ be represented as list of characters which
+ is awkward to read. This theory provides a distinguished
+ datatype for strings which then by convention
+ are serialized as monolithic ML strings. Note
+ that in Haskell these strings are identified
+ with Haskell strings.
+*}
+
+
+subsection {* Datatype of monolithic strings *}
+
+datatype ml_string = STR string
+
+consts
+ explode :: "ml_string \<Rightarrow> string"
+
+primrec
+ "explode (STR s) = s"
+
+
+subsection {* ML interface *}
+
+ML {*
+structure MLString =
+struct
+
+local
+ val thy = the_context ();
+ val const_STR = Sign.intern_const thy "STR";
+in
+ val typ_ml_string = Type (Sign.intern_type thy "ml_string", []);
+ fun term_ml_string s = Const (const_STR, HOList.typ_string --> typ_ml_string)
+ $ HOList.term_string s
+end;
+
+end;
+*}
+
+
+subsection {* Code serialization *}
+
+code_typapp ml_string
+ ml (target_atom "string")
+ haskell (target_atom "String")
+
+code_constapp STR
+ haskell ("_")
+
+setup {*
+let
+ fun print_char c =
+ let
+ val i = ord c
+ in if i < 32
+ then prefix "\\" (string_of_int i)
+ else c
+ end;
+ val print_string = quote;
+in
+ CodegenPackage.add_pretty_ml_string "ml" "Nil" "Cons" "STR"
+ print_char print_string "String.implode"
+end
+*}
+
+code_constapp explode
+ ml (target_atom "String.explode")
+ haskell ("_")
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeEmbed.thy Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,91 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+theory CodeEmbed
+imports Main MLString
+begin
+
+section {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+
+subsection {* Definitions *}
+
+types vname = ml_string;
+types "class" = ml_string;
+types sort = "class list"
+
+datatype "typ" =
+ Type ml_string "typ list" (infix "{\<struct>}" 120)
+ | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
+
+abbreviation
+ Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
+ "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+ Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
+ "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
+
+datatype "term" =
+ Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
+ | Fix vname "typ" (infix ":\<epsilon>" 112)
+ | App "term" "term" (infixl "\<bullet>" 110)
+
+abbreviation
+ Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110)
+ "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
+
+
+subsection {* ML interface *}
+
+ML {*
+structure Embed =
+struct
+
+local
+ val thy = the_context ();
+ val const_Type = Sign.intern_const thy "Type";
+ val const_TFix = Sign.intern_const thy "TFix";
+ val const_Const = Sign.intern_const thy "Const";
+ val const_App = Sign.intern_const thy "App";
+ val const_Fix = Sign.intern_const thy "Fix";
+in
+ val typ_vname = Type (Sign.intern_type thy "vname", []);
+ val typ_class = Type (Sign.intern_type thy "class", []);
+ val typ_sort = Type (Sign.intern_type thy "sort", []);
+ val typ_typ = Type (Sign.intern_type thy "typ", []);
+ val typ_term = Type (Sign.intern_type thy "term", []);
+ val term_sort = HOList.term_list typ_class MLString.term_ml_string;
+ fun term_typ f (Type (tyco, tys)) =
+ Const (const_Type, MLString.typ_ml_string --> HOList.typ_list typ_typ --> typ_typ)
+ $ MLString.term_ml_string tyco $ HOList.term_list typ_typ (term_typ f) tys
+ | term_typ f (TFree v) =
+ f v;
+ fun term_term f g (Const (c, ty)) =
+ Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term)
+ $ MLString.term_ml_string c $ g ty
+ | term_term f g (t1 $ t2) =
+ Const (const_App, typ_term --> typ_term --> typ_term)
+ $ term_term f g t1 $ term_term f g t2
+ | term_term f g (Free v) = f v;
+end;
+
+end;
+*}
+
+
+subsection {* Code serialization setup *}
+
+code_typapp
+ "typ" ml (target_atom "Term.typ")
+ "term" ml (target_atom "Term.term")
+
+code_constapp
+ Type ml ("Term.Type (_, _)")
+ TFix ml ("Term.TFree (_, _)")
+ Const ml ("Term.Const (_, _)")
+ App ml ("Term.$ (_, _)")
+ Fix ml ("Term.Free (_, _)")
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeRandom.thy Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,175 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* A simple random engine *}
+
+theory CodeRandom
+imports CodeRevappl
+begin
+
+section {* A simple random engine *}
+
+consts
+ pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
+
+primrec
+ "pick (x#xs) n = (let (k, v) = x in
+ if n < k then v else pick xs (n - k))"
+
+lemma pick_def [code, simp]:
+ "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
+declare pick.simps [simp del, code del]
+
+typedecl randseed
+
+consts
+ random_shift :: "randseed \<Rightarrow> randseed"
+ random_seed :: "randseed \<Rightarrow> nat"
+
+definition
+ random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed"
+ "random n s = (random_seed s mod n, random_shift s)"
+
+lemma random_bound:
+ assumes "0 < n"
+ shows "fst (random n s) < n"
+proof -
+ from prems mod_less_divisor have "!!m .m mod n < n" by auto
+ then show ?thesis unfolding random_def by simp
+qed
+
+lemma random_random_seed [simp]:
+ "snd (random n s) = random_shift s" unfolding random_def by simp
+
+definition
+ select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+ [simp]: "select xs s =
+ s
+ \<triangleright> random (length xs)
+ \<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
+ select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+ [simp]: "select_weight xs s =
+ s
+ \<triangleright> random (foldl (op +) 0 (map fst xs))
+ \<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
+
+lemma
+ "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
+proof (induct xs)
+ case Nil show ?case by (simp add: revappl random_def)
+next
+ have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
+ proof -
+ fix xs
+ fix y
+ show "map fst (map (Pair y) xs) = replicate (length xs) y"
+ by (induct xs) simp_all
+ qed
+ have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
+ proof -
+ fix xs
+ fix n
+ assume "n < length xs"
+ then show "pick (map (Pair 1) xs) n = nth xs n"
+ proof (induct xs fixing: n)
+ case Nil then show ?case by simp
+ next
+ case (Cons x xs) show ?case
+ proof (cases n)
+ case 0 then show ?thesis by simp
+ next
+ case (Suc _)
+ from Cons have "n < length (x # xs)" by auto
+ then have "n < Suc (length xs)" by simp
+ with Suc have "n - 1 < Suc (length xs) - 1" by auto
+ with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
+ with Suc show ?thesis by auto
+ qed
+ qed
+ qed
+ have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
+ proof -
+ have replicate_append:
+ "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
+ by (simp add: replicate_app_Cons_same)
+ fix xs
+ show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
+ unfolding map_fst_Pair proof (induct xs)
+ case Nil show ?case by simp
+ next
+ case (Cons x xs) then show ?case unfolding replicate_append by simp
+ qed
+ qed
+ have pick_nth_random:
+ "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
+ proof -
+ fix s
+ fix x
+ fix xs
+ have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
+ from pick_nth [OF bound] show
+ "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
+ qed
+ case (Cons x xs) then show ?case
+ unfolding select_weight_def sum_length revappl_split pick_nth_random
+ by (simp add: revappl_split)
+qed
+
+definition
+ random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
+ "random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
+
+lemma random_nat [code]:
+ "random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
+unfolding random_int_def Let_def split_def random_def by simp
+
+ML {*
+signature RANDOM =
+sig
+ type seed = IntInf.int;
+ val seed: unit -> seed;
+ val value: IntInf.int -> seed -> IntInf.int * seed;
+end;
+
+structure Random : RANDOM =
+struct
+
+exception RANDOM;
+
+type seed = IntInf.int;
+
+local
+ val a = 16807;
+ val m = 2147483647;
+in
+ fun next s = IntInf.mod (a * s, m)
+end;
+
+local
+ val seed_ref = ref 1;
+in
+ fun seed () =
+ let
+ val r = next (!seed_ref)
+ in
+ (seed_ref := r; r)
+ end;
+end;
+
+fun value h s =
+ if h < 1 then raise RANDOM
+ else (IntInf.mod (s, h - 1), seed ());
+
+end;
+*}
+
+code_typapp randseed
+ ml (target_atom "Random.seed")
+
+code_constapp random_int
+ ml (target_atom "Random.value")
+
+code_serialize ml select select_weight (-)
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeRevappl.thy Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,36 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Combinators for structured results *}
+
+theory CodeRevappl
+imports Main
+begin
+
+section {* Combinators for structured results *}
+
+definition
+ revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
+ revappl_def: "x \<triangleright> f = f x"
+ revappl_snd :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<times> 'b" (infixl "|\<triangleright>" 55)
+ revappl_snd_split: "z |\<triangleright> f = (fst z , f (snd z))"
+ revappl_swamp :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'd \<times> 'b) \<Rightarrow> ('c \<times> 'd) \<times> 'b" (infixl "|\<triangleright>\<triangleright>" 55)
+ revappl_swamp_split: "z |\<triangleright>\<triangleright> f = ((fst z, fst (f (snd z))), snd (f (snd z)))"
+ revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
+ revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
+
+lemma revappl_snd_def [code]:
+ "(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp
+
+lemma revappl_swamp_def [code]:
+ "(y, x) |\<triangleright>\<triangleright> f = (let (z, w) = f x in ((y, z), w))" unfolding Let_def revappl_swamp_split split_def by simp
+
+lemma revappl_uncurry_def [code]:
+ "(y, x) \<turnstile>\<triangleright> f = f y x" unfolding revappl_uncurry_split by simp
+
+lemmas revappl = revappl_def revappl_snd_def revappl_swamp_def revappl_uncurry_def
+
+lemmas revappl_split = revappl_def revappl_snd_split revappl_swamp_split revappl_uncurry_split
+
+end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Aug 21 11:02:39 2006 +0200
@@ -6,6 +6,9 @@
no_document time_use_thy "Classpackage";
no_document time_use_thy "Codegenerator";
+no_document time_use_thy "CodeEmbed";
+no_document time_use_thy "CodeRandom";
+no_document time_use_thy "CodeRevappl";
time_use_thy "Higher_Order_Logic";
time_use_thy "Abstract_NAT";