cleaned up HOL/ex/Code*.thy
authorhaftmann
Tue Mar 27 12:28:42 2007 +0200 (2007-03-27)
changeset 225288501c4a62a3c
parent 22527 84690fcd3db9
child 22529 902ed60d53a7
cleaned up HOL/ex/Code*.thy
src/HOL/IsaMakefile
src/HOL/ex/CodeRandom.thy
src/HOL/ex/CodeRevappl.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Random.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Mar 27 09:19:37 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Mar 27 12:28:42 2007 +0200
     1.3 @@ -616,10 +616,10 @@
     1.4  
     1.5  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.6  
     1.7 -$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
     1.8 -  ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
     1.9 +$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy                       \
    1.10 +  ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy                   \
    1.11    ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
    1.12 -  ex/Eval_examples.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
    1.13 +  ex/Eval_examples.thy ex/Random.thy                                            \
    1.14    ex/Codegenerator.thy ex/Codegenerator_Rat.thy                                 \
    1.15    ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy                             \
    1.16    ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy                     \
     2.1 --- a/src/HOL/ex/CodeRandom.thy	Tue Mar 27 09:19:37 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,190 +0,0 @@
     2.4 -(*  ID:         $Id$
     2.5 -    Author:     Florian Haftmann, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -header {* A simple random engine *}
     2.9 -
    2.10 -theory CodeRandom
    2.11 -imports State_Monad
    2.12 -begin
    2.13 -
    2.14 -consts
    2.15 -  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
    2.16 -
    2.17 -primrec
    2.18 -  "pick (x#xs) n = (let (k, v) = x in
    2.19 -    if n < k then v else pick xs (n - k))"
    2.20 -
    2.21 -lemma pick_def [code, simp]:
    2.22 -  "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
    2.23 -declare pick.simps [simp del, code del]
    2.24 -
    2.25 -typedecl randseed
    2.26 -
    2.27 -axiomatization
    2.28 -  random_shift :: "randseed \<Rightarrow> randseed"
    2.29 -
    2.30 -axiomatization
    2.31 -  random_seed :: "randseed \<Rightarrow> nat"
    2.32 -
    2.33 -definition
    2.34 -  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
    2.35 -  "random n s = (random_seed s mod n, random_shift s)"
    2.36 -
    2.37 -lemma random_bound:
    2.38 -  assumes "0 < n"
    2.39 -  shows "fst (random n s) < n"
    2.40 -proof -
    2.41 -  from prems mod_less_divisor have "!!m .m mod n < n" by auto
    2.42 -  then show ?thesis unfolding random_def by simp 
    2.43 -qed
    2.44 -
    2.45 -lemma random_random_seed [simp]:
    2.46 -  "snd (random n s) = random_shift s" unfolding random_def by simp
    2.47 -
    2.48 -definition
    2.49 -  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
    2.50 -  [simp]: "select xs = (do
    2.51 -      n \<leftarrow> random (length xs);
    2.52 -      return (nth xs n)
    2.53 -    done)"
    2.54 -definition
    2.55 -  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
    2.56 -  [simp]: "select_weight xs = (do
    2.57 -      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
    2.58 -      return (pick xs n)
    2.59 -    done)"
    2.60 -
    2.61 -lemma
    2.62 -  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
    2.63 -proof (induct xs)
    2.64 -  case Nil show ?case by (simp add: monad_collapse random_def)
    2.65 -next
    2.66 -  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
    2.67 -  proof -
    2.68 -    fix xs
    2.69 -    fix y
    2.70 -    show "map fst (map (Pair y) xs) = replicate (length xs) y"
    2.71 -      by (induct xs) simp_all
    2.72 -  qed
    2.73 -  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
    2.74 -  proof -
    2.75 -    fix xs
    2.76 -    fix n
    2.77 -    assume "n < length xs"
    2.78 -    then show "pick (map (Pair 1) xs) n = nth xs n"
    2.79 -    proof (induct xs arbitrary: n)
    2.80 -      case Nil then show ?case by simp
    2.81 -    next
    2.82 -      case (Cons x xs) show ?case
    2.83 -      proof (cases n)
    2.84 -        case 0 then show ?thesis by simp
    2.85 -      next
    2.86 -        case (Suc _)
    2.87 -    from Cons have "n < length (x # xs)" by auto
    2.88 -        then have "n < Suc (length xs)" by simp
    2.89 -        with Suc have "n - 1 < Suc (length xs) - 1" by auto
    2.90 -        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
    2.91 -        with Suc show ?thesis by auto
    2.92 -      qed
    2.93 -    qed
    2.94 -  qed
    2.95 -  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
    2.96 -  proof -
    2.97 -    have replicate_append:
    2.98 -      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
    2.99 -      by (simp add: replicate_app_Cons_same)
   2.100 -    fix xs
   2.101 -    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
   2.102 -    unfolding map_fst_Pair proof (induct xs)
   2.103 -      case Nil show ?case by simp
   2.104 -    next
   2.105 -      case (Cons x xs) then show ?case unfolding replicate_append by simp
   2.106 -    qed
   2.107 -  qed
   2.108 -  have pick_nth_random:
   2.109 -    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
   2.110 -  proof -
   2.111 -    fix s
   2.112 -    fix x
   2.113 -    fix xs
   2.114 -    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
   2.115 -    from pick_nth [OF bound] show
   2.116 -      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
   2.117 -  qed
   2.118 -  have pick_nth_random_do:
   2.119 -    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
   2.120 -      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
   2.121 -  unfolding monad_collapse split_def unfolding pick_nth_random ..
   2.122 -  case (Cons x xs) then show ?case
   2.123 -    unfolding select_weight_def sum_length pick_nth_random_do
   2.124 -    by simp
   2.125 -qed
   2.126 -
   2.127 -definition
   2.128 -  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
   2.129 -  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
   2.130 -
   2.131 -lemma random_nat [code]:
   2.132 -  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
   2.133 -unfolding random_int_def by simp
   2.134 -
   2.135 -axiomatization
   2.136 -  run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
   2.137 -
   2.138 -ML {*
   2.139 -signature RANDOM =
   2.140 -sig
   2.141 -  type seed = IntInf.int;
   2.142 -  val seed: unit -> seed;
   2.143 -  val value: IntInf.int -> seed -> IntInf.int * seed;
   2.144 -end;
   2.145 -
   2.146 -structure Random : RANDOM =
   2.147 -struct
   2.148 -
   2.149 -open IntInf;
   2.150 -
   2.151 -exception RANDOM;
   2.152 -
   2.153 -type seed = int;
   2.154 -
   2.155 -local
   2.156 -  val a = fromInt 16807;
   2.157 -    (*greetings to SML/NJ*)
   2.158 -  val m = (the o fromString) "2147483647";
   2.159 -in
   2.160 -  fun next s = (a * s) mod m;
   2.161 -end;
   2.162 -
   2.163 -local
   2.164 -  val seed_ref = ref (fromInt 1);
   2.165 -in
   2.166 -  fun seed () =
   2.167 -    let
   2.168 -      val r = next (!seed_ref)
   2.169 -    in
   2.170 -      (seed_ref := r; r)
   2.171 -    end;
   2.172 -end;
   2.173 -
   2.174 -fun value h s =
   2.175 -  if h < 1 then raise RANDOM
   2.176 -  else (s mod (h - 1), seed ());
   2.177 -
   2.178 -end;
   2.179 -*}
   2.180 -
   2.181 -code_type randseed
   2.182 -  (SML "Random.seed")
   2.183 -
   2.184 -code_const random_int
   2.185 -  (SML "Random.value")
   2.186 -
   2.187 -code_const run_random
   2.188 -  (SML "case _ (Random.seed ()) of (x, '_) => x")
   2.189 -
   2.190 -code_gen select select_weight
   2.191 -  (SML #)
   2.192 -
   2.193 -end
   2.194 \ No newline at end of file
     3.1 --- a/src/HOL/ex/CodeRevappl.thy	Tue Mar 27 09:19:37 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,42 +0,0 @@
     3.4 -(*  ID:         $Id$
     3.5 -    Author:     Florian Haftmann, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -header {* Combinators for structured results *}
     3.9 -
    3.10 -theory CodeRevappl
    3.11 -imports Main
    3.12 -begin
    3.13 -
    3.14 -section {* Combinators for structured results *}
    3.15 -
    3.16 -
    3.17 -subsection {* primitive definitions *}
    3.18 -
    3.19 -definition
    3.20 -  revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
    3.21 -  revappl_def: "x \<triangleright> f = f x"
    3.22 -  revappl_snd :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<times> 'b" (infixl "|\<triangleright>" 55)
    3.23 -  revappl_snd_split: "z |\<triangleright> f = (fst z , f (snd z))"
    3.24 -  revappl_swamp :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'd \<times> 'b) \<Rightarrow> ('c \<times> 'd) \<times> 'b" (infixl "|\<triangleright>\<triangleright>" 55)
    3.25 -  revappl_swamp_split: "z |\<triangleright>\<triangleright> f = ((fst z, fst (f (snd z))), snd (f (snd z)))"
    3.26 -  revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
    3.27 -  revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
    3.28 -
    3.29 -
    3.30 -subsection {* lemmas *}
    3.31 -
    3.32 -lemma revappl_snd_def [code]:
    3.33 -  "(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp
    3.34 -
    3.35 -lemma revappl_swamp_def [code]:
    3.36 -  "(y, x) |\<triangleright>\<triangleright> f = (let (z, w) = f x in ((y, z), w))" unfolding Let_def revappl_swamp_split split_def by simp
    3.37 -
    3.38 -lemma revappl_uncurry_def [code]:
    3.39 -  "(y, x) \<turnstile>\<triangleright> f = f y x" unfolding revappl_uncurry_split by simp
    3.40 -
    3.41 -lemmas revappl = revappl_def revappl_snd_def revappl_swamp_def revappl_uncurry_def
    3.42 -
    3.43 -lemmas revappl_split = revappl_def revappl_snd_split revappl_swamp_split revappl_uncurry_split
    3.44 -
    3.45 -end
    3.46 \ No newline at end of file
     4.1 --- a/src/HOL/ex/ROOT.ML	Tue Mar 27 09:19:37 2007 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Tue Mar 27 12:28:42 2007 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  no_document time_use_thy "Classpackage";
     4.6  no_document time_use_thy "Eval_examples";
     4.7 -no_document time_use_thy "CodeRandom";
     4.8 +no_document time_use_thy "Random";
     4.9  no_document time_use_thy "Codegenerator_Rat";
    4.10  no_document time_use_thy "Codegenerator";
    4.11  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/Random.thy	Tue Mar 27 12:28:42 2007 +0200
     5.3 @@ -0,0 +1,186 @@
     5.4 +(*  ID:         $Id$
     5.5 +    Author:     Florian Haftmann, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* A simple random engine *}
     5.9 +
    5.10 +theory Random
    5.11 +imports State_Monad
    5.12 +begin
    5.13 +
    5.14 +fun
    5.15 +  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
    5.16 +where
    5.17 +  pick_undef: "pick [] n = undefined"
    5.18 +  | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
    5.19 +lemmas [code nofunc] = pick_undef
    5.20 +
    5.21 +typedecl randseed
    5.22 +
    5.23 +axiomatization
    5.24 +  random_shift :: "randseed \<Rightarrow> randseed"
    5.25 +
    5.26 +axiomatization
    5.27 +  random_seed :: "randseed \<Rightarrow> nat"
    5.28 +
    5.29 +definition
    5.30 +  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where
    5.31 +  "random n s = (random_seed s mod n, random_shift s)"
    5.32 +
    5.33 +lemma random_bound:
    5.34 +  assumes "0 < n"
    5.35 +  shows "fst (random n s) < n"
    5.36 +proof -
    5.37 +  from prems mod_less_divisor have "!!m .m mod n < n" by auto
    5.38 +  then show ?thesis unfolding random_def by simp 
    5.39 +qed
    5.40 +
    5.41 +lemma random_random_seed [simp]:
    5.42 +  "snd (random n s) = random_shift s" unfolding random_def by simp
    5.43 +
    5.44 +definition
    5.45 +  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
    5.46 +  [simp]: "select xs = (do
    5.47 +      n \<leftarrow> random (length xs);
    5.48 +      return (nth xs n)
    5.49 +    done)"
    5.50 +definition
    5.51 +  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where
    5.52 +  [simp]: "select_weight xs = (do
    5.53 +      n \<leftarrow> random (foldl (op +) 0 (map fst xs));
    5.54 +      return (pick xs n)
    5.55 +    done)"
    5.56 +
    5.57 +lemma
    5.58 +  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
    5.59 +proof (induct xs)
    5.60 +  case Nil show ?case by (simp add: monad_collapse random_def)
    5.61 +next
    5.62 +  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
    5.63 +  proof -
    5.64 +    fix xs
    5.65 +    fix y
    5.66 +    show "map fst (map (Pair y) xs) = replicate (length xs) y"
    5.67 +      by (induct xs) simp_all
    5.68 +  qed
    5.69 +  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
    5.70 +  proof -
    5.71 +    fix xs
    5.72 +    fix n
    5.73 +    assume "n < length xs"
    5.74 +    then show "pick (map (Pair 1) xs) n = nth xs n"
    5.75 +    proof (induct xs arbitrary: n)
    5.76 +      case Nil then show ?case by simp
    5.77 +    next
    5.78 +      case (Cons x xs) show ?case
    5.79 +      proof (cases n)
    5.80 +        case 0 then show ?thesis by simp
    5.81 +      next
    5.82 +        case (Suc _)
    5.83 +    from Cons have "n < length (x # xs)" by auto
    5.84 +        then have "n < Suc (length xs)" by simp
    5.85 +        with Suc have "n - 1 < Suc (length xs) - 1" by auto
    5.86 +        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
    5.87 +        with Suc show ?thesis by auto
    5.88 +      qed
    5.89 +    qed
    5.90 +  qed
    5.91 +  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
    5.92 +  proof -
    5.93 +    have replicate_append:
    5.94 +      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
    5.95 +      by (simp add: replicate_app_Cons_same)
    5.96 +    fix xs
    5.97 +    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
    5.98 +    unfolding map_fst_Pair proof (induct xs)
    5.99 +      case Nil show ?case by simp
   5.100 +    next
   5.101 +      case (Cons x xs) then show ?case unfolding replicate_append by simp
   5.102 +    qed
   5.103 +  qed
   5.104 +  have pick_nth_random:
   5.105 +    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
   5.106 +  proof -
   5.107 +    fix s
   5.108 +    fix x
   5.109 +    fix xs
   5.110 +    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
   5.111 +    from pick_nth [OF bound] show
   5.112 +      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
   5.113 +  qed
   5.114 +  have pick_nth_random_do:
   5.115 +    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
   5.116 +      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
   5.117 +  unfolding monad_collapse split_def unfolding pick_nth_random ..
   5.118 +  case (Cons x xs) then show ?case
   5.119 +    unfolding select_weight_def sum_length pick_nth_random_do
   5.120 +    by simp
   5.121 +qed
   5.122 +
   5.123 +definition
   5.124 +  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where
   5.125 +  "random_int k = (do n \<leftarrow> random (nat k); return (int n) done)"
   5.126 +
   5.127 +lemma random_nat [code]:
   5.128 +  "random n = (do k \<leftarrow> random_int (int n); return (nat k) done)"
   5.129 +unfolding random_int_def by simp
   5.130 +
   5.131 +axiomatization
   5.132 +  run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
   5.133 +
   5.134 +ML {*
   5.135 +signature RANDOM =
   5.136 +sig
   5.137 +  type seed = IntInf.int;
   5.138 +  val seed: unit -> seed;
   5.139 +  val value: IntInf.int -> seed -> IntInf.int * seed;
   5.140 +end;
   5.141 +
   5.142 +structure Random : RANDOM =
   5.143 +struct
   5.144 +
   5.145 +open IntInf;
   5.146 +
   5.147 +exception RANDOM;
   5.148 +
   5.149 +type seed = int;
   5.150 +
   5.151 +local
   5.152 +  val a = fromInt 16807;
   5.153 +    (*greetings to SML/NJ*)
   5.154 +  val m = (the o fromString) "2147483647";
   5.155 +in
   5.156 +  fun next s = (a * s) mod m;
   5.157 +end;
   5.158 +
   5.159 +local
   5.160 +  val seed_ref = ref (fromInt 1);
   5.161 +in
   5.162 +  fun seed () =
   5.163 +    let
   5.164 +      val r = next (!seed_ref)
   5.165 +    in
   5.166 +      (seed_ref := r; r)
   5.167 +    end;
   5.168 +end;
   5.169 +
   5.170 +fun value h s =
   5.171 +  if h < 1 then raise RANDOM
   5.172 +  else (s mod (h - 1), seed ());
   5.173 +
   5.174 +end;
   5.175 +*}
   5.176 +
   5.177 +code_type randseed
   5.178 +  (SML "Random.seed")
   5.179 +
   5.180 +code_const random_int
   5.181 +  (SML "Random.value")
   5.182 +
   5.183 +code_const run_random
   5.184 +  (SML "case _ (Random.seed ()) of (x, '_) => x")
   5.185 +
   5.186 +code_gen select select_weight
   5.187 +  (SML #)
   5.188 +
   5.189 +end