# HG changeset patch
# User haftmann
# Date 1242734252 -7200
# Node ID 5c8fb4fd67e0e903e6adb2e96b541551adbda08c
# Parent  52d332f8f909db18757cb85ac22c7766c453bd42
moved Code_Index, Random and Quickcheck before Main

diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Code_Eval.thy
--- 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 *}
 
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Code_Index.thy
--- 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
 
 
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Imperative_HOL/Array.thy
--- 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 *}
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/IsaMakefile
--- 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 \
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Library/Code_Integer.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 {*
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Library/Efficient_Nat.thy
--- 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 {*
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Main.thy
--- 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 {*
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Quickcheck.thy
--- 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)
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Random.thy
--- 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)
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Rational.thy
--- 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 *}
diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/RealDef.thy
--- 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