--- a/src/HOL/Code_Eval.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Code_Eval.thy Tue May 19 13:57:32 2009 +0200
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Eval
-imports Plain Typerep
+imports Plain Typerep Code_Index
begin
subsection {* Term representation *}
@@ -215,6 +215,9 @@
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
by (simp only: term_of_anything)
+lemma (in term_syntax) term_of_index_code [code]:
+ "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
+ by (simp only: term_of_anything)
subsection {* Obfuscate *}
--- a/src/HOL/Code_Index.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Code_Index.thy Tue May 19 13:57:32 2009 +0200
@@ -3,7 +3,7 @@
header {* Type of indices *}
theory Code_Index
-imports Main
+imports Nat_Numeral
begin
text {*
@@ -264,11 +264,6 @@
else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
by (auto simp add: int_of_def mod_div_equality')
-lemma (in term_syntax) term_of_index_code [code]:
- "Code_Eval.term_of k =
- Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k"
- by (simp only: term_of_anything)
-
hide (open) const of_nat nat_of int_of
--- a/src/HOL/Imperative_HOL/Array.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue May 19 13:57:32 2009 +0200
@@ -6,7 +6,7 @@
header {* Monadic arrays *}
theory Array
-imports Heap_Monad Code_Index
+imports Heap_Monad
begin
subsection {* Primitives *}
--- a/src/HOL/IsaMakefile Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/IsaMakefile Tue May 19 13:57:32 2009 +0200
@@ -212,15 +212,17 @@
Hilbert_Choice.thy \
IntDiv.thy \
Int.thy \
- Typerep.thy \
List.thy \
Main.thy \
Map.thy \
Nat_Numeral.thy \
Presburger.thy \
+ Quickcheck.thy \
+ Random.thy \
Recdef.thy \
SetInterval.thy \
String.thy \
+ Typerep.thy \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
$(SRC)/Provers/Arith/cancel_numerals.ML \
@@ -287,10 +289,8 @@
Transcendental.thy \
GCD.thy \
Parity.thy \
- Quickcheck.thy \
Lubs.thy \
PReal.thy \
- Random.thy \
Rational.thy \
RComplete.thy \
RealDef.thy \
--- a/src/HOL/Library/Code_Integer.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy Tue May 19 13:57:32 2009 +0200
@@ -5,7 +5,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports Main Code_Index
+imports Main
begin
text {*
--- a/src/HOL/Library/Efficient_Nat.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue May 19 13:57:32 2009 +0200
@@ -5,7 +5,7 @@
header {* Implementation of natural numbers by target-language integers *}
theory Efficient_Nat
-imports Code_Index Code_Integer Main
+imports Code_Integer Main
begin
text {*
--- a/src/HOL/Main.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Main.thy Tue May 19 13:57:32 2009 +0200
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Code_Eval Map Recdef SAT
+imports Plain Quickcheck Map Recdef SAT
begin
text {*
--- a/src/HOL/Quickcheck.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Quickcheck.thy Tue May 19 13:57:32 2009 +0200
@@ -3,7 +3,7 @@
header {* A simple counterexample generator *}
theory Quickcheck
-imports Main Real Random
+imports Random Code_Eval
begin
notation fcomp (infixl "o>" 60)
@@ -175,36 +175,6 @@
end
-definition (in term_syntax)
- 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
- [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
-
-instantiation rat :: random
-begin
-
-definition
- "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
- let j = Code_Index.int_of (denom + 1)
- in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
-
-instance ..
-
-end
-
-definition (in term_syntax)
- valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
-
-instantiation real :: random
-begin
-
-definition
- "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
-
-instance ..
-
-end
-
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Random.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Random.thy Tue May 19 13:57:32 2009 +0200
@@ -3,7 +3,7 @@
header {* A HOL random engine *}
theory Random
-imports Code_Index
+imports Code_Index List
begin
notation fcomp (infixl "o>" 60)
@@ -42,9 +42,6 @@
primrec seed_invariant :: "seed \<Rightarrow> bool" where
"seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
-lemma if_same: "(if b then f x else f y) = f (if b then x else y)"
- by (cases b) simp_all
-
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
"split_seed s = (let
(v, w) = s;
@@ -98,6 +95,14 @@
"pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
by (induct xs) (auto simp add: expand_fun_eq)
+lemma pick_same:
+ "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Index.of_nat l) = nth xs l"
+proof (induct xs arbitrary: l)
+ case Nil then show ?case by simp
+next
+ case (Cons x xs) then show ?case by (cases l) simp_all
+qed
+
definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
"select_weight xs = range (listsum (map fst xs))
o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
@@ -113,6 +118,27 @@
then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed
+lemma select_weigth_drop_zero:
+ "Random.select_weight (filter (\<lambda>(k, _). k > 0) xs) = Random.select_weight xs"
+proof -
+ have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
+ by (induct xs) auto
+ then show ?thesis by (simp only: select_weight_def pick_drop_zero)
+qed
+
+lemma select_weigth_select:
+ assumes "xs \<noteq> []"
+ shows "Random.select_weight (map (Pair 1) xs) = Random.select xs"
+proof -
+ have less: "\<And>s. fst (Random.range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)"
+ using assms by (intro range) simp
+ moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Index.of_nat (length xs)"
+ by (induct xs) simp_all
+ ultimately show ?thesis
+ by (auto simp add: select_weight_def select_def scomp_def split_def
+ expand_fun_eq pick_same [symmetric])
+qed
+
definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
[code del]: "select_default k x y = range k
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
@@ -169,7 +195,6 @@
hide (open) type seed
hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
iterate range select pick select_weight select_default
-hide (open) fact log_def
no_notation fcomp (infixl "o>" 60)
no_notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/Rational.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Rational.thy Tue May 19 13:57:32 2009 +0200
@@ -1001,6 +1001,28 @@
"Fract a b / Fract c d = Fract_norm (a * d) (b * c)"
by simp
+definition (in term_syntax)
+ 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
+ [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation rat :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>num. Random.range i o\<rightarrow> (\<lambda>denom. Pair (
+ let j = Code_Index.int_of (denom + 1)
+ in valterm_fract num (j, \<lambda>u. Code_Eval.term_of j))))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
hide (open) const Fract_norm
text {* Setup for SML code generator *}
--- a/src/HOL/RealDef.thy Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/RealDef.thy Tue May 19 13:57:32 2009 +0200
@@ -1126,6 +1126,26 @@
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
+definition (in term_syntax)
+ valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
+ [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation real :: random
+begin
+
+definition
+ "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
text {* Setup for SML code generator *}
types_code