1.1 --- a/src/HOL/Code_Eval.thy	Tue May 19 13:57:31 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Tue May 19 13:57:32 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Term evaluation using the generic code generator *}
     1.5  
     1.6  theory Code_Eval
     1.7 -imports Plain Typerep
     1.8 +imports Plain Typerep Code_Index
     1.9  begin
    1.10  
    1.11  subsection {* Term representation *}
    1.12 @@ -215,6 +215,9 @@
    1.13        else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
    1.14    by (simp only: term_of_anything)
    1.15  
    1.16 +lemma (in term_syntax) term_of_index_code [code]:
    1.17 +  "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
    1.18 +  by (simp only: term_of_anything)
    1.19  
    1.20  subsection {* Obfuscate *}
    1.21  

     2.1 --- a/src/HOL/Code_Index.thy	Tue May 19 13:57:31 2009 +0200
     2.2 +++ b/src/HOL/Code_Index.thy	Tue May 19 13:57:32 2009 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  header {* Type of indices *}
     2.5  
     2.6  theory Code_Index
     2.7 -imports Main
     2.8 +imports Nat_Numeral
     2.9  begin
    2.10  
    2.11  text {*
    2.12 @@ -264,11 +264,6 @@
    2.13      else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
    2.14    by (auto simp add: int_of_def mod_div_equality')
    2.15  
    2.16 -lemma (in term_syntax) term_of_index_code [code]:
    2.17 -  "Code_Eval.term_of k =
    2.18 -    Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k"
    2.19 -  by (simp only: term_of_anything)
    2.20 -
    2.21  hide (open) const of_nat nat_of int_of
    2.22  
    2.23  

     3.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue May 19 13:57:31 2009 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue May 19 13:57:32 2009 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Monadic arrays *}
     3.5  
     3.6  theory Array
     3.7 -imports Heap_Monad Code_Index
     3.8 +imports Heap_Monad
     3.9  begin
    3.10  
    3.11  subsection {* Primitives *}

     4.1 --- a/src/HOL/IsaMakefile	Tue May 19 13:57:31 2009 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Tue May 19 13:57:32 2009 +0200
     4.3 @@ -212,15 +212,17 @@
     4.4    Hilbert_Choice.thy \
     4.5    IntDiv.thy \
     4.6    Int.thy \
     4.7 -  Typerep.thy \
     4.8    List.thy \
     4.9    Main.thy \
    4.10    Map.thy \
    4.11    Nat_Numeral.thy \
    4.12    Presburger.thy \
    4.13 +  Quickcheck.thy \
    4.14 +  Random.thy \
    4.15    Recdef.thy \
    4.16    SetInterval.thy \
    4.17    String.thy \
    4.18 +  Typerep.thy \
    4.19    $(SRC)/Provers/Arith/assoc_fold.ML \
    4.20    $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
    4.21    $(SRC)/Provers/Arith/cancel_numerals.ML \
    4.22 @@ -287,10 +289,8 @@
    4.23    Transcendental.thy \
    4.24    GCD.thy \
    4.25    Parity.thy \
    4.26 -  Quickcheck.thy \
    4.27    Lubs.thy \
    4.28    PReal.thy \
    4.29 -  Random.thy \
    4.30    Rational.thy \
    4.31    RComplete.thy \
    4.32    RealDef.thy \

     5.1 --- a/src/HOL/Library/Code_Integer.thy	Tue May 19 13:57:31 2009 +0200
     5.2 +++ b/src/HOL/Library/Code_Integer.thy	Tue May 19 13:57:32 2009 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Pretty integer literals for code generation *}
     5.5  
     5.6  theory Code_Integer
     5.7 -imports Main Code_Index
     5.8 +imports Main
     5.9  begin
    5.10  
    5.11  text {*

     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:31 2009 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue May 19 13:57:32 2009 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Implementation of natural numbers by target-language integers *}
     6.5  
     6.6  theory Efficient_Nat
     6.7 -imports Code_Index Code_Integer Main
     6.8 +imports Code_Integer Main
     6.9  begin
    6.10  
    6.11  text {*

     7.1 --- a/src/HOL/Main.thy	Tue May 19 13:57:31 2009 +0200
     7.2 +++ b/src/HOL/Main.thy	Tue May 19 13:57:32 2009 +0200
     7.3 @@ -1,7 +1,7 @@
     7.4  header {* Main HOL *}
     7.5  
     7.6  theory Main
     7.7 -imports Plain Code_Eval Map Recdef SAT
     7.8 +imports Plain Quickcheck Map Recdef SAT
     7.9  begin
    7.10  
    7.11  text {*

     8.1 --- a/src/HOL/Quickcheck.thy	Tue May 19 13:57:31 2009 +0200
     8.2 +++ b/src/HOL/Quickcheck.thy	Tue May 19 13:57:32 2009 +0200
     8.3 @@ -3,7 +3,7 @@
     8.4  header {* A simple counterexample generator *}
     8.5  
     8.6  theory Quickcheck
     8.7 -imports Main Real Random
     8.8 +imports Random Code_Eval
     8.9  begin
    8.10  
    8.11  notation fcomp (infixl "o>" 60)
    8.12 @@ -175,36 +175,6 @@
    8.13  
    8.14  end
    8.15  
    8.16 -definition (in term_syntax)
    8.17 -  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
    8.18 -  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
    8.19 -
    8.20 -instantiation rat :: random
    8.21 -begin
    8.22 -
    8.23 -definition
    8.24 -  "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
    8.25 -     let j = Code_Index.int_of (denom + 1)
    8.26 -     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
    8.27 -
    8.28 -instance ..
    8.29 -
    8.30 -end
    8.31 -
    8.32 -definition (in term_syntax)
    8.33 -  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
    8.34 -  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
    8.35 -
    8.36 -instantiation real :: random
    8.37 -begin
    8.38 -
    8.39 -definition
    8.40 -  "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
    8.41 -
    8.42 -instance ..
    8.43 -
    8.44 -end
    8.45 -
    8.46  
    8.47  no_notation fcomp (infixl "o>" 60)
    8.48  no_notation scomp (infixl "o\<rightarrow>" 60)

     9.1 --- a/src/HOL/Random.thy	Tue May 19 13:57:31 2009 +0200
     9.2 +++ b/src/HOL/Random.thy	Tue May 19 13:57:32 2009 +0200
     9.3 @@ -3,7 +3,7 @@
     9.4  header {* A HOL random engine *}
     9.5  
     9.6  theory Random
     9.7 -imports Code_Index
     9.8 +imports Code_Index List
     9.9  begin
    9.10  
    9.11  notation fcomp (infixl "o>" 60)
    9.12 @@ -42,9 +42,6 @@
    9.13  primrec seed_invariant :: "seed \<Rightarrow> bool" where
    9.14    "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    9.15  
    9.16 -lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
    9.17 -  by (cases b) simp_all
    9.18 -
    9.19  definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
    9.20    "split_seed s = (let
    9.21       (v, w) = s;
    9.22 @@ -98,6 +95,14 @@
    9.23    "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
    9.24    by (induct xs) (auto simp add: expand_fun_eq)
    9.25  
    9.26 +lemma pick_same:
    9.27 +  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
    9.28 +proof (induct xs arbitrary: l)
    9.29 +  case Nil then show ?case by simp
    9.30 +next
    9.31 +  case (Cons x xs) then show ?case by (cases l) simp_all
    9.32 +qed
    9.33 +
    9.34  definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    9.35    "select_weight xs = range (listsum (map fst xs))
    9.36     o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
    9.37 @@ -113,6 +118,27 @@
    9.38    then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
    9.39  qed
    9.40  
    9.41 +lemma select_weigth_drop_zero:
    9.42 +  "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
    9.43 +proof -
    9.44 +  have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
    9.45 +    by (induct xs) auto
    9.46 +  then show ?thesis by (simp only: select_weight_def pick_drop_zero)
    9.47 +qed
    9.48 +
    9.49 +lemma select_weigth_select:
    9.50 +  assumes "xs \<noteq> []"
    9.51 +  shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
    9.52 +proof -
    9.53 +  have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
    9.54 +    using assms by (intro range) simp
    9.55 +  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
    9.56 +    by (induct xs) simp_all
    9.57 +  ultimately show ?thesis
    9.58 +    by (auto simp add: select_weight_def select_def scomp_def split_def
    9.59 +      expand_fun_eq pick_same [symmetric])
    9.60 +qed
    9.61 +
    9.62  definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    9.63    [code del]: "select_default k x y = range k
    9.64       o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
    9.65 @@ -169,7 +195,6 @@
    9.66  hide (open) type seed
    9.67  hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
    9.68    iterate range select pick select_weight select_default
    9.69 -hide (open) fact log_def
    9.70  
    9.71  no_notation fcomp (infixl "o>" 60)
    9.72  no_notation scomp (infixl "o\<rightarrow>" 60)

    10.1 --- a/src/HOL/Rational.thy	Tue May 19 13:57:31 2009 +0200
    10.2 +++ b/src/HOL/Rational.thy	Tue May 19 13:57:32 2009 +0200
    10.3 @@ -1001,6 +1001,28 @@
    10.4    "Fract a b / Fract c d = Fract_norm (a * d) (b * c)"
    10.5    by simp
    10.6  
    10.7 +definition (in term_syntax)
    10.8 +  valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
    10.9 +  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
   10.10 +
   10.11 +notation fcomp (infixl "o>" 60)
   10.12 +notation scomp (infixl "o\<rightarrow>" 60)
   10.13 +
   10.14 +instantiation rat :: random
   10.15 +begin
   10.16 +
   10.17 +definition
   10.18 +  "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
   10.19 +     let j = Code_Index.int_of (denom + 1)
   10.20 +     in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
   10.21 +
   10.22 +instance ..
   10.23 +
   10.24 +end
   10.25 +
   10.26 +no_notation fcomp (infixl "o>" 60)
   10.27 +no_notation scomp (infixl "o\<rightarrow>" 60)
   10.28 +
   10.29  hide (open) const Fract_norm
   10.30  
   10.31  text {* Setup for SML code generator *}

    11.1 --- a/src/HOL/RealDef.thy	Tue May 19 13:57:31 2009 +0200
    11.2 +++ b/src/HOL/RealDef.thy	Tue May 19 13:57:32 2009 +0200
    11.3 @@ -1126,6 +1126,26 @@
    11.4  lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
    11.5    by (simp add: of_rat_divide)
    11.6  
    11.7 +definition (in term_syntax)
    11.8 +  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
    11.9 +  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
   11.10 +
   11.11 +notation fcomp (infixl "o>" 60)
   11.12 +notation scomp (infixl "o\<rightarrow>" 60)
   11.13 +
   11.14 +instantiation real :: random
   11.15 +begin
   11.16 +
   11.17 +definition
   11.18 +  "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
   11.19 +
   11.20 +instance ..
   11.21 +
   11.22 +end
   11.23 +
   11.24 +no_notation fcomp (infixl "o>" 60)
   11.25 +no_notation scomp (infixl "o\<rightarrow>" 60)
   11.26 +
   11.27  text {* Setup for SML code generator *}
   11.28  
   11.29  types_code