--- a/NEWS Fri Dec 03 10:28:39 2010 +0100
+++ b/NEWS Fri Dec 03 10:43:09 2010 +0100
@@ -101,6 +101,14 @@
*** HOL ***
+* Quickcheck now by default uses exhaustive testing instead of random testing.
+Random testing can be invoked by quickcheck[random],
+exhaustive testing by quickcheck[exhaustive].
+
+* Quickcheck instantiates polymorphic types with small finite datatypes
+by default. This enables a simple execution mechanism to handle
+quantifiers and function equality over the finite datatypes.
+
* Functions can be declared as coercions and type inference will add them
as necessary upon input of a term. In Complex_Main, real :: nat => real
and real :: int => real are declared as coercions. A new coercion function
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Dec 03 10:43:09 2010 +0100
@@ -231,7 +231,7 @@
with wf less loc
have "approx_stk G hp [xcp] ST'"
by (auto simp add: sup_state_conv approx_stk_def approx_val_def
- elim: conf_widen split: Err.split)
+ elim: conf_widen split: err.split)
moreover
note len pc
ultimately
@@ -702,7 +702,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
apply (frule conf_widen)
prefer 2
apply assumption
--- a/src/HOL/Product_Type.thy Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Dec 03 10:43:09 2010 +0100
@@ -160,7 +160,7 @@
declare prod.simps(2) [nitpick_simp del]
-declare weak_case_cong [cong del]
+declare prod.weak_case_cong [cong del]
subsubsection {* Tuple syntax *}
@@ -440,7 +440,7 @@
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
- by (fact weak_case_cong)
+ by (fact prod.weak_case_cong)
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
by (simp add: split_eta)
@@ -578,7 +578,7 @@
\medskip @{term split} used as a logical connective or set former.
\medskip These rules are for use with @{text blast}; could instead
- call @{text simp} using @{thm [source] split} as rewrite. *}
+ call @{text simp} using @{thm [source] prod.split} as rewrite. *}
lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
apply (simp only: split_tupled_all)
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Dec 03 10:43:09 2010 +0100
@@ -275,7 +275,7 @@
proof (cases x, clarify)
fix a b
show "P (a, b)"
- proof (induct a arbitrary: b rule: Nat.induct)
+ proof (induct a arbitrary: b rule: nat.induct)
case zero
show "P (0, b)" using assms by (induct b) auto
next
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 03 10:43:09 2010 +0100
@@ -628,9 +628,9 @@
val ([dt_induct'], thy7) =
thy6
- |> Sign.add_path big_name
- |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
- ||> Sign.parent_path
+ |> Global_Theory.add_thms
+ [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+ [case_names_induct])]
||> Theory.checkpoint;
in
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 03 10:43:09 2010 +0100
@@ -98,18 +98,18 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thmss
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thms
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 03 10:43:09 2010 +0100
@@ -362,14 +362,14 @@
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val prfx = Binding.qualify true (space_implode "_" new_type_names);
val (((inject, distinct), [induct]), thy2) =
thy1
|> store_thmss "inject" new_type_names raw_inject
||>> store_thmss "distinct" new_type_names raw_distinct
- ||> Sign.add_path (space_implode "_" new_type_names)
||>> Global_Theory.add_thms
- [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
- ||> Sign.restore_naming thy1;
+ [((prfx (Binding.name "induct"), raw_induct),
+ [mk_case_names_induct descr])];
in
thy2
|> derive_datatype_props config dt_names alt_names [descr] sorts
--- a/src/HOL/ex/set.thy Fri Dec 03 10:28:39 2010 +0100
+++ b/src/HOL/ex/set.thy Fri Dec 03 10:43:09 2010 +0100
@@ -205,7 +205,7 @@
lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
-- {* Example 11: needs a hint. *}
-by(metis Nat.induct)
+by(metis nat.induct)
lemma
"(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
--- a/src/Pure/library.ML Fri Dec 03 10:28:39 2010 +0100
+++ b/src/Pure/library.ML Fri Dec 03 10:43:09 2010 +0100
@@ -727,7 +727,7 @@
(*simple quoting (does not escape special chars)*)
val quote = enclose "\"" "\"";
-(*space_implode "..." (space_explode "hello") = "h...e...l...l...o"*)
+(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
fun space_implode a bs = implode (separate a bs);
val commas = space_implode ", ";