--- a/NEWS Mon Nov 22 17:46:51 2010 +0100
+++ b/NEWS Mon Nov 22 17:49:12 2010 +0100
@@ -92,6 +92,9 @@
* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
avoid confusion with finite sets. INCOMPATIBILITY.
+* Quickcheck's generator for random generation is renamed from "code" to
+"random". INCOMPATIBILITY.
+
* Theory Multiset provides stable quicksort implementation of sort_key.
* Quickcheck now has a configurable time limit which is set to 30 seconds
--- a/src/HOL/Code_Evaluation.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy Mon Nov 22 17:49:12 2010 +0100
@@ -21,7 +21,10 @@
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
"App _ _ = dummy_term"
-code_datatype Const App
+definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
+ "Abs _ _ _ = dummy_term"
+
+code_datatype Const App Abs
class term_of = typerep +
fixes term_of :: "'a \<Rightarrow> term"
@@ -124,8 +127,8 @@
code_type "term"
(Eval "Term.term")
-code_const Const and App
- (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
+code_const Const and App and Abs
+ (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
code_const "term_of \<Colon> String.literal \<Rightarrow> term"
(Eval "HOLogic.mk'_literal")
@@ -184,7 +187,7 @@
(Eval "Code'_Evaluation.tracing")
-hide_const dummy_term App valapp
-hide_const (open) Const termify valtermify term_of term_of_num tracing
+hide_const dummy_term valapp
+hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Enum.thy Mon Nov 22 17:49:12 2010 +0100
@@ -0,0 +1,458 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Finite types as explicit enumerations *}
+
+theory Enum
+imports Map String
+begin
+
+subsection {* Class @{text enum} *}
+
+class enum =
+ fixes enum :: "'a list"
+ assumes UNIV_enum: "UNIV = set enum"
+ and enum_distinct: "distinct enum"
+begin
+
+subclass finite proof
+qed (simp add: UNIV_enum)
+
+lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
+
+lemma in_enum [intro]: "x \<in> set enum"
+ unfolding enum_all by auto
+
+lemma enum_eq_I:
+ assumes "\<And>x. x \<in> set xs"
+ shows "set enum = set xs"
+proof -
+ from assms UNIV_eq_I have "UNIV = set xs" by auto
+ with enum_all show ?thesis by simp
+qed
+
+end
+
+
+subsection {* Equality and order on functions *}
+
+instantiation "fun" :: (enum, equal) equal
+begin
+
+definition
+ "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
+
+instance proof
+qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
+
+end
+
+lemma [code nbe]:
+ "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
+ by (fact equal_refl)
+
+lemma [code]:
+ "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum"
+by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
+
+lemma order_fun [code]:
+ fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
+ shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
+ and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
+ by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
+
+
+subsection {* Quantifiers *}
+
+lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
+ by (simp add: list_all_iff enum_all)
+
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
+ by (simp add: list_ex_iff enum_all)
+
+lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
+unfolding list_ex1_iff enum_all by auto
+
+
+subsection {* Default instances *}
+
+primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+ "n_lists 0 xs = [[]]"
+ | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
+
+lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
+ by (induct n) simp_all
+
+lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
+ by (induct n) (auto simp add: length_concat o_def listsum_triv)
+
+lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+
+lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+proof (rule set_eqI)
+ fix ys :: "'a list"
+ show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+ proof -
+ have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+ moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
+ by (induct n arbitrary: ys) auto
+ moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
+ by (induct ys) auto
+ ultimately show ?thesis by auto
+ qed
+qed
+
+lemma distinct_n_lists:
+ assumes "distinct xs"
+ shows "distinct (n_lists n xs)"
+proof (rule card_distinct)
+ from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
+ have "card (set (n_lists n xs)) = card (set xs) ^ n"
+ proof (induct n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
+ = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
+ by (rule card_UN_disjoint) auto
+ moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
+ by (rule card_image) (simp add: inj_on_def)
+ ultimately show ?case by auto
+ qed
+ also have "\<dots> = length xs ^ n" by (simp add: card_length)
+ finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
+ by (simp add: length_n_lists)
+qed
+
+lemma map_of_zip_enum_is_Some:
+ assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
+ shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
+proof -
+ from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
+ (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
+ by (auto intro!: map_of_zip_is_Some)
+ then show ?thesis using enum_all by auto
+qed
+
+lemma map_of_zip_enum_inject:
+ fixes xs ys :: "'b\<Colon>enum list"
+ assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
+ "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
+ and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
+ shows "xs = ys"
+proof -
+ have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
+ proof
+ fix x :: 'a
+ from length map_of_zip_enum_is_Some obtain y1 y2
+ where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
+ and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
+ moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
+ by (auto dest: fun_cong)
+ ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
+ by simp
+ qed
+ with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
+qed
+
+instantiation "fun" :: (enum, enum) enum
+begin
+
+definition
+ "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+
+instance proof
+ show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
+ proof (rule UNIV_eq_I)
+ fix f :: "'a \<Rightarrow> 'b"
+ have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
+ by (auto simp add: map_of_zip_map fun_eq_iff)
+ then show "f \<in> set enum"
+ by (auto simp add: enum_fun_def set_n_lists)
+ qed
+next
+ from map_of_zip_enum_inject
+ show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
+ by (auto intro!: inj_onI simp add: enum_fun_def
+ distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
+qed
+
+end
+
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
+ in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
+ by (simp add: enum_fun_def Let_def)
+
+instantiation unit :: enum
+begin
+
+definition
+ "enum = [()]"
+
+instance proof
+qed (simp_all add: enum_unit_def UNIV_unit)
+
+end
+
+instantiation bool :: enum
+begin
+
+definition
+ "enum = [False, True]"
+
+instance proof
+qed (simp_all add: enum_bool_def UNIV_bool)
+
+end
+
+primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+ "product [] _ = []"
+ | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+
+lemma product_list_set:
+ "set (product xs ys) = set xs \<times> set ys"
+ by (induct xs) auto
+
+lemma distinct_product:
+ assumes "distinct xs" and "distinct ys"
+ shows "distinct (product xs ys)"
+ using assms by (induct xs)
+ (auto intro: inj_onI simp add: product_list_set distinct_map)
+
+instantiation prod :: (enum, enum) enum
+begin
+
+definition
+ "enum = product enum enum"
+
+instance by default
+ (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
+
+end
+
+instantiation sum :: (enum, enum) enum
+begin
+
+definition
+ "enum = map Inl enum @ map Inr enum"
+
+instance by default
+ (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
+
+end
+
+primrec sublists :: "'a list \<Rightarrow> 'a list list" where
+ "sublists [] = [[]]"
+ | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+
+lemma length_sublists:
+ "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
+ by (induct xs) (simp_all add: Let_def)
+
+lemma sublists_powset:
+ "set ` set (sublists xs) = Pow (set xs)"
+proof -
+ have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
+ by (auto simp add: image_def)
+ have "set (map set (sublists xs)) = Pow (set xs)"
+ by (induct xs)
+ (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
+ then show ?thesis by simp
+qed
+
+lemma distinct_set_sublists:
+ assumes "distinct xs"
+ shows "distinct (map set (sublists xs))"
+proof (rule card_distinct)
+ have "finite (set xs)" by rule
+ then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
+ with assms distinct_card [of xs]
+ have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
+ then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
+ by (simp add: sublists_powset length_sublists)
+qed
+
+instantiation nibble :: enum
+begin
+
+definition
+ "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
+ Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
+
+instance proof
+qed (simp_all add: enum_nibble_def UNIV_nibble)
+
+end
+
+instantiation char :: enum
+begin
+
+definition
+ "enum = map (split Char) (product enum enum)"
+
+lemma enum_chars [code]:
+ "enum = chars"
+ unfolding enum_char_def chars_def enum_nibble_def by simp
+
+instance proof
+qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
+ distinct_map distinct_product enum_distinct)
+
+end
+
+instantiation option :: (enum) enum
+begin
+
+definition
+ "enum = None # map Some enum"
+
+instance proof
+qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
+
+end
+
+subsection {* Small finite types *}
+
+text {* We define small finite types for the use in Quickcheck *}
+
+datatype finite_1 = a\<^isub>1
+
+instantiation finite_1 :: enum
+begin
+
+definition
+ "enum = [a\<^isub>1]"
+
+instance proof
+qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
+
+end
+
+instantiation finite_1 :: linorder
+begin
+
+definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
+where
+ "less_eq_finite_1 x y = True"
+
+definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
+where
+ "less_finite_1 x y = False"
+
+instance
+apply (intro_classes)
+apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
+apply (metis finite_1.exhaust)
+done
+
+end
+
+hide_const a\<^isub>1
+
+datatype finite_2 = a\<^isub>1 | a\<^isub>2
+
+instantiation finite_2 :: enum
+begin
+
+definition
+ "enum = [a\<^isub>1, a\<^isub>2]"
+
+instance proof
+qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
+
+end
+
+instantiation finite_2 :: linorder
+begin
+
+definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
+where
+ "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
+
+definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
+where
+ "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
+
+
+instance
+apply (intro_classes)
+apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
+apply (metis finite_2.distinct finite_2.nchotomy)+
+done
+
+end
+
+hide_const a\<^isub>1 a\<^isub>2
+
+
+datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
+
+instantiation finite_3 :: enum
+begin
+
+definition
+ "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
+
+instance proof
+qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
+
+end
+
+instantiation finite_3 :: linorder
+begin
+
+definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
+where
+ "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
+ | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
+
+definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
+where
+ "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
+
+
+instance proof (intro_classes)
+qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
+
+end
+
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
+
+
+datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
+
+instantiation finite_4 :: enum
+begin
+
+definition
+ "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
+
+instance proof
+qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
+
+end
+
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
+
+
+datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
+
+instantiation finite_5 :: enum
+begin
+
+definition
+ "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
+
+instance proof
+qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
+
+end
+
+hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
+
+
+hide_type finite_1 finite_2 finite_3 finite_4 finite_5
+hide_const (open) enum n_lists product
+
+end
--- a/src/HOL/IsaMakefile Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 22 17:49:12 2010 +0100
@@ -246,6 +246,7 @@
Divides.thy \
DSequence.thy \
Equiv_Relations.thy \
+ Enum.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
Int.thy \
@@ -416,7 +417,7 @@
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
- Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
+ Library/Efficient_Nat.thy Library/Eval_Witness.thy \
Library/Executable_Set.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
@@ -1016,7 +1017,8 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
- ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy \
+ ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \
+ ex/Chinese.thy \
ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy \
ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
@@ -1294,7 +1296,8 @@
Mirabelle/Tools/mirabelle_metis.ML \
Mirabelle/Tools/mirabelle_quickcheck.ML \
Mirabelle/Tools/mirabelle_refute.ML \
- Mirabelle/Tools/mirabelle_sledgehammer.ML
+ Mirabelle/Tools/mirabelle_sledgehammer.ML \
+ Mirabelle/Tools/sledgehammer_tactic.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Library/Enum.thy Mon Nov 22 17:46:51 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,308 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Finite types as explicit enumerations *}
-
-theory Enum
-imports Map Main
-begin
-
-subsection {* Class @{text enum} *}
-
-class enum =
- fixes enum :: "'a list"
- assumes UNIV_enum: "UNIV = set enum"
- and enum_distinct: "distinct enum"
-begin
-
-subclass finite proof
-qed (simp add: UNIV_enum)
-
-lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
-
-lemma in_enum [intro]: "x \<in> set enum"
- unfolding enum_all by auto
-
-lemma enum_eq_I:
- assumes "\<And>x. x \<in> set xs"
- shows "set enum = set xs"
-proof -
- from assms UNIV_eq_I have "UNIV = set xs" by auto
- with enum_all show ?thesis by simp
-qed
-
-end
-
-
-subsection {* Equality and order on functions *}
-
-instantiation "fun" :: (enum, equal) equal
-begin
-
-definition
- "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
-
-instance proof
-qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
-
-end
-
-lemma [code nbe]:
- "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
- by (fact equal_refl)
-
-lemma order_fun [code]:
- fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
- shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
- and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
- by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
-
-
-subsection {* Quantifiers *}
-
-lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
- by (simp add: list_all_iff enum_all)
-
-lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
- by (simp add: list_ex_iff enum_all)
-
-
-subsection {* Default instances *}
-
-primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
- "n_lists 0 xs = [[]]"
- | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
-
-lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
- by (induct n) simp_all
-
-lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
- by (induct n) (auto simp add: length_concat o_def listsum_triv)
-
-lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
-
-lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
-proof (rule set_eqI)
- fix ys :: "'a list"
- show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
- proof -
- have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
- moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
- by (induct n arbitrary: ys) auto
- moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
- by (induct ys) auto
- ultimately show ?thesis by auto
- qed
-qed
-
-lemma distinct_n_lists:
- assumes "distinct xs"
- shows "distinct (n_lists n xs)"
-proof (rule card_distinct)
- from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
- have "card (set (n_lists n xs)) = card (set xs) ^ n"
- proof (induct n)
- case 0 then show ?case by simp
- next
- case (Suc n)
- moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
- = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
- by (rule card_UN_disjoint) auto
- moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
- by (rule card_image) (simp add: inj_on_def)
- ultimately show ?case by auto
- qed
- also have "\<dots> = length xs ^ n" by (simp add: card_length)
- finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
- by (simp add: length_n_lists)
-qed
-
-lemma map_of_zip_enum_is_Some:
- assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
- shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
-proof -
- from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
- (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
- by (auto intro!: map_of_zip_is_Some)
- then show ?thesis using enum_all by auto
-qed
-
-lemma map_of_zip_enum_inject:
- fixes xs ys :: "'b\<Colon>enum list"
- assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
- "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
- and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
- shows "xs = ys"
-proof -
- have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
- proof
- fix x :: 'a
- from length map_of_zip_enum_is_Some obtain y1 y2
- where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
- and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
- moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
- by (auto dest: fun_cong)
- ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
- by simp
- qed
- with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
-qed
-
-instantiation "fun" :: (enum, enum) enum
-begin
-
-definition
- "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
-
-instance proof
- show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
- proof (rule UNIV_eq_I)
- fix f :: "'a \<Rightarrow> 'b"
- have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
- by (auto simp add: map_of_zip_map fun_eq_iff)
- then show "f \<in> set enum"
- by (auto simp add: enum_fun_def set_n_lists)
- qed
-next
- from map_of_zip_enum_inject
- show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
- by (auto intro!: inj_onI simp add: enum_fun_def
- distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
-qed
-
-end
-
-lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
- in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
- by (simp add: enum_fun_def Let_def)
-
-instantiation unit :: enum
-begin
-
-definition
- "enum = [()]"
-
-instance proof
-qed (simp_all add: enum_unit_def UNIV_unit)
-
-end
-
-instantiation bool :: enum
-begin
-
-definition
- "enum = [False, True]"
-
-instance proof
-qed (simp_all add: enum_bool_def UNIV_bool)
-
-end
-
-primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
- "product [] _ = []"
- | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
-
-lemma product_list_set:
- "set (product xs ys) = set xs \<times> set ys"
- by (induct xs) auto
-
-lemma distinct_product:
- assumes "distinct xs" and "distinct ys"
- shows "distinct (product xs ys)"
- using assms by (induct xs)
- (auto intro: inj_onI simp add: product_list_set distinct_map)
-
-instantiation prod :: (enum, enum) enum
-begin
-
-definition
- "enum = product enum enum"
-
-instance by default
- (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
-
-end
-
-instantiation sum :: (enum, enum) enum
-begin
-
-definition
- "enum = map Inl enum @ map Inr enum"
-
-instance by default
- (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
-
-end
-
-primrec sublists :: "'a list \<Rightarrow> 'a list list" where
- "sublists [] = [[]]"
- | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
-lemma length_sublists:
- "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
- by (induct xs) (simp_all add: Let_def)
-
-lemma sublists_powset:
- "set ` set (sublists xs) = Pow (set xs)"
-proof -
- have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
- by (auto simp add: image_def)
- have "set (map set (sublists xs)) = Pow (set xs)"
- by (induct xs)
- (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
- then show ?thesis by simp
-qed
-
-lemma distinct_set_sublists:
- assumes "distinct xs"
- shows "distinct (map set (sublists xs))"
-proof (rule card_distinct)
- have "finite (set xs)" by rule
- then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
- with assms distinct_card [of xs]
- have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
- then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
- by (simp add: sublists_powset length_sublists)
-qed
-
-instantiation nibble :: enum
-begin
-
-definition
- "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
- Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
-
-instance proof
-qed (simp_all add: enum_nibble_def UNIV_nibble)
-
-end
-
-instantiation char :: enum
-begin
-
-definition
- "enum = map (split Char) (product enum enum)"
-
-lemma enum_chars [code]:
- "enum = chars"
- unfolding enum_char_def chars_def enum_nibble_def by simp
-
-instance proof
-qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
- distinct_map distinct_product enum_distinct)
-
-end
-
-instantiation option :: (enum) enum
-begin
-
-definition
- "enum = None # map Some enum"
-
-instance proof
-qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
-
-end
-
-end
--- a/src/HOL/Library/FuncSet.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Library/FuncSet.thy Mon Nov 22 17:49:12 2010 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Library/FuncSet.thy
- Author: Florian Kammueller and Lawrence C Paulson
+ Author: Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
*)
header {* Pi and Function Sets *}
@@ -251,4 +251,158 @@
g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
by (blast intro: card_inj order_antisym)
+subsection {* Extensional Function Spaces *}
+
+definition extensional_funcset
+where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
+
+lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
+unfolding extensional_def by (auto intro: ext)
+
+lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
+unfolding extensional_funcset_def by simp
+
+lemma extensional_funcset_empty_range:
+ assumes "S \<noteq> {}"
+ shows "extensional_funcset S {} = {}"
+using assms unfolding extensional_funcset_def by auto
+
+lemma extensional_funcset_arb:
+ assumes "f \<in> extensional_funcset S T" "x \<notin> S"
+ shows "f x = undefined"
+using assms
+unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
+
+lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
+unfolding extensional_funcset_def by auto
+
+lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
+unfolding extensional_def by auto
+
+lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T"
+unfolding extensional_funcset_def extensional_def by auto
+
+lemma extensional_funcset_restrict_domain:
+ "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
+unfolding extensional_funcset_def extensional_def by auto
+
+lemma extensional_funcset_extend_domain_eq:
+ assumes "x \<notin> S"
+ shows
+ "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
+ using assms
+proof -
+ {
+ fix f
+ assume "f : extensional_funcset (insert x S) T"
+ from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
+ unfolding image_iff
+ apply (rule_tac x="(f x, f(x := undefined))" in bexI)
+ apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done
+ }
+ moreover
+ {
+ fix f
+ assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
+ from this assms have "f : extensional_funcset (insert x S) T"
+ by (auto intro: extensional_funcset_extend_domainI)
+ }
+ ultimately show ?thesis by auto
+qed
+
+lemma extensional_funcset_fun_upd_restricts_rangeI: "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T - {f x})"
+unfolding extensional_funcset_def extensional_def
+apply auto
+apply (case_tac "x = xa")
+apply auto done
+
+lemma extensional_funcset_fun_upd_extends_rangeI:
+ assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
+ shows "f(x := a) : extensional_funcset (insert x S) T"
+ using assms unfolding extensional_funcset_def extensional_def by auto
+
+subsubsection {* Injective Extensional Function Spaces *}
+
+lemma extensional_funcset_fun_upd_inj_onI:
+ assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
+ shows "inj_on (f(x := a)) S"
+ using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
+
+lemma extensional_funcset_extend_domain_inj_on_eq:
+ assumes "x \<notin> S"
+ shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
+ (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+proof -
+ from assms show ?thesis
+ apply auto
+ apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
+ apply (auto simp add: image_iff inj_on_def)
+ apply (rule_tac x="xa x" in exI)
+ apply (auto intro: extensional_funcset_mem)
+ apply (rule_tac x="xa(x := undefined)" in exI)
+ apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
+ apply (auto dest!: extensional_funcset_mem split: split_if_asm)
+ done
+qed
+
+lemma extensional_funcset_extend_domain_inj_onI:
+ assumes "x \<notin> S"
+ shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
+proof -
+ from assms show ?thesis
+ apply (auto intro!: inj_onI)
+ apply (metis fun_upd_same)
+ by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
+qed
+
+
+subsubsection {* Cardinality *}
+
+lemma card_extensional_funcset:
+ assumes "finite S"
+ shows "card (extensional_funcset S T) = (card T) ^ (card S)"
+using assms
+proof (induct rule: finite_induct)
+ case empty
+ show ?case
+ by (auto simp add: extensional_funcset_empty_domain)
+next
+ case (insert x S)
+ {
+ fix g g' y y'
+ assume assms: "g \<in> extensional_funcset S T"
+ "g' \<in> extensional_funcset S T"
+ "y \<in> T" "y' \<in> T"
+ "g(x := y) = g'(x := y')"
+ from this have "y = y'"
+ by (metis fun_upd_same)
+ have "g = g'"
+ by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
+ from `y = y'` `g = g'` have "y = y' & g = g'" by simp
+ }
+ from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
+ by (auto intro: inj_onI)
+ from this insert.hyps show ?case
+ by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
+qed
+
+lemma finite_extensional_funcset:
+ assumes "finite S" "finite T"
+ shows "finite (extensional_funcset S T)"
+proof -
+ from card_extensional_funcset[OF assms(1), of T] assms(2)
+ have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
+ by auto
+ from this show ?thesis
+ proof
+ assume "card (extensional_funcset S T) \<noteq> 0"
+ from this show ?thesis
+ by (auto intro: card_ge_0_finite)
+ next
+ assume "S \<noteq> {} \<and> T = {}"
+ from this show ?thesis
+ by (auto simp add: extensional_funcset_empty_range)
+ qed
+qed
+
end
--- a/src/HOL/Library/Library.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Library/Library.thy Mon Nov 22 17:49:12 2010 +0100
@@ -14,7 +14,6 @@
Countable
Diagonalize
Dlist
- Enum
Eval_Witness
Float
Formal_Power_Series
--- a/src/HOL/Library/Quickcheck_Types.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Library/Quickcheck_Types.thy Mon Nov 22 17:49:12 2010 +0100
@@ -460,7 +460,7 @@
section {* Quickcheck configuration *}
-quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
+quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
hide_type non_distrib_lattice flat_complete_lattice bot top
--- a/src/HOL/List.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/List.thy Mon Nov 22 17:49:12 2010 +0100
@@ -4877,6 +4877,10 @@
definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
+definition list_ex1
+where
+ list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
+
text {*
Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
over @{const list_all} and @{const list_ex} in specifications.
@@ -4892,6 +4896,11 @@
"list_ex P [] \<longleftrightarrow> False"
by (simp_all add: list_ex_iff)
+lemma list_ex1_simps [simp, code]:
+ "list_ex1 P [] = False"
+ "list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)"
+unfolding list_ex1_iff list_all_iff by auto
+
lemma Ball_set_list_all [code_unfold]:
"Ball (set xs) P \<longleftrightarrow> list_all P xs"
by (simp add: list_all_iff)
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Nov 22 17:49:12 2010 +0100
@@ -13,6 +13,7 @@
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
"Tools/mirabelle_sledgehammer_filter.ML"
+ "Tools/sledgehammer_tactic.ML"
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Mon Nov 22 17:49:12 2010 +0100
@@ -0,0 +1,87 @@
+(* Title: sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+fun run_atp force_full_types timeout i n ctxt goal name =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val params as {full_types, ...} =
+ ((if force_full_types then [("full_types", "true")] else [])
+ @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
+(* @ [("overlord", "true")] *)
+ |> Sledgehammer_Isar.default_params ctxt
+ val prover = Sledgehammer.get_prover thy false name
+ val facts = []
+ (* Check for constants other than the built-in HOL constants. If none of
+ them appear (as should be the case for TPTP problems, unless "auto" or
+ "simp" already did its "magic"), we can skip the relevance filter. *)
+ val pure_goal =
+ not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
+ not (String.isSubstring "HOL" s))
+ (prop_of goal))
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, facts = [],
+ only = true, subgoal_count = n}
+ in
+ prover params (K "") problem |> #message
+ handle ERROR message => "Error: " ^ message ^ "\n"
+ end
+
+fun to_period ("." :: _) = []
+ | to_period ("" :: ss) = to_period ss
+ | to_period (s :: ss) = s :: to_period ss
+ | to_period [] = []
+
+val extract_metis_facts =
+ space_explode " "
+ #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
+ #> fst o chop_while (not o member (op =) ["metis", "metisFT"])
+ #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
+
+val atp = "e" (* or "vampire" *)
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun sledgehammer_with_metis_tac ctxt i th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
+ val s = run_atp false timeout i i ctxt th atp
+ val xs = these (extract_metis_facts s)
+ val ths = maps (thms_of_name ctxt) xs
+ in Metis_Tactics.metis_tac ctxt ths i th end
+
+fun sledgehammer_as_oracle_tac ctxt i th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
+ val s = run_atp true timeout i i ctxt th atp
+ in
+ if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
+ else Seq.empty
+ end
+
+end;
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Mon Nov 22 17:49:12 2010 +0100
@@ -1,58 +1,144 @@
theory MutabelleExtra
-imports Complex_Main SML_Quickcheck
-(*
- "~/Downloads/Jinja/J/TypeSafe"
- "~/Downloads/Jinja/J/Annotate"
- (* FIXME "Example" *)
- "~/Downloads/Jinja/J/execute_Bigstep"
- "~/Downloads/Jinja/J/execute_WellType"
- "~/Downloads/Jinja/JVM/JVMDefensive"
- "~/Downloads/Jinja/JVM/JVMListExample"
- "~/Downloads/Jinja/BV/BVExec"
- "~/Downloads/Jinja/BV/LBVJVM"
- "~/Downloads/Jinja/BV/BVNoTypeError"
- "~/Downloads/Jinja/BV/BVExample"
- "~/Downloads/Jinja/Compiler/TypeComp"
-*)
-(*"~/Downloads/NormByEval/NBE"*)
-uses "mutabelle.ML"
+imports Complex_Main
+(* "~/repos/afp/thys/AVL-Trees/AVL"
+ "~/repos/afp/thys/BinarySearchTree/BinaryTree"
+ "~/repos/afp/thys/Huffman/Huffman"
+ "~/repos/afp/thys/List-Index/List_Index"
+ "~/repos/afp/thys/Matrix/Matrix"
+ "~/repos/afp/thys/NormByEval/NBE"
+ "~/repos/afp/thys/Polynomials/Polynomial"
+ "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
+ "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
+uses
+ "mutabelle.ML"
"mutabelle_extra.ML"
begin
-(* FIXME !?!?! *)
-ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
-ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
-ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
-ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
+
+section {* configuration *}
-quickcheck_params [size = 5, iterations = 1000]
+ML {* val log_directory = "" *}
+
+
+quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
+
(*
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
ML {* Auto_Tools.time_limit := 10 *}
+ML {* val mtds = [
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
+ MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
+]
+*}
+
+ML {*
+fun mutation_testing_of (name, thy) =
+ (MutabelleExtra.random_seed := 1.0;
+ MutabelleExtra.thms_of false thy
+ |> MutabelleExtra.take_random 200
+ |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
+ @{theory} mtds thms (log_directory ^ "/" ^ name)))
+*}
+
text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
+(*
ML {*
-(*
+
MutabelleExtra.random_seed := 1.0;
MutabelleExtra.thms_of true @{theory Complex_Main}
|> MutabelleExtra.take_random 1000000
|> (fn thms => List.drop (thms, 1000))
|> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
- @{theory} [MutabelleExtra.quickcheck_mtd "SML",
- MutabelleExtra.quickcheck_mtd "code"
+ @{theory} [
+ MutabelleExtra.quickcheck_mtd "code",
+ MutabelleExtra.smallcheck_mtd
(*MutabelleExtra.refute_mtd,
MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
+
+ *}
*)
+
+section {* Mutation testing Isabelle theories *}
+
+subsection {* List theory *}
+
+(*
+ML {*
+mutation_testing_of ("List", @{theory List})
*}
+*)
+
+section {* Mutation testing AFP theories *}
+
+subsection {* AVL-Trees *}
+
+(*
+ML {*
+mutation_testing_of ("AVL-Trees", @{theory AVL})
+ *}
+*)
+
+subsection {* BinaryTree *}
+
+(*
+ML {*
+mutation_testing_of ("BinaryTree", @{theory BinaryTree})
+ *}
+*)
+
+subsection {* Huffman *}
+
+(*
+ML {*
+mutation_testing_of ("Huffman", @{theory Huffman})
+ *}
+*)
-(* FIXME !?!?! *)
-ML {* Output.Private_Hooks.tracing_fn := old_tr *}
-ML {* Output.Private_Hooks.writeln_fn := old_wr *}
-ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
-ML {* Output.Private_Hooks.warning_fn := old_wa *}
+subsection {* List_Index *}
+
+(*
+ML {*
+mutation_testing_of ("List_Index", @{theory List_Index})
+ *}
+*)
+
+subsection {* Matrix *}
+
+(*
+ML {*
+mutation_testing_of ("Matrix", @{theory Matrix})
+ *}
+*)
+
+subsection {* NBE *}
+
+(*
+ML {*
+mutation_testing_of ("NBE", @{theory NBE})
+ *}
+*)
+
+subsection {* Polynomial *}
+
+(*
+ML {*
+mutation_testing_of ("Polynomial", @{theory Polynomial})
+ *}
+*)
+
+subsection {* Presburger Automata *}
+
+(*
+ML {*
+mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
+ *}
+*)
end
--- a/src/HOL/Mutabelle/mutabelle.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Mon Nov 22 17:49:12 2010 +0100
@@ -498,7 +498,7 @@
fun is_executable thy insts th =
((Quickcheck.test_term
- (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 1)))) (ProofContext.init_global thy))
+ ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
(SOME (!testgen_name)) (preprocess thy insts (prop_of th));
Output.urgent_message "executable"; true) handle ERROR s =>
(Output.urgent_message ("not executable: " ^ s); false));
@@ -507,7 +507,7 @@
| qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter
(Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
((x, pretty (the_default [] (fst (Quickcheck.test_term
- (Context.proof_map (Quickcheck.map_test_params (apfst (K (sz, qciter))))
+ ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
(ProofContext.init_global usedthy))
(SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Nov 22 17:49:12 2010 +0100
@@ -8,7 +8,7 @@
val take_random : int -> 'a list -> 'a list
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
type timing = (string * int) list
type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -20,7 +20,10 @@
type entry = string * bool * subentry list
type report = entry list
-val quickcheck_mtd : string -> mtd
+val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
+
+val solve_direct_mtd : mtd
+val try_mtd : mtd
(*
val refute_mtd : mtd
val nitpick_mtd : mtd
@@ -45,15 +48,17 @@
(* mutation options *)
-val max_mutants = 4
-val num_mutations = 1
+(*val max_mutants = 4
+val num_mutations = 1*)
(* soundness check: *)
-(*val max_mutants = 1
-val num_mutations = 0*)
+val max_mutants = 10
+val num_mutations = 1
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
+(* Another Random engine *)
+
exception RANDOM;
fun rmod x y = x - y * Real.realFloor (x / y);
@@ -73,7 +78,26 @@
if h < l orelse l < 0 then raise RANDOM
else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+fun take_random 0 _ = []
+ | take_random _ [] = []
+ | take_random n xs =
+ let val j = random_range 0 (length xs - 1) in
+ Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
+ end
+
+(* possible outcomes *)
+
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
+
+fun string_of_outcome GenuineCex = "GenuineCex"
+ | string_of_outcome PotentialCex = "PotentialCex"
+ | string_of_outcome NoCex = "NoCex"
+ | string_of_outcome Donno = "Donno"
+ | string_of_outcome Timeout = "Timeout"
+ | string_of_outcome Error = "Error"
+ | string_of_outcome Solved = "Solved"
+ | string_of_outcome Unsolved = "Unsolved"
+
type timing = (string * int) list
type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -85,25 +109,49 @@
type entry = string * bool * subentry list
type report = entry list
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
- | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
+(* possible invocations *)
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (Mutabelle.freeze t));
+(** quickcheck **)
-fun invoke_quickcheck quickcheck_generator thy t =
+fun invoke_quickcheck change_options quickcheck_generator thy t =
TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
(fn _ =>
- case Quickcheck.test_term (ProofContext.init_global thy)
- (SOME quickcheck_generator) (preprocess thy [] t) of
- (NONE, (time_report, report)) => (NoCex, (time_report, report))
- | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
+ case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
+ (SOME quickcheck_generator, []) [t] of
+ (NONE, _) => (NoCex, ([], NONE))
+ | (SOME _, _) => (GenuineCex, ([], NONE))) ()
handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
-fun quickcheck_mtd quickcheck_generator =
- ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
+fun quickcheck_mtd change_options quickcheck_generator =
+ ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
+
+(** solve direct **)
+
+fun invoke_solve_direct thy t =
+ let
+ val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
+ in
+ case Solve_Direct.solve_direct false state of
+ (true, _) => (Solved, ([], NONE))
+ | (false, _) => (Unsolved, ([], NONE))
+ end
- (*
+val solve_direct_mtd = ("solve_direct", invoke_solve_direct)
+
+(** try **)
+
+fun invoke_try thy t =
+ let
+ val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
+ in
+ case Try.invoke_try NONE state of
+ true => (Solved, ([], NONE))
+ | false => (Unsolved, ([], NONE))
+ end
+
+val try_mtd = ("try", invoke_try)
+
+(*
fun invoke_refute thy t =
let
val res = MyRefute.refute_term thy [] t
@@ -185,6 +233,8 @@
val nitpick_mtd = ("nitpick", invoke_nitpick)
*)
+(* filtering forbidden theorems and mutants *)
+
val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
val forbidden =
@@ -200,7 +250,6 @@
(@{const_name "top_fun_inst.top_fun"}, "'a"),
(@{const_name "Pure.term"}, "'a"),
(@{const_name "top_class.top"}, "'a"),
- (@{const_name "HOL.equal"}, "'a"),
(@{const_name "Quotient.Quot_True"}, "'a")(*,
(@{const_name "uminus"}, "'a"),
(@{const_name "Nat.size"}, "'a"),
@@ -211,7 +260,7 @@
"nibble"]
val forbidden_consts =
- [@{const_name nibble_pair_of_char}]
+ [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
fun is_forbidden_theorem (s, th) =
let val consts = Term.add_const_names (prop_of th) [] in
@@ -220,7 +269,8 @@
length (space_explode "." s) <> 2 orelse
String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
String.isSuffix "_def" s orelse
- String.isSuffix "_raw" s
+ String.isSuffix "_raw" s orelse
+ String.isPrefix "term_of" (List.last (space_explode "." s))
end
val forbidden_mutant_constnames =
@@ -235,23 +285,54 @@
@{const_name "top_fun_inst.top_fun"},
@{const_name "Pure.term"},
@{const_name "top_class.top"},
- @{const_name "HOL.equal"},
- @{const_name "Quotient.Quot_True"}]
+ (*@{const_name "HOL.equal"},*)
+ @{const_name "Quotient.Quot_True"}
+ (*@{const_name "==>"}, @{const_name "=="}*)]
+
+val forbidden_mutant_consts =
+ [
+ (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
+ (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
+ (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
+ (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
+ (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
+ (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
fun is_forbidden_mutant t =
let
- val consts = Term.add_const_names t []
+ val const_names = Term.add_const_names t []
+ val consts = Term.add_consts t []
in
- exists (String.isPrefix "Nitpick") consts orelse
- exists (String.isSubstring "_sumC") consts orelse
- exists (member (op =) forbidden_mutant_constnames) consts
+ exists (String.isPrefix "Nitpick") const_names orelse
+ exists (String.isSubstring "_sumC") const_names orelse
+ exists (member (op =) forbidden_mutant_constnames) const_names orelse
+ exists (member (op =) forbidden_mutant_consts) consts
end
+(* executable via quickcheck *)
+
fun is_executable_term thy t =
- can (TimeLimit.timeLimit (seconds 2.0)
- (Quickcheck.test_term
- (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
- (SOME "SML"))) (preprocess thy [] t)
+ let
+ val ctxt = ProofContext.init_global thy
+ in
+ can (TimeLimit.timeLimit (seconds 2.0)
+ (Quickcheck.test_goal_terms
+ ((Config.put Quickcheck.finite_types true #>
+ Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
+ (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+ end
fun is_executable_thm thy th = is_executable_term thy (prop_of th)
@@ -267,44 +348,47 @@
val count = length oo filter o equal
-fun take_random 0 _ = []
- | take_random _ [] = []
- | take_random n xs =
- let val j = random_range 0 (length xs - 1) in
- Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
- end
-
fun cpu_time description f =
let
val start = start_timing ()
val result = Exn.capture f ()
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-
+(*
+fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
+ let
+ val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+ val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
+ handle ERROR s => (tracing s; (Error, ([], NONE))))
+ val _ = Output.urgent_message (" Done")
+ in (res, (time :: timing, reports)) end
+*)
fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
let
val _ = Output.urgent_message ("Invoking " ^ mtd_name)
- val ((res, (timing, reports)), time) = cpu_time "total time"
- (fn () => case try (invoke_mtd thy) t of
+ val (res, (timing, reports)) = (*cpu_time "total time"
+ (fn () => *)case try (invoke_mtd thy) t of
SOME (res, (timing, reports)) => (res, (timing, reports))
| NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
- (Error , ([], NONE))))
+ (Error, ([], NONE)))
val _ = Output.urgent_message (" Done")
- in (res, (time :: timing, reports)) end
+ in (res, (timing, reports)) end
(* theory -> term list -> mtd -> subentry *)
-(*
+
fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
let
- val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
+ val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
in
(mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
count Donno res, count Timeout res, count Error res)
end
+(* creating entries *)
+
fun create_entry thy thm exec mutants mtds =
(Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-*)
+
fun create_detailed_entry thy thm exec mutants mtds =
let
fun create_mutant_subentry mutant = (mutant,
@@ -318,13 +402,14 @@
fun mutate_theorem create_entry thy mtds thm =
let
val exec = is_executable_thm thy thm
- val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
+ val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
val mutants =
(if num_mutations = 0 then
[Thm.prop_of thm]
else
Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
num_mutations)
+ |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
|> filter_out is_forbidden_mutant
val mutants =
if exec then
@@ -344,6 +429,7 @@
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
|> List.mapPartial (try (Sign.cert_term thy))
+ |> List.filter (is_some o try (cterm_of thy))
val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
in
create_entry thy thm exec mutants mtds
@@ -352,13 +438,6 @@
(* theory -> mtd list -> thm list -> report *)
val mutate_theorems = map ooo mutate_theorem
-fun string_of_outcome GenuineCex = "GenuineCex"
- | string_of_outcome PotentialCex = "PotentialCex"
- | string_of_outcome NoCex = "NoCex"
- | string_of_outcome Donno = "Donno"
- | string_of_outcome Timeout = "Timeout"
- | string_of_outcome Error = "Error"
-
fun string_of_mutant_subentry thy thm_name (t, results) =
"mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
space_implode "; "
@@ -378,12 +457,12 @@
cat_lines (map (fn (size, [report]) =>
"size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
- mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
- space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
+ mtd_name ^ ": " ^ string_of_outcome outcome
+ (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
(*^ "\n" ^ string_of_reports reports*)
in
"mutant of " ^ thm_name ^ ":\n"
- ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
+ ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
@@ -394,8 +473,7 @@
fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
"lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
"\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
- "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
- "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
+ "\" \nquickcheck\noops\n"
fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
"subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
@@ -409,10 +487,12 @@
Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
Int.toString error ^ "!"
+
(* entry -> string *)
fun string_for_entry (thm_name, exec, subentries) =
thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
cat_lines (map string_for_subentry subentries) ^ "\n"
+
(* report -> string *)
fun string_for_report report = cat_lines (map string_for_entry report)
@@ -424,15 +504,16 @@
fun mutate_theorems_and_write_report thy mtds thms file_name =
let
val _ = Output.urgent_message "Starting Mutabelle..."
- val Quickcheck.Test_Params test_params = Quickcheck.test_params_of (ProofContext.init_global thy)
+ val ctxt = ProofContext.init_global thy
val path = Path.explode file_name
(* for normal report: *)
- (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
- (*for detailled report: *)
- val (gen_create_entry, gen_string_for_entry) =
- (create_detailed_entry, string_of_detailed_entry thy)
- val (gen_create_entry, gen_string_for_entry) =
- (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
+ (*
+ val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
+ *)
+ (* for detailled report: *)
+ val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
+ (* for theory creation: *)
+ (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
in
File.write path (
"Mutation options = " ^
@@ -440,8 +521,8 @@
"; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
"QC options = " ^
(*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
- "size: " ^ string_of_int (#size test_params) ^
- "; iterations: " ^ string_of_int (#iterations test_params) ^ "\n");
+ "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
+ "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n");
map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
()
end
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Nov 22 17:49:12 2010 +0100
@@ -50,8 +50,8 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
-quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
+quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
+quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
oops
--- a/src/HOL/Quickcheck.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Quickcheck.thy Mon Nov 22 17:49:12 2010 +0100
@@ -3,7 +3,7 @@
header {* A simple counterexample generator *}
theory Quickcheck
-imports Random Code_Evaluation
+imports Random Code_Evaluation Enum
uses ("Tools/quickcheck_generators.ML")
begin
--- a/src/HOL/Smallcheck.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Smallcheck.thy Mon Nov 22 17:49:12 2010 +0100
@@ -16,7 +16,7 @@
instantiation unit :: small
begin
-definition "find_first f d = f ()"
+definition "small f d = f ()"
instance ..
@@ -48,6 +48,73 @@
end
+section {* full small value generator type classes *}
+
+class full_small = term_of +
+fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation unit :: full_small
+begin
+
+definition "full_small f d = f (Code_Evaluation.valtermify ())"
+
+instance ..
+
+end
+
+instantiation int :: full_small
+begin
+
+function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
+ where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
+instantiation prod :: (full_small, full_small) full_small
+begin
+ML {* @{const_name "Pair"} *}
+definition
+ "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
+ %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
+
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_small}", full_small) full_small
+begin
+
+fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+where
+ "full_small_fun' f i d = (if i > 1 then
+ full_small (%(a, at). full_small (%(b, bt).
+ full_small_fun' (%(g, gt). f (g(a := b),
+ (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+
+(Code_Evaluation.Const (STR ''Fun.fun_upd'')
+
+(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
+
+ (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
+ full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+
+definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+where
+ "full_small_fun f d = full_small_fun' f d d"
+
+
+instance ..
+
+end
+
subsection {* Defining combinators for any first-order data type *}
definition catch_match :: "term list option => term list option => term list option"
@@ -59,7 +126,7 @@
use "Tools/smallvalue_generators.ML"
-(* We do not activate smallcheck yet.
+(* We do not activate smallcheck yet.
setup {* Smallvalue_Generators.setup *}
*)
--- a/src/HOL/Tools/quickcheck_generators.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Mon Nov 22 17:49:12 2010 +0100
@@ -12,7 +12,10 @@
-> seed -> (('a -> 'b) * (unit -> term)) * seed
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
- val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
+ val ensure_sort_datatype:
+ sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
+ string list * string list -> typ list * typ list -> theory -> theory)
+ -> Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
Proof.context -> term -> int -> term list option * (bool list * bool)
val put_counterexample: (unit -> int -> seed -> term list option * seed)
@@ -279,30 +282,29 @@
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle Sorts.CLASS_ERROR _ => NONE;
-fun ensure_random_datatype config raw_tycos thy =
+fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy =
let
val algebra = Sign.classes_of thy;
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
Datatype.the_descr thy raw_tycos;
val typerep_vs = (map o apsnd)
(curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
- val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
+ val sort_insts = (map (rpair sort) o flat o maps snd o maps snd)
(Datatype_Aux.interpret_construction descr typerep_vs
{ atyp = single, dtyp = (K o K o K) [] });
val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
(Datatype_Aux.interpret_construction descr typerep_vs
{ atyp = K [], dtyp = K o K });
val has_inst = exists (fn tyco =>
- can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
+ can (Sorts.mg_domain algebra tyco) sort) tycos;
in if has_inst then thy
- else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
- of SOME constrain => instantiate_random_datatype config descr
+ else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
+ of SOME constrain => instantiate_datatype config descr
(map constrain typerep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
-
(** building and compiling generator expressions **)
structure Counterexample = Proof_Data (
@@ -389,7 +391,7 @@
let
val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
- in if Quickcheck.report ctxt then
+ in if Config.get ctxt Quickcheck.report then
let
val t' = mk_reporting_generator_expr thy t Ts;
val compile = Code_Runtime.dynamic_value_strict
@@ -410,9 +412,9 @@
(** setup **)
val setup =
- Datatype.interpretation ensure_random_datatype
+ Datatype.interpretation (ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
#> Code_Target.extend_target (target, (Code_Runtime.target, K I))
#> Context.theory_map
- (Quickcheck.add_generator ("code", compile_generator_expr));
+ (Quickcheck.add_generator ("random", compile_generator_expr));
end;
--- a/src/HOL/Tools/smallvalue_generators.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Mon Nov 22 17:49:12 2010 +0100
@@ -6,7 +6,6 @@
signature SMALLVALUE_GENERATORS =
sig
- val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
Proof.context -> term -> int -> term list option * (bool list * bool)
val put_counterexample: (unit -> int -> term list option)
@@ -51,10 +50,12 @@
(** abstract syntax **)
+fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
+
val size = @{term "i :: code_numeral"}
val size_pred = @{term "(i :: code_numeral) - 1"}
val size_ge_zero = @{term "(i :: code_numeral) > 0"}
-fun test_function T = Free ("f", T --> @{typ "term list option"})
+fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
fun mk_none_continuation (x, y) =
let
@@ -75,16 +76,23 @@
fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
--> @{typ "Code_Evaluation.term list option"}
+val full_smallN = "full_small";
+
+fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+ --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+
fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
let
- val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
- val smalls = map2 (fn name => fn T => Free (name, smallT T))
+ val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
+ val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
smallsN (Ts @ Us)
fun mk_small_call T =
let
- val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
+ val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
in
- (T, (fn t => small $ absdummy (T, t) $ size_pred))
+ (T, (fn t => small $
+ (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
+ $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
let
@@ -92,14 +100,23 @@
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
val small = nth smalls k
in
- (T, (fn t => small $ absdummy (T, t) $ size_pred))
+ (T, (fn t => small $
+ (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
+ $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
fun mk_consexpr simpleT (c, xs) =
let
val (Ts, fns) = split_list xs
val constr = Const (c, Ts ---> simpleT)
- val bounds = map Bound (((length xs) - 1) downto 0)
- val start_term = test_function simpleT $ (list_comb (constr, bounds))
+ val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
+ val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
+ val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+ val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+ val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
+ bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
+ val start_term = test_function simpleT $
+ (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
+ $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
in fold_rev (fn f => fn t => f t) fns start_term end
fun mk_rhs exprs =
@{term "If :: bool => term list option => term list option => term list option"}
@@ -117,36 +134,21 @@
end
val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
-
-fun gen_inst_state_tac ctxt rel st =
- case Term.add_vars (prop_of st) [] of
- [v as (_, T)] =>
- let
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
- val rel' = cert rel
- val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
- in
- PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
- end
- | _ => Seq.empty;
-
+
fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
- fun my_relation_tac ctxt st =
+ fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+ Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
+ fun mk_termination_measure T =
let
- val ((_ $ (_ $ rel)) :: tl) = prems_of st
- val domT = (HOLogic.dest_setT (fastype_of rel))
- fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
- Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
- val measure = mk_measure (mk_sumcases @{typ nat} mk_single_measure domT)
+ val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
in
- (Function_Common.apply_termination_rule ctxt 1
- THEN gen_inst_state_tac ctxt measure) st
+ mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
end
fun termination_tac ctxt =
- my_relation_tac ctxt
+ Function_Relation.relation_tac ctxt mk_termination_measure 1
THEN rtac @{thm wf_measure} 1
THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
@@ -154,12 +156,12 @@
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1
THEN auto_tac (clasimpset_of ctxt)
- in
+ in
thy
- |> Class.instantiation (tycos, vs, @{sort small})
+ |> Class.instantiation (tycos, vs, @{sort full_small})
|> Function.add_function
(map (fn (T, (name, _)) =>
- Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
+ Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
(map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
Function_Common.default_config pat_completeness_auto
|> snd
@@ -167,34 +169,10 @@
|> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
|> snd
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_smallvalue_datatype config raw_tycos thy =
- let
- val algebra = Sign.classes_of thy;
- val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
- Datatype.the_descr thy raw_tycos;
- val typerep_vs = (map o apsnd)
- (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
- val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = single, dtyp = (K o K o K) [] });
- (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
- (Datatype_Aux.interpret_construction descr typerep_vs
- { atyp = K [], dtyp = K o K });*)
- val has_inst = exists (fn tyco =>
- can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
- in if has_inst then thy
- else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
- of SOME constrain => (instantiate_smallvalue_datatype config descr
- (map constrain typerep_vs) tycos prfx (names, auxnames)
- ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
- handle FUNCTION_TYPE =>
- (Datatype_Aux.message config
- "Creation of smallvalue generators failed because the datatype contains a function type";
- thy))
- | NONE => thy
- end;
+ end handle FUNCTION_TYPE =>
+ (Datatype_Aux.message config
+ "Creation of smallvalue generators failed because the datatype contains a function type";
+ thy)
(** building and compiling generator expressions **)
@@ -209,25 +187,26 @@
fun mk_generator_expr thy prop Ts =
let
val bound_max = length Ts - 1;
- val bounds = map Bound (bound_max downto 0)
- val result = list_comb (prop, bounds);
- val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
+ val bounds = map_index (fn (i, ty) =>
+ (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
+ 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 "Smallcheck.catch_match :: term list option => term list option => term list option"} $
(@{term "If :: bool => term list option => term list option => term list option"}
- $ result $ @{term "None :: term list option"}
- $ (@{term "Some :: term list => term list option"} $ terms))
+ $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
$ @{term "None :: term list option"};
- fun mk_small_closure (depth, T) t =
- Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
- $ absdummy (T, t) $ depth
- in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
+ fun mk_small_closure (_, _, i, T) t =
+ Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
+ in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
fun compile_generator_expr ctxt t =
let
val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
- in if Quickcheck.report ctxt then
+ in if Config.get ctxt Quickcheck.report then
error "Compilation with reporting facility is not supported"
else
let
@@ -242,7 +221,8 @@
(** setup **)
val setup =
- Datatype.interpretation ensure_smallvalue_datatype
+ Datatype.interpretation
+ (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
#> Context.theory_map
(Quickcheck.add_generator ("small", compile_generator_expr));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Birthday_Paradoxon.thy Mon Nov 22 17:49:12 2010 +0100
@@ -0,0 +1,101 @@
+(* Title: HOL/ex/Birthday_Paradoxon.thy
+ Author: Lukas Bulwahn, TU Muenchen, 2007
+*)
+
+header {* A Formulation of the Birthday Paradoxon *}
+
+theory Birthday_Paradoxon
+imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
+begin
+
+section {* Cardinality *}
+
+lemma card_product_dependent:
+ assumes "finite S"
+ assumes "\<forall>x \<in> S. finite (T x)"
+ shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
+proof -
+ note `finite S`
+ moreover
+ have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
+ moreover
+ from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
+ moreover
+ have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
+ moreover
+ ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
+ by (auto, subst card_UN_disjoint) auto
+ also have "... = (SUM x:S. card (T x))"
+ by (subst card_image) (auto intro: inj_onI)
+ finally show ?thesis by auto
+qed
+
+lemma card_extensional_funcset_inj_on:
+ assumes "finite S" "finite T" "card S \<le> card T"
+ shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
+using assms
+proof (induct S arbitrary: T rule: finite_induct)
+ case empty
+ from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
+next
+ case (insert x S)
+ { fix x
+ from `finite T` have "finite (T - {x})" by auto
+ from `finite S` this have "finite (extensional_funcset S (T - {x}))"
+ by (rule finite_extensional_funcset)
+ moreover
+ have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
+ ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
+ by (auto intro: finite_subset)
+ } note finite_delete = this
+ from insert have hyps: "\<forall>y \<in> T. card ({g. g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "\<forall> _ \<in> T. _ = ?k") by auto
+ from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
+ have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
+ card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
+ by metis
+ also from extensional_funcset_extend_domain_inj_onI[OF `x \<notin> S`, of T] have "... = card {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S}"
+ by (simp add: card_image)
+ also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
+ card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
+ also from `finite T` finite_delete have "... = (\<Sum>y \<in> T. card {g. g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S})"
+ by (subst card_product_dependent) auto
+ also from hyps have "... = (card T) * ?k"
+ by auto
+ also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
+ using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
+ by (simp add: fact_mod)
+ also have "... = fact (card T) div fact (card T - card (insert x S))"
+ using insert by (simp add: fact_reduce_nat[of "card T"])
+ finally show ?case .
+qed
+
+lemma card_extensional_funcset_not_inj_on:
+ assumes "finite S" "finite T" "card S \<le> card T"
+ shows "card {f \<in> extensional_funcset S T. \<not> inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))"
+proof -
+ have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
+ from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
+ by (auto intro!: finite_extensional_funcset)
+ have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
+ from assms this finite subset show ?thesis
+ by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
+qed
+
+lemma setprod_upto_nat_unfold:
+ "setprod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * setprod f {m..(n - 1)}))"
+ by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
+
+section {* Birthday paradoxon *}
+
+lemma birthday_paradoxon:
+ assumes "card S = 23" "card T = 365"
+ shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
+proof -
+ from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
+ from assms show ?thesis
+ using card_extensional_funcset[OF `finite S`, of T]
+ card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
+ by (simp add: fact_div_fact setprod_upto_nat_unfold)
+qed
+
+end
--- a/src/HOL/ex/Quickcheck_Examples.thy Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Nov 22 17:49:12 2010 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/ex/Quickcheck_Examples.thy
- Author: Stefan Berghofer
- Copyright 2004 TU Muenchen
+ Author: Stefan Berghofer, Lukas Bulwahn
+ Copyright 2004 - 2010 TU Muenchen
*)
header {* Examples for the 'quickcheck' command *}
@@ -9,29 +9,41 @@
imports Main
begin
+setup {* Smallvalue_Generators.setup *}
+
text {*
The 'quickcheck' command allows to find counterexamples by evaluating
-formulae under an assignment of free variables to random values.
-In contrast to 'refute', it can deal with inductive datatypes,
-but cannot handle quantifiers.
+formulae.
+Currently, there are two different exploration schemes:
+- random testing: this is incomplete, but explores the search space faster.
+- exhaustive testing: this is complete, but increasing the depth leads to
+ exponentially many assignments.
+
+quickcheck can handle quantifiers on finite universes.
+
*}
subsection {* Lists *}
theorem "map g (map f xs) = map (g o f) xs"
- quickcheck[expect = no_counterexample]
+ quickcheck[size = 3]
+ quickcheck[generator = random, expect = no_counterexample]
+ quickcheck[generator = small, size = 3, iterations = 1, report = false, expect = no_counterexample]
oops
theorem "map g (map f xs) = map (f o g) xs"
- quickcheck[expect = counterexample]
+ quickcheck[generator = random, expect = counterexample]
+ quickcheck[generator = small, report = false]
oops
theorem "rev (xs @ ys) = rev ys @ rev xs"
quickcheck[expect = no_counterexample]
+ quickcheck[generator = small, expect = no_counterexample, report = false]
oops
theorem "rev (xs @ ys) = rev xs @ rev ys"
- quickcheck[expect = counterexample]
+ quickcheck[generator = small, expect = counterexample, report = false]
+ quickcheck[generator = random, expect = counterexample]
oops
theorem "rev (rev xs) = xs"
@@ -39,6 +51,7 @@
oops
theorem "rev xs = xs"
+ quickcheck[generator = small, report = false]
quickcheck[expect = counterexample]
oops
@@ -49,11 +62,13 @@
| "app (f # fs) x = app fs (f x)"
lemma "app (fs @ gs) x = app gs (app fs x)"
- quickcheck[expect = no_counterexample]
+ quickcheck[generator = random, expect = no_counterexample]
+ quickcheck[generator = small, iterations = 1, size = 4, report = false, expect = no_counterexample]
by (induct fs arbitrary: x) simp_all
lemma "app (fs @ gs) x = app fs (app gs x)"
- quickcheck[expect = counterexample]
+ quickcheck[generator = random, expect = counterexample]
+ quickcheck[generator = small, report = false, expect = counterexample]
oops
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -67,15 +82,18 @@
text {* A lemma, you'd think to be true from our experience with delAll *}
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
-- {* Wrong. Precondition needed.*}
+ quickcheck[generator = small, report = false]
quickcheck[expect = counterexample]
oops
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck[generator = small, report = false]
quickcheck[expect = counterexample]
-- {* Also wrong.*}
oops
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck[generator = small, report = false]
quickcheck[expect = no_counterexample]
by (induct xs) auto
@@ -85,12 +103,13 @@
else (x#(replace a b xs)))"
lemma "occurs a xs = occurs b (replace a b xs)"
+ quickcheck[generator = small, report = false]
quickcheck[expect = counterexample]
-- {* Wrong. Precondition needed.*}
oops
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
- quickcheck[expect = no_counterexample]
+ quickcheck[expect = no_counterexample, report = false]
by (induct xs) simp_all
@@ -133,8 +152,106 @@
| "root (Node f x y) = f"
theorem "hd (inOrder xt) = root xt"
+ quickcheck[generator = small, report = false]
quickcheck[expect = counterexample]
--{* Wrong! *}
oops
+
+subsection {* Exhaustive Testing beats Random Testing *}
+
+text {* Here are some examples from mutants from the List theory
+where exhaustive testing beats random testing *}
+
+lemma
+ "[] ~= xs ==> hd xs = last (x # xs)"
+quickcheck[generator = random, report = false]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+ assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
+ shows "drop n xs = takeWhile P xs"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+oops
+
+lemma
+ "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+oops
+
+lemma
+ "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[generator = random, iterations = 10000, report = false, quiet]
+quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+oops
+
+lemma
+ "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[generator = random, iterations = 1000, report = false, quiet]
+quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+oops
+
+lemma
+ "ns ! k < length ns ==> k <= listsum ns"
+quickcheck[generator = random, iterations = 10000, report = true, quiet]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+ "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
+quickcheck[generator = random, iterations = 10000, report = true]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+ "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false]
+oops
+
+lemma
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+lemma
+ "(ys = zs) = (xs @ ys = splice xs zs)"
+quickcheck[generator = random]
+quickcheck[generator = small, report = false, expect = counterexample]
+oops
+
+section {* Examples with quantifiers *}
+
+text {*
+ These examples show that we can handle quantifiers.
+*}
+
+lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
+ quickcheck[expect = counterexample]
+oops
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+ quickcheck[expect = counterexample]
+oops
+
+lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+ quickcheck[expect = counterexample]
+oops
+
end
--- a/src/HOL/ex/ROOT.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/HOL/ex/ROOT.ML Mon Nov 22 17:49:12 2010 +0100
@@ -67,7 +67,8 @@
"Summation",
"Gauge_Integration",
"Dedekind_Real",
- "Quicksort"
+ "Quicksort",
+ "Birthday_Paradoxon"
];
HTML.with_charset "utf-8" (no_document use_thys)
--- a/src/Pure/Isar/proof.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/Pure/Isar/proof.ML Mon Nov 22 17:49:12 2010 +0100
@@ -16,6 +16,7 @@
val context_of: state -> context
val theory_of: state -> theory
val map_context: (context -> context) -> state -> state
+ val map_context_result : (context -> 'a * context) -> state -> 'a * state
val map_contexts: (context -> context) -> state -> state
val propagate_ml_env: state -> state
val bind_terms: (indexname * term option) list -> state -> state
--- a/src/Tools/quickcheck.ML Mon Nov 22 17:46:51 2010 +0100
+++ b/src/Tools/quickcheck.ML Mon Nov 22 17:49:12 2010 +0100
@@ -10,25 +10,33 @@
(* configuration *)
val auto: bool Unsynchronized.ref
val timing : bool Unsynchronized.ref
+ val size : int Config.T
+ val iterations : int Config.T
+ val no_assms : bool Config.T
+ val report : bool Config.T
+ val quiet : bool Config.T
+ val timeout : real Config.T
+ val finite_types : bool Config.T
+ val finite_type_size : int Config.T
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
- datatype expectation = No_Expectation | No_Counterexample | Counterexample;
- datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : real};
+ datatype expectation = No_Expectation | No_Counterexample | Counterexample;
+ datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
val test_params_of : Proof.context -> test_params
- val report : Proof.context -> bool
- val map_test_params :
- ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
- -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
+ val map_test_params : (typ list * expectation -> typ list * expectation)
-> Context.generic -> Context.generic
val add_generator:
string * (Proof.context -> term -> int -> term list option * (bool list * bool))
-> Context.generic -> Context.generic
(* testing terms and proof states *)
+ val test_term_small: Proof.context -> term ->
+ (string * term) list option * ((string * int) list * ((int * report list) list) option)
val test_term: Proof.context -> string option -> term ->
(string * term) list option * ((string * int) list * ((int * report list) list) option)
+ val test_goal_terms:
+ Proof.context -> string option * (string * typ) list -> term list
+ -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
end;
@@ -78,43 +86,39 @@
if expect1 = expect2 then expect1 else No_Expectation
(* quickcheck configuration -- default parameters, test generators *)
+val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
+val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
+val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
+val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
+val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
+val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
+val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
+val (finite_type_size, setup_finite_type_size) = Attrib.config_int "quickcheck_finite_type_size" (K 3)
+
+val setup_config =
+ setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
+ #> setup_finite_types #> setup_finite_type_size
datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : real};
+ {default_type: typ list, expect : expectation};
-fun dest_test_params
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))));
+fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
-fun make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) =
- Test_Params { size = size, iterations = iterations, default_type = default_type,
- no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout };
+fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect};
-fun map_test_params' f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))));
+fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
fun merge_test_params
- (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 },
- Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) =
- make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
- ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
- ((merge_expectation (expect1, expect2), report1 orelse report2),
- (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
+ (Test_Params {default_type = default_type1, expect = expect1},
+ Test_Params {default_type = default_type2, expect = expect2}) =
+ make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
structure Data = Generic_Data
(
type T =
(string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
* test_params;
- val empty = ([], Test_Params
- { size = 10, iterations = 100, default_type = [], no_assms = false,
- expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
+ val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
fun merge ((generators1, params1), (generators2, params2)) : T =
(AList.merge (op =) (K true) (generators1, generators2),
@@ -123,35 +127,9 @@
val test_params_of = snd o Data.get o Context.Proof;
-val size = fst o fst o dest_test_params o test_params_of
-
-val iterations = snd o fst o dest_test_params o test_params_of
-
-val default_type = fst o fst o snd o dest_test_params o test_params_of
-
-val no_assms = snd o fst o snd o dest_test_params o test_params_of
-
-val expect = fst o fst o snd o snd o dest_test_params o test_params_of
-
-val report = snd o fst o snd o snd o dest_test_params o test_params_of
-
-val quiet = fst o snd o snd o snd o dest_test_params o test_params_of
+val default_type = fst o dest_test_params o test_params_of
-val timeout = snd o snd o snd o snd o dest_test_params o test_params_of
-
-fun map_report f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout))));
-
-fun map_quiet f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout))));
-
-fun set_report report = Data.map (apsnd (map_report (K report)))
-
-fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet)))
+val expect = snd o dest_test_params o test_params_of
val map_test_params = Data.map o apsnd o map_test_params'
@@ -197,6 +175,40 @@
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
+fun test_term_small ctxt t =
+ let
+ val (names, t') = prep_test_term t;
+ val current_size = Unsynchronized.ref 0
+ fun excipit s =
+ "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
+ val (tester, comp_time) = cpu_time "compilation"
+ (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
+ val empty_report = Report { iterations = 0, raised_match_errors = 0,
+ satisfied_assms = [], positive_concl_tests = 0 }
+ fun with_size k timings =
+ if k > Config.get ctxt size then (NONE, timings)
+ else
+ let
+ val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+ val _ = current_size := k
+ val (result, timing) = cpu_time ("size " ^ string_of_int k)
+ (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE))
+ in
+ case result of
+ NONE => with_size (k + 1) (timing :: timings)
+ | SOME q => (SOME q, (timing :: timings))
+ end;
+ val result = with_size 1 [comp_time]
+ in
+ apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
+ end
+
+(* we actually assume we know the generators and its behaviour *)
+fun is_iteratable "SML" = true
+ | is_iteratable "random" = true
+ | is_iteratable _ = false
+
fun test_term ctxt generator_name t =
let
val (names, t') = prep_test_term t;
@@ -205,12 +217,13 @@
"Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
val (testers, comp_time) = cpu_time "quickcheck compilation"
(fn () => (case generator_name
- of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
+ of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
| SOME name => [mk_tester_select name ctxt t']));
fun iterate f 0 report = (NONE, report)
| iterate f j report =
let
- val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then ()
+ val (test_result, single_report) = apsnd Run (f ()) handle Match =>
+ (if Config.get ctxt quiet then ()
else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
val report = collect_single_report single_report report
in
@@ -220,20 +233,29 @@
satisfied_assms = [], positive_concl_tests = 0 }
fun with_testers k [] = (NONE, [])
| with_testers k (tester :: testers) =
- case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report
+ let
+ val niterations = case generator_name of
+ SOME generator_name =>
+ if is_iteratable generator_name then Config.get ctxt iterations else 1
+ | NONE => Config.get ctxt iterations
+ val (result, timing) = cpu_time ("size " ^ string_of_int k)
+ (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
+ in
+ case result
of (NONE, report) => apsnd (cons report) (with_testers k testers)
- | (SOME q, report) => (SOME q, [report]);
+ | (SOME q, report) => (SOME q, [report])
+ end
fun with_size k reports =
- if k > size ctxt then (NONE, reports)
+ if k > Config.get ctxt size then (NONE, reports)
else
- (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+ (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
let
- val _ = current_size := k
+ val _ = current_size := k
val (result, new_report) = with_testers k testers
val reports = ((k, new_report) :: reports)
in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
val ((result, reports), exec_time) =
- TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
+ TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
(fn () => apfst
(fn result => case result of NONE => NONE
| SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
@@ -241,9 +263,14 @@
error (excipit "ran out of time")
| Exn.Interrupt => error (excipit "was interrupted") (* FIXME violates Isabelle/ML exception model *)
in
- (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
+ (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
end;
+fun get_finite_types ctxt =
+ fst (chop (Config.get ctxt finite_type_size)
+ (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
+ "Enum.finite_4", "Enum.finite_5"]))
+
exception WELLSORTED of string
fun monomorphic_term thy insts default_T =
@@ -264,7 +291,32 @@
datatype wellsorted_error = Wellsorted_Error of string | Term of term
-fun test_goal generator_name insts i state =
+fun test_goal_terms lthy (generator_name, insts) check_goals =
+ let
+ val thy = ProofContext.theory_of lthy
+ val inst_goals =
+ if Config.get lthy finite_types then
+ maps (fn check_goal => map (fn T =>
+ Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+ handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
+ else
+ maps (fn check_goal => map (fn T =>
+ Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+ handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
+ val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
+ val correct_inst_goals =
+ case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
+ [] => error error_msg
+ | xs => xs
+ val _ = if Config.get lthy quiet then () else warning error_msg
+ fun collect_results f reports [] = (NONE, rev reports)
+ | collect_results f reports (t :: ts) =
+ case f t of
+ (SOME res, report) => (SOME res, rev (report :: reports))
+ | (NONE, report) => collect_results f (report :: reports) ts
+ in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
+
+fun test_goal (generator_name, insts) i state =
let
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -276,7 +328,7 @@
of NONE => NONE
| SOME "" => NONE
| SOME locale => SOME locale;
- val assms = if no_assms lthy then [] else case some_locale
+ val assms = if Config.get lthy no_assms then [] else case some_locale
of NONE => Assumption.all_assms_of lthy
| SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
@@ -284,21 +336,9 @@
of NONE => [proto_goal]
| SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
- val inst_goals = maps (fn check_goal => map (fn T =>
- Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
- handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
- val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
- val correct_inst_goals =
- case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
- [] => error error_msg
- | xs => xs
- val _ = if quiet lthy then () else warning error_msg
- fun collect_results f reports [] = (NONE, rev reports)
- | collect_results f reports (t :: ts) =
- case f t of
- (SOME res, report) => (SOME res, rev (report :: reports))
- | (NONE, report) => collect_results f (report :: reports) ts
- in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
+ in
+ test_goal_terms lthy (generator_name, insts) check_goals
+ end
(* pretty printing *)
@@ -349,8 +389,8 @@
val ctxt = Proof.context_of state;
val res =
state
- |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true))
- |> try (test_goal NONE [] 1);
+ |> Proof.map_context (Config.put report false #> Config.put quiet true)
+ |> try (test_goal (NONE, []) 1);
in
case res of
NONE => (false, state)
@@ -360,7 +400,7 @@
end
val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
-
+ #> setup_config
(* Isar commands *)
@@ -383,57 +423,37 @@
| read_expectation "counterexample" = Counterexample
| read_expectation s = error ("Not an expectation value: " ^ s)
-fun parse_test_param ctxt ("size", [arg]) =
- (apfst o apfst o K) (read_nat arg)
- | parse_test_param ctxt ("iterations", [arg]) =
- (apfst o apsnd o K) (read_nat arg)
- | parse_test_param ctxt ("default_type", arg) =
- (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
- | parse_test_param ctxt ("no_assms", [arg]) =
- (apsnd o apfst o apsnd o K) (read_bool arg)
- | parse_test_param ctxt ("expect", [arg]) =
- (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
- | parse_test_param ctxt ("report", [arg]) =
- (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
- | parse_test_param ctxt ("quiet", [arg]) =
- (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
- | parse_test_param ctxt ("timeout", [arg]) =
- (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
- | parse_test_param ctxt (name, _) =
- error ("Unknown test parameter: " ^ name);
+fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
+ | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
+ | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
+ map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
+ | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
+ | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
+ | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
+ | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
+ | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
+ | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
+ | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
+ | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
-fun parse_test_param_inst ctxt ("generator", [arg]) =
- (apsnd o apfst o K o SOME) arg
- | parse_test_param_inst ctxt (name, arg) =
+fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
+ (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
+ | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
case try (ProofContext.read_typ ctxt) name
- of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
- (v, ProofContext.read_typ ctxt (the_single arg))
- | _ => (apfst o parse_test_param ctxt) (name, arg);
+ of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
+ (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
+ | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
-fun quickcheck_params_cmd args thy =
- let
- val ctxt = ProofContext.init_global thy
- val f = fold (parse_test_param ctxt) args;
- in
- thy
- |> (Context.theory_map o map_test_params) f
- end;
-
+fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
+
fun gen_quickcheck args i state =
- let
- val ctxt = Proof.context_of state;
- val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
- val f = fold (parse_test_param_inst ctxt) args;
- val (test_params, (generator_name, insts)) = f (default_params, (NONE, []));
- in
- state
- |> Proof.map_context (Context.proof_map (map_test_params (K test_params)))
- |> (fn state' => test_goal generator_name insts i state'
- |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
- error ("quickcheck expected to find no counterexample but found one") else ()
- | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
- error ("quickcheck expected to find a counterexample but did not find one") else ()))
- end;
+ state
+ |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
+ |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
+ |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
+ error ("quickcheck expected to find no counterexample but found one") else ()
+ | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
+ error ("quickcheck expected to find a counterexample but did not find one") else ()))
fun quickcheck args i state = fst (gen_quickcheck args i state);