--- a/src/HOL/Code_Eval.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Code_Eval.thy Mon May 18 23:15:56 2009 +0200
@@ -28,6 +28,14 @@
lemma term_of_anything: "term_of x \<equiv> t"
by (rule eq_reflection) (cases "term_of x", cases t, simp)
+definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
+ \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
+ "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
+
+lemma valapp_code [code, code inline]:
+ "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
+ by (simp only: valapp_def fst_conv snd_conv)
+
subsubsection {* @{text term_of} instances *}
@@ -135,6 +143,97 @@
code_reserved Eval HOLogic
+subsubsection {* Syntax *}
+
+definition termify :: "'a \<Rightarrow> term" where
+ [code del]: "termify x = dummy_term"
+
+abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
+ "valtermify x \<equiv> (x, \<lambda>u. termify x)"
+
+setup {*
+let
+ fun map_default f xs =
+ let val ys = map f xs
+ in if exists is_some ys
+ then SOME (map2 the_default xs ys)
+ else NONE
+ end;
+ fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
+ if not (Term.has_abs t)
+ then if fold_aterms (fn Const _ => I | _ => K false) t true
+ then SOME (HOLogic.reflect_term t)
+ else error "Cannot termify expression containing variables"
+ else error "Cannot termify expression containing abstraction"
+ | subst_termify_app (t, ts) = case map_default subst_termify ts
+ of SOME ts' => SOME (list_comb (t, ts'))
+ | NONE => NONE
+ and subst_termify (Abs (v, T, t)) = (case subst_termify t
+ of SOME t' => SOME (Abs (v, T, t'))
+ | NONE => NONE)
+ | subst_termify t = subst_termify_app (strip_comb t)
+ fun check_termify ts ctxt = map_default subst_termify ts
+ |> Option.map (rpair ctxt)
+in
+ Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+end;
+*}
+
+locale term_syntax
+begin
+
+notation App (infixl "<\<cdot>>" 70)
+ and valapp (infixl "{\<cdot>}" 70)
+
+end
+
+interpretation term_syntax .
+
+no_notation App (infixl "<\<cdot>>" 70)
+ and valapp (infixl "{\<cdot>}" 70)
+
+
+subsection {* Numeric types *}
+
+definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where
+ "term_of_num two = (\<lambda>_. dummy_term)"
+
+lemma (in term_syntax) term_of_num_code [code]:
+ "term_of_num two k = (if k = 0 then termify Int.Pls
+ else (if k mod two = 0
+ then termify Int.Bit0 <\<cdot>> term_of_num two (k div two)
+ else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))"
+ by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def)
+
+lemma (in term_syntax) term_of_nat_code [code]:
+ "term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n"
+ by (simp only: term_of_anything)
+
+lemma (in term_syntax) term_of_int_code [code]:
+ "term_of (k::int) = (if k = 0 then termify (0 :: int)
+ else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
+ 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)
+
+
+subsection {* Obfuscate *}
+
+print_translation {*
+let
+ val term = Const ("<TERM>", dummyT);
+ fun tr1' [_, _] = term;
+ fun tr2' [] = term;
+in
+ [(@{const_syntax Const}, tr1'),
+ (@{const_syntax App}, tr1'),
+ (@{const_syntax dummy_term}, tr2')]
+end
+*}
+
+hide const dummy_term App valapp
+hide (open) const Const termify valtermify term_of term_of_num
+
+
subsection {* Evaluation setup *}
ML {*
@@ -159,23 +258,4 @@
Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
*}
-
-subsubsection {* Syntax *}
-
-print_translation {*
-let
- val term = Const ("<TERM>", dummyT);
- fun tr1' [_, _] = term;
- fun tr2' [] = term;
-in
- [(@{const_syntax Const}, tr1'),
- (@{const_syntax App}, tr1'),
- (@{const_syntax dummy_term}, tr2')]
end
-*}
-
-hide const dummy_term
-hide (open) const Const App
-hide (open) const term_of
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Index.thy Mon May 18 23:15:56 2009 +0200
@@ -0,0 +1,330 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of indices *}
+
+theory Code_Index
+imports Main
+begin
+
+text {*
+ Indices are isomorphic to HOL @{typ nat} but
+ mapped to target-language builtin integers.
+*}
+
+subsection {* Datatype of indices *}
+
+typedef (open) index = "UNIV \<Colon> nat set"
+ morphisms nat_of of_nat by rule
+
+lemma of_nat_nat_of [simp]:
+ "of_nat (nat_of k) = k"
+ by (rule nat_of_inverse)
+
+lemma nat_of_of_nat [simp]:
+ "nat_of (of_nat n) = n"
+ by (rule of_nat_inverse) (rule UNIV_I)
+
+lemma [measure_function]:
+ "is_measure nat_of" by (rule is_measure_trivial)
+
+lemma index:
+ "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+ fix n :: nat
+ assume "\<And>n\<Colon>index. PROP P n"
+ then show "PROP P (of_nat n)" .
+next
+ fix n :: index
+ assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
+ then have "PROP P (of_nat (nat_of n))" .
+ then show "PROP P n" by simp
+qed
+
+lemma index_case:
+ assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
+ shows P
+ by (rule assms [of "nat_of k"]) simp
+
+lemma index_induct_raw:
+ assumes "\<And>n. P (of_nat n)"
+ shows "P k"
+proof -
+ from assms have "P (of_nat (nat_of k))" .
+ then show ?thesis by simp
+qed
+
+lemma nat_of_inject [simp]:
+ "nat_of k = nat_of l \<longleftrightarrow> k = l"
+ by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+ "of_nat n = of_nat m \<longleftrightarrow> n = m"
+ by (rule of_nat_inject) (rule UNIV_I)+
+
+instantiation index :: zero
+begin
+
+definition [simp, code del]:
+ "0 = of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+ "Suc_index k = of_nat (Suc (nat_of k))"
+
+rep_datatype "0 \<Colon> index" Suc_index
+proof -
+ fix P :: "index \<Rightarrow> bool"
+ fix k :: index
+ assume "P 0" then have init: "P (of_nat 0)" by simp
+ assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
+ then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
+ then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+ from init step have "P (of_nat (nat_of k))"
+ by (induct "nat_of k") simp_all
+ then show "P k" by simp
+qed simp_all
+
+declare index_case [case_names nat, cases type: index]
+declare index.induct [case_names nat, induct type: index]
+
+lemma index_decr [termination_simp]:
+ "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
+ by (cases k) simp
+
+lemma [simp, code]:
+ "index_size = nat_of"
+proof (rule ext)
+ fix k
+ have "index_size k = nat_size (nat_of k)"
+ by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
+ also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+ finally show "index_size k = nat_of k" .
+qed
+
+lemma [simp, code]:
+ "size = nat_of"
+proof (rule ext)
+ fix k
+ show "size k = nat_of k"
+ by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
+qed
+
+lemmas [code del] = index.recs index.cases
+
+lemma [code]:
+ "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
+ by (cases k, cases l) (simp add: eq)
+
+lemma [code nbe]:
+ "eq_class.eq (k::index) k \<longleftrightarrow> True"
+ by (rule HOL.eq_refl)
+
+
+subsection {* Indices as datatype of ints *}
+
+instantiation index :: number
+begin
+
+definition
+ "number_of = of_nat o nat"
+
+instance ..
+
+end
+
+lemma nat_of_number [simp]:
+ "nat_of (number_of k) = number_of k"
+ by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
+
+code_datatype "number_of \<Colon> int \<Rightarrow> index"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+ "(1\<Colon>index) = of_nat 1"
+
+definition [simp, code del]:
+ "n + m = of_nat (nat_of n + nat_of m)"
+
+definition [simp, code del]:
+ "n - m = of_nat (nat_of n - nat_of m)"
+
+definition [simp, code del]:
+ "n * m = of_nat (nat_of n * nat_of m)"
+
+definition [simp, code del]:
+ "n div m = of_nat (nat_of n div nat_of m)"
+
+definition [simp, code del]:
+ "n mod m = of_nat (nat_of n mod nat_of m)"
+
+definition [simp, code del]:
+ "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+ "n < m \<longleftrightarrow> nat_of n < nat_of m"
+
+instance proof
+qed (auto simp add: index left_distrib div_mult_self1)
+
+end
+
+lemma zero_index_code [code inline, code]:
+ "(0\<Colon>index) = Numeral0"
+ by (simp add: number_of_index_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>index)"
+ using zero_index_code ..
+
+lemma one_index_code [code inline, code]:
+ "(1\<Colon>index) = Numeral1"
+ by (simp add: number_of_index_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>index)"
+ using one_index_code ..
+
+lemma plus_index_code [code nbe]:
+ "of_nat n + of_nat m = of_nat (n + m)"
+ by simp
+
+definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
+ [simp, code del]: "subtract_index = op -"
+
+lemma subtract_index_code [code nbe]:
+ "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
+ by simp
+
+lemma minus_index_code [code]:
+ "n - m = subtract_index n m"
+ by simp
+
+lemma times_index_code [code nbe]:
+ "of_nat n * of_nat m = of_nat (n * m)"
+ by simp
+
+lemma less_eq_index_code [code nbe]:
+ "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
+ by simp
+
+lemma less_index_code [code nbe]:
+ "of_nat n < of_nat m \<longleftrightarrow> n < m"
+ by simp
+
+lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
+
+lemma of_nat_code [code]:
+ "of_nat = Nat.of_nat"
+proof
+ fix n :: nat
+ have "Nat.of_nat n = of_nat n"
+ by (induct n) simp_all
+ then show "of_nat n = Nat.of_nat n"
+ by (rule sym)
+qed
+
+lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+ by (cases i) auto
+
+definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
+ "nat_of_aux i n = nat_of i + n"
+
+lemma nat_of_aux_code [code]:
+ "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+ by (auto simp add: nat_of_aux_def index_not_eq_zero)
+
+lemma nat_of_code [code]:
+ "nat_of i = nat_of_aux i 0"
+ by (simp add: nat_of_aux_def)
+
+definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
+ [code del]: "div_mod_index n m = (n div m, n mod m)"
+
+lemma [code]:
+ "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+ unfolding div_mod_index_def by auto
+
+lemma [code]:
+ "n div m = fst (div_mod_index n m)"
+ unfolding div_mod_index_def by simp
+
+lemma [code]:
+ "n mod m = snd (div_mod_index n m)"
+ unfolding div_mod_index_def by simp
+
+definition int_of :: "index \<Rightarrow> int" where
+ "int_of = Nat.of_nat o nat_of"
+
+lemma int_of_code [code]:
+ "int_of k = (if k = 0 then 0
+ 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
+
+
+subsection {* Code generator setup *}
+
+text {* Implementation of indices by bounded integers *}
+
+code_type index
+ (SML "int")
+ (OCaml "int")
+ (Haskell "Int")
+
+code_instance index :: eq
+ (Haskell -)
+
+setup {*
+ fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
+ false false) ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML Int int
+code_reserved OCaml Pervasives int
+
+code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+ (SML "Int.+/ ((_),/ (_))")
+ (OCaml "Pervasives.( + )")
+ (Haskell infixl 6 "+")
+
+code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+ (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+ (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+ (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+ (SML "Int.*/ ((_),/ (_))")
+ (OCaml "Pervasives.( * )")
+ (Haskell infixl 7 "*")
+
+code_const div_mod_index
+ (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+ (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+ (Haskell "divMod")
+
+code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+ (SML "!((_ : Int.int) = _)")
+ (OCaml "!((_ : int) = _)")
+ (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+ (SML "Int.<=/ ((_),/ (_))")
+ (OCaml "!((_ : int) <= _)")
+ (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+ (SML "Int.</ ((_),/ (_))")
+ (OCaml "!((_ : int) < _)")
+ (Haskell infix 4 "<")
+
+end
--- a/src/HOL/Complex_Main.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Complex_Main.thy Mon May 18 23:15:56 2009 +0200
@@ -9,6 +9,7 @@
Ln
Taylor
Integration
+ Quickcheck
begin
end
--- a/src/HOL/Extraction/Higman.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Extraction/Higman.thy Mon May 18 23:15:56 2009 +0200
@@ -349,9 +349,9 @@
end
-function mk_word_aux :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_aux k = (do
- i \<leftarrow> range 10;
+ i \<leftarrow> Random.range 10;
(if i > 7 \<and> k > 2 \<or> k > 1000 then return []
else do
let l = (if i mod 2 = 0 then A else B);
@@ -362,10 +362,10 @@
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
-definition mk_word :: "seed \<Rightarrow> letter list \<times> seed" where
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word = mk_word_aux 0"
-primrec mk_word_s :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_s 0 = mk_word"
| "mk_word_s (Suc n) = (do
_ \<leftarrow> mk_word;
--- a/src/HOL/IsaMakefile Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/IsaMakefile Mon May 18 23:15:56 2009 +0200
@@ -206,6 +206,7 @@
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
ATP_Linkup.thy \
Code_Eval.thy \
+ Code_Index.thy \
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
@@ -286,8 +287,10 @@
Transcendental.thy \
GCD.thy \
Parity.thy \
+ Quickcheck.thy \
Lubs.thy \
PReal.thy \
+ Random.thy \
Rational.thy \
RComplete.thy \
RealDef.thy \
@@ -333,12 +336,11 @@
Library/comm_ring.ML Library/Coinductive_List.thy \
Library/AssocList.thy Library/Formal_Power_Series.thy \
Library/Binomial.thy Library/Eval_Witness.thy \
- Library/Code_Index.thy Library/Code_Char.thy \
+ Library/Code_Char.thy \
Library/Code_Char_chr.thy Library/Code_Integer.thy \
Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
Library/Boolean_Algebra.thy Library/Countable.thy \
Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \
- Library/Random.thy Library/Quickcheck.thy \
Library/Poly_Deriv.thy \
Library/Polynomial.thy \
Library/Preorder.thy \
@@ -851,7 +853,7 @@
ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
- ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy \
+ ex/Sudoku.thy ex/Tarski.thy \
ex/Termination.thy ex/Unification.thy ex/document/root.bib \
ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
--- a/src/HOL/Library/Code_Index.thy Mon May 18 23:15:38 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Type of indices *}
-
-theory Code_Index
-imports Main
-begin
-
-text {*
- Indices are isomorphic to HOL @{typ nat} but
- mapped to target-language builtin integers.
-*}
-
-subsection {* Datatype of indices *}
-
-typedef (open) index = "UNIV \<Colon> nat set"
- morphisms nat_of of_nat by rule
-
-lemma of_nat_nat_of [simp]:
- "of_nat (nat_of k) = k"
- by (rule nat_of_inverse)
-
-lemma nat_of_of_nat [simp]:
- "nat_of (of_nat n) = n"
- by (rule of_nat_inverse) (rule UNIV_I)
-
-lemma [measure_function]:
- "is_measure nat_of" by (rule is_measure_trivial)
-
-lemma index:
- "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
- fix n :: nat
- assume "\<And>n\<Colon>index. PROP P n"
- then show "PROP P (of_nat n)" .
-next
- fix n :: index
- assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
- then have "PROP P (of_nat (nat_of n))" .
- then show "PROP P n" by simp
-qed
-
-lemma index_case:
- assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
- shows P
- by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
- assumes "\<And>n. P (of_nat n)"
- shows "P k"
-proof -
- from assms have "P (of_nat (nat_of k))" .
- then show ?thesis by simp
-qed
-
-lemma nat_of_inject [simp]:
- "nat_of k = nat_of l \<longleftrightarrow> k = l"
- by (rule nat_of_inject)
-
-lemma of_nat_inject [simp]:
- "of_nat n = of_nat m \<longleftrightarrow> n = m"
- by (rule of_nat_inject) (rule UNIV_I)+
-
-instantiation index :: zero
-begin
-
-definition [simp, code del]:
- "0 = of_nat 0"
-
-instance ..
-
-end
-
-definition [simp]:
- "Suc_index k = of_nat (Suc (nat_of k))"
-
-rep_datatype "0 \<Colon> index" Suc_index
-proof -
- fix P :: "index \<Rightarrow> bool"
- fix k :: index
- assume "P 0" then have init: "P (of_nat 0)" by simp
- assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
- then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
- from init step have "P (of_nat (nat_of k))"
- by (induct "nat_of k") simp_all
- then show "P k" by simp
-qed simp_all
-
-declare index_case [case_names nat, cases type: index]
-declare index.induct [case_names nat, induct type: index]
-
-lemma index_decr [termination_simp]:
- "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
- by (cases k) simp
-
-lemma [simp, code]:
- "index_size = nat_of"
-proof (rule ext)
- fix k
- have "index_size k = nat_size (nat_of k)"
- by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
- also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
- finally show "index_size k = nat_of k" .
-qed
-
-lemma [simp, code]:
- "size = nat_of"
-proof (rule ext)
- fix k
- show "size k = nat_of k"
- by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
-qed
-
-lemmas [code del] = index.recs index.cases
-
-lemma [code]:
- "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
- by (cases k, cases l) (simp add: eq)
-
-lemma [code nbe]:
- "eq_class.eq (k::index) k \<longleftrightarrow> True"
- by (rule HOL.eq_refl)
-
-
-subsection {* Indices as datatype of ints *}
-
-instantiation index :: number
-begin
-
-definition
- "number_of = of_nat o nat"
-
-instance ..
-
-end
-
-lemma nat_of_number [simp]:
- "nat_of (number_of k) = number_of k"
- by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
-
-code_datatype "number_of \<Colon> int \<Rightarrow> index"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
- "(1\<Colon>index) = of_nat 1"
-
-definition [simp, code del]:
- "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
- "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
- "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
- "n div m = of_nat (nat_of n div nat_of m)"
-
-definition [simp, code del]:
- "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
- "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
- "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: index left_distrib div_mult_self1)
-
-end
-
-lemma zero_index_code [code inline, code]:
- "(0\<Colon>index) = Numeral0"
- by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
- using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
- "(1\<Colon>index) = Numeral1"
- by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
- using one_index_code ..
-
-lemma plus_index_code [code nbe]:
- "of_nat n + of_nat m = of_nat (n + m)"
- by simp
-
-definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
- [simp, code del]: "subtract_index = op -"
-
-lemma subtract_index_code [code nbe]:
- "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
- by simp
-
-lemma minus_index_code [code]:
- "n - m = subtract_index n m"
- by simp
-
-lemma times_index_code [code nbe]:
- "of_nat n * of_nat m = of_nat (n * m)"
- by simp
-
-lemma less_eq_index_code [code nbe]:
- "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
- by simp
-
-lemma less_index_code [code nbe]:
- "of_nat n < of_nat m \<longleftrightarrow> n < m"
- by simp
-
-lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-
-lemma of_nat_code [code]:
- "of_nat = Nat.of_nat"
-proof
- fix n :: nat
- have "Nat.of_nat n = of_nat n"
- by (induct n) simp_all
- then show "of_nat n = Nat.of_nat n"
- by (rule sym)
-qed
-
-lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
- by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
- "nat_of_aux i n = nat_of i + n"
-
-lemma nat_of_aux_code [code]:
- "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
- by (auto simp add: nat_of_aux_def index_not_eq_zero)
-
-lemma nat_of_code [code]:
- "nat_of i = nat_of_aux i 0"
- by (simp add: nat_of_aux_def)
-
-definition div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
- [code del]: "div_mod_index n m = (n div m, n mod m)"
-
-lemma [code]:
- "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
- unfolding div_mod_index_def by auto
-
-lemma [code]:
- "n div m = fst (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-lemma [code]:
- "n mod m = snd (div_mod_index n m)"
- unfolding div_mod_index_def by simp
-
-hide (open) const of_nat nat_of
-
-subsection {* ML interface *}
-
-ML {*
-structure Index =
-struct
-
-fun mk k = HOLogic.mk_number @{typ index} k;
-
-end;
-*}
-
-
-subsection {* Code generator setup *}
-
-text {* Implementation of indices by bounded integers *}
-
-code_type index
- (SML "int")
- (OCaml "int")
- (Haskell "Int")
-
-code_instance index :: eq
- (Haskell -)
-
-setup {*
- fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
- false false) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML Int int
-code_reserved OCaml Pervasives int
-
-code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.+/ ((_),/ (_))")
- (OCaml "Pervasives.( + )")
- (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.max/ (_/ -/ _,/ 0 : int)")
- (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
- (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
- (SML "Int.*/ ((_),/ (_))")
- (OCaml "Pervasives.( * )")
- (Haskell infixl 7 "*")
-
-code_const div_mod_index
- (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
- (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
- (Haskell "divMod")
-
-code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
- (OCaml "!((_ : int) = _)")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.<=/ ((_),/ (_))")
- (OCaml "!((_ : int) <= _)")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
- (SML "Int.</ ((_),/ (_))")
- (OCaml "!((_ : int) < _)")
- (Haskell infix 4 "<")
-
-text {* Evaluation *}
-
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
-
-code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
- (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
-
-end
--- a/src/HOL/Library/Code_Integer.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy Mon May 18 23:15:56 2009 +0200
@@ -5,7 +5,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports Main
+imports Main Code_Index
begin
text {*
@@ -91,15 +91,17 @@
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
+code_const Code_Index.int_of
+ (SML "IntInf.fromInt")
+ (OCaml "Big'_int.big'_int'_of'_int")
+ (Haskell "toEnum")
+
code_reserved SML IntInf
code_reserved OCaml Big_int
text {* Evaluation *}
-lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
-
code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
- (SML "HOLogic.mk'_number/ HOLogic.intT")
+ (Eval "HOLogic.mk'_number/ HOLogic.intT")
end
\ No newline at end of file
--- a/src/HOL/Library/Enum.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Library/Enum.thy Mon May 18 23:15:56 2009 +0200
@@ -116,9 +116,8 @@
by (simp add: length_n_lists)
qed
-lemma map_of_zip_map:
- fixes f :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>enum"
- shows "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
+lemma map_of_zip_map: (*FIXME move to Map.thy*)
+ "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
by (induct xs) (simp_all add: expand_fun_eq)
lemma map_of_zip_enum_is_Some:
--- a/src/HOL/Library/Library.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Library/Library.thy Mon May 18 23:15:56 2009 +0200
@@ -9,7 +9,6 @@
Boolean_Algebra
Char_ord
Code_Char_chr
- Code_Index
Code_Integer
Coinductive_List
Commutative_Ring
@@ -45,11 +44,9 @@
Preorder
Primes
Product_Vector
- Quickcheck
Quicksort
Quotient
Ramsey
- Random
Reflection
RBT
State_Monad
--- a/src/HOL/Library/Quickcheck.thy Mon May 18 23:15:38 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A simple counterexample generator *}
-
-theory Quickcheck
-imports Random Code_Eval Map
-begin
-
-subsection {* The @{text random} class *}
-
-class random = typerep +
- fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
-
-text {* Type @{typ "'a itself"} *}
-
-instantiation itself :: ("{type, typerep}") random
-begin
-
-definition
- "random _ = Pair (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
-
-instance ..
-
-end
-
-
-subsection {* Quickcheck generator *}
-
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name Pair}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-end;
-
-structure Quickcheck =
-struct
-
-open Quickcheck;
-
-val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
-
-val target = "Quickcheck";
-
-fun mk_generator_expr thy prop tys =
- let
- val bound_max = length tys - 1;
- val bounds = map_index (fn (i, ty) =>
- (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
- val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
- val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
- val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
- $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
- val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
- fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
- fun mk_split ty = Sign.mk_const thy
- (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
- fun mk_scomp_split ty t t' =
- StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
- (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
- fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
- (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
- val t = fold_rev mk_bindclause bounds (return $ check);
- in Abs ("n", @{typ index}, t) end;
-
-fun compile_generator_expr thy t =
- let
- val tys = (map snd o fst o strip_abs) t;
- val t' = mk_generator_expr thy t tys;
- val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g (s + 1) #>> (Option.map o map) proc) thy t' [];
- in f #> Random_Engine.run end;
-
-end
-*}
-
-setup {*
- Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
- #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
-*}
-
-
-subsection {* Type @{typ "'a \<Rightarrow> 'b"} *}
-
-ML {*
-structure Random_Engine =
-struct
-
-open Random_Engine;
-
-fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
- (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
- (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
- (seed : Random_Engine.seed) =
- let
- val (seed', seed'') = random_split seed;
- val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
- val fun_upd = Const (@{const_name fun_upd},
- (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
- fun random_fun' x =
- let
- val (seed, fun_map, f_t) = ! state;
- in case AList.lookup (uncurry eq) fun_map x
- of SOME y => y
- | NONE => let
- val t1 = term_of x;
- val ((y, t2), seed') = random seed;
- val fun_map' = (x, y) :: fun_map;
- val f_t' = fun_upd $ f_t $ t1 $ t2 ();
- val _ = state := (seed', fun_map', f_t');
- in y end
- end;
- fun term_fun' () = #3 (! state);
- in ((random_fun', term_fun'), seed'') end;
-
-end
-*}
-
-axiomatization
- random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
- \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
- \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
-
-code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
- -- {* With enough criminal energy this can be abused to derive @{prop False};
- for this reason we use a distinguished target @{text Quickcheck}
- not spoiling the regular trusted code generation *}
-
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
-begin
-
-definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
- "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
-
-instance ..
-
-end
-
-code_reserved Quickcheck Random_Engine
-
-end
--- a/src/HOL/Library/Random.thy Mon May 18 23:15:38 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A HOL random engine *}
-
-theory Random
-imports Code_Index
-begin
-
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
-
-
-subsection {* Auxiliary functions *}
-
-definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
- "inc_shift v k = (if v = k then 1 else k + 1)"
-
-definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
- "minus_shift r k l = (if k < l then r + k - l else k - l)"
-
-fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
- "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
-
-
-subsection {* Random seeds *}
-
-types seed = "index \<times> index"
-
-primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
- "next (v, w) = (let
- k = v div 53668;
- v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
- l = w div 52774;
- w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
- z = minus_shift 2147483562 v' (w' + 1) + 1
- in (z, (v', w')))"
-
-lemma next_not_0:
- "fst (next s) \<noteq> 0"
- by (cases s) (auto simp add: minus_shift_def Let_def)
-
-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;
- (v', w') = snd (next s);
- v'' = inc_shift 2147483562 v;
- s'' = (v'', w');
- w'' = inc_shift 2147483398 w;
- s''' = (v', w'')
- in (s'', s'''))"
-
-
-subsection {* Base selectors *}
-
-fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
- "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
-
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
- "range k = iterate (log 2147483561 k)
- (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
- o\<rightarrow> (\<lambda>v. Pair (v mod k))"
-
-lemma range:
- "k > 0 \<Longrightarrow> fst (range k s) < k"
- by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
-
-definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
- "select xs = range (Code_Index.of_nat (length xs))
- o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
-
-lemma select:
- assumes "xs \<noteq> []"
- shows "fst (select xs s) \<in> set xs"
-proof -
- from assms have "Code_Index.of_nat (length xs) > 0" by simp
- with range have
- "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
- then have
- "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
- then show ?thesis
- by (simp add: scomp_apply split_beta select_def)
-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))"
-
-lemma select_default_zero:
- "fst (select_default 0 x y s) = y"
- by (simp add: scomp_apply split_beta select_default_def)
-
-lemma select_default_code [code]:
- "select_default k x y = (if k = 0
- then range 1 o\<rightarrow> (\<lambda>_. Pair y)
- else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
-proof
- fix s
- have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
- by (simp add: range_def scomp_Pair scomp_apply split_beta)
- then show "select_default k x y s = (if k = 0
- then range 1 o\<rightarrow> (\<lambda>_. Pair y)
- else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
- by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
-qed
-
-
-subsection {* @{text ML} interface *}
-
-ML {*
-structure Random_Engine =
-struct
-
-type seed = int * int;
-
-local
-
-val seed = ref
- (let
- val now = Time.toMilliseconds (Time.now ());
- val (q, s1) = IntInf.divMod (now, 2147483562);
- val s2 = q mod 2147483398;
- in (s1 + 1, s2 + 1) end);
-
-in
-
-fun run f =
- let
- val (x, seed') = f (! seed);
- val _ = seed := seed'
- in x end;
-
-end;
-
-end;
-*}
-
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
-
-end
-
--- a/src/HOL/Nat_Numeral.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Mon May 18 23:15:56 2009 +0200
@@ -316,13 +316,13 @@
lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
by (simp add: nat_number_of_def)
-lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
by (simp add: nat_number_of_def)
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
by (simp add: nat_1 nat_number_of_def)
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
by (simp add: nat_numeral_1_eq_1)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck.thy Mon May 18 23:15:56 2009 +0200
@@ -0,0 +1,212 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A simple counterexample generator *}
+
+theory Quickcheck
+imports Main Real Random
+begin
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* The @{text random} class *}
+
+class random = typerep +
+ fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+
+subsection {* Quickcheck generator *}
+
+ML {*
+structure Quickcheck =
+struct
+
+open Quickcheck;
+
+val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop tys =
+ let
+ val bound_max = length tys - 1;
+ val bounds = map_index (fn (i, ty) =>
+ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
+ val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+ val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
+ val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
+ $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
+ val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
+ fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+ fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
+ fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+ fun mk_split ty = Sign.mk_const thy
+ (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+ fun mk_scomp_split ty t t' =
+ mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
+ (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
+ fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
+ (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
+ in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
+
+fun compile_generator_expr thy t =
+ let
+ val tys = (map snd o fst o strip_abs) t;
+ val t' = mk_generator_expr thy t tys;
+ val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ in f #> Random_Engine.run end;
+
+end
+*}
+
+setup {*
+ Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
+ #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
+*}
+
+
+subsection {* Fundamental types*}
+
+instantiation bool :: random
+begin
+
+definition
+ "random i = Random.range i o\<rightarrow>
+ (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
+
+instance ..
+
+end
+
+instantiation itself :: (typerep) random
+begin
+
+definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+ "random_itself _ = Pair (Code_Eval.valtermify TYPE('a))"
+
+instance ..
+
+end
+
+text {* Type @{typ "'a \<Rightarrow> 'b"} *}
+
+ML {*
+structure Random_Engine =
+struct
+
+open Random_Engine;
+
+fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
+ (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
+ (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
+ (seed : Random_Engine.seed) =
+ let
+ val (seed', seed'') = random_split seed;
+ val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
+ val fun_upd = Const (@{const_name fun_upd},
+ (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
+ fun random_fun' x =
+ let
+ val (seed, fun_map, f_t) = ! state;
+ in case AList.lookup (uncurry eq) fun_map x
+ of SOME y => y
+ | NONE => let
+ val t1 = term_of x;
+ val ((y, t2), seed') = random seed;
+ val fun_map' = (x, y) :: fun_map;
+ val f_t' = fun_upd $ f_t $ t1 $ t2 ();
+ val _ = state := (seed', fun_map', f_t');
+ in y end
+ end;
+ fun term_fun' () = #3 (! state);
+ in ((random_fun', term_fun'), seed'') end;
+
+end
+*}
+
+axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+ \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
+ \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
+ -- {* With enough criminal energy this can be abused to derive @{prop False};
+ for this reason we use a distinguished target @{text Quickcheck}
+ not spoiling the regular trusted code generation *}
+
+instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+begin
+
+definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+ "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
+
+instance ..
+
+end
+
+code_reserved Quickcheck Random_Engine
+
+
+subsection {* Numeric types *}
+
+instantiation nat :: random
+begin
+
+definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+ "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
+ let n = Code_Index.nat_of k
+ in (n, \<lambda>_. Code_Eval.term_of n)))"
+
+instance ..
+
+end
+
+instantiation int :: random
+begin
+
+definition
+ "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
+ let j = (if k \<ge> i then Code_Index.int_of (k - i) else - Code_Index.int_of (i - k))
+ in (j, \<lambda>_. Code_Eval.term_of j)))"
+
+instance ..
+
+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)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Random.thy Mon May 18 23:15:56 2009 +0200
@@ -0,0 +1,178 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A HOL random engine *}
+
+theory Random
+imports Code_Index
+begin
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* Auxiliary functions *}
+
+definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where
+ "inc_shift v k = (if v = k then 1 else k + 1)"
+
+definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where
+ "minus_shift r k l = (if k < l then r + k - l else k - l)"
+
+fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
+ "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
+
+
+subsection {* Random seeds *}
+
+types seed = "index \<times> index"
+
+primrec "next" :: "seed \<Rightarrow> index \<times> seed" where
+ "next (v, w) = (let
+ k = v div 53668;
+ v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
+ l = w div 52774;
+ w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
+ z = minus_shift 2147483562 v' (w' + 1) + 1
+ in (z, (v', w')))"
+
+lemma next_not_0:
+ "fst (next s) \<noteq> 0"
+ by (cases s) (auto simp add: minus_shift_def Let_def)
+
+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;
+ (v', w') = snd (next s);
+ v'' = inc_shift 2147483562 v;
+ s'' = (v'', w');
+ w'' = inc_shift 2147483398 w;
+ s''' = (v', w'')
+ in (s'', s'''))"
+
+
+subsection {* Base selectors *}
+
+fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+ "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
+
+definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+ "range k = iterate (log 2147483561 k)
+ (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
+ o\<rightarrow> (\<lambda>v. Pair (v mod k))"
+
+lemma range:
+ "k > 0 \<Longrightarrow> fst (range k s) < k"
+ by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
+
+definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+ "select xs = range (Code_Index.of_nat (length xs))
+ o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+
+lemma select:
+ assumes "xs \<noteq> []"
+ shows "fst (select xs s) \<in> set xs"
+proof -
+ from assms have "Code_Index.of_nat (length xs) > 0" by simp
+ with range have
+ "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
+ then have
+ "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
+ then show ?thesis
+ by (simp add: scomp_apply split_beta select_def)
+qed
+
+primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+ "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
+
+lemma pick_member:
+ "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
+ by (induct xs arbitrary: i) simp_all
+
+lemma pick_drop_zero:
+ "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
+ by (induct xs) (auto simp add: expand_fun_eq)
+
+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))"
+
+lemma select_weight_member:
+ assumes "0 < listsum (map fst xs)"
+ shows "fst (select_weight xs s) \<in> set (map snd xs)"
+proof -
+ from range assms
+ have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
+ with pick_member
+ have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
+ then show ?thesis by (simp add: select_weight_def scomp_def split_def)
+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))"
+
+lemma select_default_zero:
+ "fst (select_default 0 x y s) = y"
+ by (simp add: scomp_apply split_beta select_default_def)
+
+lemma select_default_code [code]:
+ "select_default k x y = (if k = 0
+ then range 1 o\<rightarrow> (\<lambda>_. Pair y)
+ else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
+proof
+ fix s
+ have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
+ by (simp add: range_def scomp_Pair scomp_apply split_beta)
+ then show "select_default k x y s = (if k = 0
+ then range 1 o\<rightarrow> (\<lambda>_. Pair y)
+ else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
+ by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
+qed
+
+
+subsection {* @{text ML} interface *}
+
+ML {*
+structure Random_Engine =
+struct
+
+type seed = int * int;
+
+local
+
+val seed = ref
+ (let
+ val now = Time.toMilliseconds (Time.now ());
+ val (q, s1) = IntInf.divMod (now, 2147483562);
+ val s2 = q mod 2147483398;
+ in (s1 + 1, s2 + 1) end);
+
+in
+
+fun run f =
+ let
+ val (x, seed') = f (! seed);
+ val _ = seed := seed'
+ in x end;
+
+end;
+
+end;
+*}
+
+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)
+
+end
+
--- a/src/HOL/Tools/hologic.ML Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Mon May 18 23:15:56 2009 +0200
@@ -122,6 +122,8 @@
val mk_typerep: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
+ val mk_return: typ -> typ -> term -> term
+ val mk_ST: ((term * typ) * (string * typ) option) list -> term -> typ -> typ option * typ -> term
end;
structure HOLogic: HOLOGIC =
@@ -612,8 +614,23 @@
| reflect_term (t1 $ t2) =
Const ("Code_Eval.App", termT --> termT --> termT)
$ reflect_term t1 $ reflect_term t2
- | reflect_term (t as Free _) = t
- | reflect_term (t as Bound _) = t
- | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
+ | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
+ | reflect_term t = t;
+
+
+(* open state monads *)
+
+fun mk_return T U x = pair_const T U $ x;
+
+fun mk_ST clauses t U (someT, V) =
+ let
+ val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
+ fun mk_clause ((t, U), SOME (v, T)) (t', U') =
+ (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
+ $ t $ lambda (Free (v, T)) t', U)
+ | mk_clause ((t, U), NONE) (t', U') =
+ (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
+ $ t $ t', U)
+ in fold_rev mk_clause clauses (t, U) |> fst end;
end;
--- a/src/HOL/ex/Predicate_Compile_ex.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Mon May 18 23:15:56 2009 +0200
@@ -12,6 +12,8 @@
thm even.equation
+ML_val {* Predicate.yieldn 10 @{code even_0} *}
+
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
append_Nil: "append [] xs xs"
@@ -22,6 +24,8 @@
thm append.equation
+ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}
+
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
for f where
--- a/src/HOL/ex/Quickcheck_Generators.thy Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy Mon May 18 23:15:56 2009 +0200
@@ -8,27 +8,11 @@
subsection {* Datatypes *}
-definition
- collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
"collapse f = (do g \<leftarrow> f; g done)"
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
- liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-end;
-*}
-
lemma random'_if:
- fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
+ fixes random' :: "index \<Rightarrow> index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
assumes "random' 0 j = (\<lambda>s. undefined)"
and "\<And>i. random' (Suc_index i) j = rhs2 i"
shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
@@ -36,15 +20,18 @@
setup {*
let
+ fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+ fun scomp T1 T2 sT f g = Const (@{const_name scomp},
+ liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
exception REC of string;
exception TYP of string;
fun mk_collapse thy ty = Sign.mk_const thy
- (@{const_name collapse}, [@{typ seed}, ty]);
+ (@{const_name collapse}, [@{typ Random.seed}, ty]);
fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
fun mk_split thy ty ty' = Sign.mk_const thy
- (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
+ (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT (term_ty ty') @{typ Random.seed}]);
fun mk_scomp_split thy ty ty' t t' =
- StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
+ scomp (term_ty ty) (term_ty ty') @{typ Random.seed} t
(mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
fun mk_cons thy this_ty (c, args) =
let
@@ -57,7 +44,7 @@
val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term
(list_comb (c, map (fn k => Bound (k + 1)) t_indices))
|> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
- val return = StateMonad.return (term_ty this_ty) @{typ seed}
+ val return = HOLogic.mk_return (term_ty this_ty) @{typ Random.seed}
(HOLogic.mk_prod (c_t, t_t));
val t = fold_rev (fn ((ty, _), random) =>
mk_scomp_split thy ty this_ty random)
@@ -67,21 +54,21 @@
fun mk_conss thy ty [] = NONE
| mk_conss thy ty [(_, t)] = SOME t
| mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
- (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
- HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
+ (Sign.mk_const thy (@{const_name Random.select}, [liftT (term_ty ty) @{typ Random.seed}]) $
+ HOLogic.mk_list (liftT (term_ty ty) @{typ Random.seed}) (map snd ts)));
fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) =
let
val SOME t_atom = mk_conss thy ty ts_atom;
in case mk_conss thy ty ts_rec
of SOME t_rec => mk_collapse thy (term_ty ty) $
- (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
+ (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $
@{term "i\<Colon>index"} $ t_rec $ t_atom)
| NONE => t_atom
end;
fun mk_random_eqs thy vs tycos =
let
val this_ty = Type (hd tycos, map TFree vs);
- val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
+ val this_ty' = liftT (term_ty this_ty) @{typ Random.seed};
val random_name = Long_Name.base_name @{const_name random};
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
@@ -100,8 +87,8 @@
|> (map o apsnd) (List.partition fst)
|> map (mk_clauses thy this_ty)
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
- (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
- Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
+ (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ Random.seed},
+ Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))),
(random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
]))) rhss;
in eqss end;
@@ -113,7 +100,7 @@
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
- random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
+ random' $ @{term "max (i\<Colon>index) 1"} $ @{term "i\<Colon>index"})
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
(fn thm => Context.mapping (Code.del_eqn thm) I));
fun add_code simps lthy =
@@ -146,32 +133,15 @@
end
| random_inst tycos thy = raise REC
("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
- fun add_random_inst tycos thy = random_inst tycos thy
- handle REC msg => (warning msg; thy)
- | TYP msg => (warning msg; thy)
+ fun add_random_inst [@{type_name bool}] thy = thy
+ | add_random_inst [@{type_name nat}] thy = thy
+ | add_random_inst tycos thy = random_inst tycos thy
+ handle REC msg => (warning msg; thy)
+ | TYP msg => (warning msg; thy)
in DatatypePackage.interpretation add_random_inst end
*}
-subsection {* Type @{typ int} *}
-
-instantiation int :: random
-begin
-
-definition
- "random n = (do
- (b, _) \<leftarrow> random n;
- (m, t) \<leftarrow> random n;
- return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
- else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
- (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
- done)"
-
-instance ..
-
-end
-
-
subsection {* Examples *}
theorem "map g (map f xs) = map (g o f) xs"
@@ -294,4 +264,8 @@
quickcheck [generator = code]
oops
+lemma "int (nat k) = k"
+ quickcheck [generator = code]
+ oops
+
end
--- a/src/HOL/ex/ROOT.ML Mon May 18 23:15:38 2009 +0200
+++ b/src/HOL/ex/ROOT.ML Mon May 18 23:15:56 2009 +0200
@@ -11,7 +11,6 @@
"Word",
"Eval_Examples",
"Quickcheck_Generators",
- "Term_Of_Syntax",
"Codegenerator",
"Codegenerator_Pretty",
"NormalForm",
--- a/src/HOL/ex/Term_Of_Syntax.thy Mon May 18 23:15:38 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/ex/Term_Of_Syntax.thy
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Input syntax for term_of functions *}
-
-theory Term_Of_Syntax
-imports Code_Eval
-begin
-
-setup {*
- Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
- #> snd
-*}
-
-notation (output)
- rterm_of ("\<guillemotleft>_\<guillemotright>")
-
-locale rterm_syntax =
- fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
-
-parse_translation {*
-let
- fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
- | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
-in
- [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
-end
-*}
-
-setup {*
-let
- val subst_rterm_of = map_aterms
- (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
- o HOLogic.reflect_term;
- fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
- | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
- error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
- | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
- fun subst_rterm_of'' t =
- let
- val t' = subst_rterm_of' (strip_comb t);
- in if t aconv t'
- then NONE
- else SOME t'
- end;
- fun check_rterm_of ts ctxt =
- let
- val ts' = map subst_rterm_of'' ts;
- in if exists is_some ts'
- then SOME (map2 the_default ts ts', ctxt)
- else NONE
- end;
-in
- Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
-end;
-*}
-
-end