# HG changeset patch
# User haftmann
# Date 1174991322 -7200
# Node ID 8501c4a62a3c4daf85a1ca54aea8af13e520b5d1
# Parent  84690fcd3db91a2d6148aae7bd2fc658b702eaa5
cleaned up HOL/ex/Code*.thy

diff -r 84690fcd3db9 -r 8501c4a62a3c src/HOL/IsaMakefile
--- 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                     \
diff -r 84690fcd3db9 -r 8501c4a62a3c src/HOL/ex/CodeRandom.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
diff -r 84690fcd3db9 -r 8501c4a62a3c src/HOL/ex/CodeRevappl.thy
--- 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
diff -r 84690fcd3db9 -r 8501c4a62a3c src/HOL/ex/ROOT.ML
--- 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";
 
diff -r 84690fcd3db9 -r 8501c4a62a3c src/HOL/ex/Random.thy
--- /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