--- a/src/HOL/IsaMakefile Tue Mar 27 09:19:37 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Mar 27 12:28:42 2007 +0200
@@ -616,10 +616,10 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
-$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
- ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \
+$(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/Eval_examples.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
+ ex/Eval_examples.thy ex/Random.thy \
ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
--- a/src/HOL/ex/CodeRandom.thy Tue Mar 27 09:19:37 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,190 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* A simple random engine *}
-
-theory CodeRandom
-imports State_Monad
-begin
-
-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
-
-axiomatization
- random_shift :: "randseed \<Rightarrow> randseed"
-
-axiomatization
- random_seed :: "randseed \<Rightarrow> nat"
-
-definition
- random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
- "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" where
- [simp]: "select xs = (do
- n \<leftarrow> random (length xs);
- return (nth xs n)
- done)"
-definition
- select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
- [simp]: "select_weight xs = (do
- n \<leftarrow> random (foldl (op +) 0 (map fst xs));
- return (pick xs n)
- done)"
-
-lemma
- "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
-proof (induct xs)
- case Nil show ?case by (simp add: monad_collapse 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 arbitrary: 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
- have pick_nth_random_do:
- "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
- (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
- unfolding monad_collapse split_def unfolding pick_nth_random ..
- case (Cons x xs) then show ?case
- unfolding select_weight_def sum_length pick_nth_random_do
- by simp
-qed
-
-definition
- random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
- "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
-
-lemma random_nat [code]:
- "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
-unfolding random_int_def by simp
-
-axiomatization
- run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
-
-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
-
-open IntInf;
-
-exception RANDOM;
-
-type seed = int;
-
-local
- val a = fromInt 16807;
- (*greetings to SML/NJ*)
- val m = (the o fromString) "2147483647";
-in
- fun next s = (a * s) mod m;
-end;
-
-local
- val seed_ref = ref (fromInt 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 (s mod (h - 1), seed ());
-
-end;
-*}
-
-code_type randseed
- (SML "Random.seed")
-
-code_const random_int
- (SML "Random.value")
-
-code_const run_random
- (SML "case _ (Random.seed ()) of (x, '_) => x")
-
-code_gen select select_weight
- (SML #)
-
-end
\ No newline at end of file
--- a/src/HOL/ex/CodeRevappl.thy Tue Mar 27 09:19:37 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Combinators for structured results *}
-
-theory CodeRevappl
-imports Main
-begin
-
-section {* Combinators for structured results *}
-
-
-subsection {* primitive definitions *}
-
-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)"
-
-
-subsection {* lemmas *}
-
-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 Tue Mar 27 09:19:37 2007 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Mar 27 12:28:42 2007 +0200
@@ -9,7 +9,7 @@
no_document time_use_thy "Classpackage";
no_document time_use_thy "Eval_examples";
-no_document time_use_thy "CodeRandom";
+no_document time_use_thy "Random";
no_document time_use_thy "Codegenerator_Rat";
no_document time_use_thy "Codegenerator";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Random.thy Tue Mar 27 12:28:42 2007 +0200
@@ -0,0 +1,186 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* A simple random engine *}
+
+theory Random
+imports State_Monad
+begin
+
+fun
+ pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
+where
+ pick_undef: "pick [] n = undefined"
+ | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
+lemmas [code nofunc] = pick_undef
+
+typedecl randseed
+
+axiomatization
+ random_shift :: "randseed \<Rightarrow> randseed"
+
+axiomatization
+ random_seed :: "randseed \<Rightarrow> nat"
+
+definition
+ random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
+ "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" where
+ [simp]: "select xs = (do
+ n \<leftarrow> random (length xs);
+ return (nth xs n)
+ done)"
+definition
+ select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
+ [simp]: "select_weight xs = (do
+ n \<leftarrow> random (foldl (op +) 0 (map fst xs));
+ return (pick xs n)
+ done)"
+
+lemma
+ "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
+proof (induct xs)
+ case Nil show ?case by (simp add: monad_collapse 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 arbitrary: 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
+ have pick_nth_random_do:
+ "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
+ (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
+ unfolding monad_collapse split_def unfolding pick_nth_random ..
+ case (Cons x xs) then show ?case
+ unfolding select_weight_def sum_length pick_nth_random_do
+ by simp
+qed
+
+definition
+ random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
+ "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
+
+lemma random_nat [code]:
+ "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
+unfolding random_int_def by simp
+
+axiomatization
+ run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
+
+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
+
+open IntInf;
+
+exception RANDOM;
+
+type seed = int;
+
+local
+ val a = fromInt 16807;
+ (*greetings to SML/NJ*)
+ val m = (the o fromString) "2147483647";
+in
+ fun next s = (a * s) mod m;
+end;
+
+local
+ val seed_ref = ref (fromInt 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 (s mod (h - 1), seed ());
+
+end;
+*}
+
+code_type randseed
+ (SML "Random.seed")
+
+code_const random_int
+ (SML "Random.value")
+
+code_const run_random
+ (SML "case _ (Random.seed ()) of (x, '_) => x")
+
+code_gen select select_weight
+ (SML #)
+
+end