# HG changeset patch # User haftmann # Date 1290444552 -3600 # Node ID 3b9b39ac1f24c138474075cde54e8ee3a3482bc1 # Parent abd4e73588476ee507d97dee5b21c97bf3e12e40# Parent f643399acab30daea34ccf4da748bf3d4da33cc6 merged diff -r abd4e7358847 -r 3b9b39ac1f24 NEWS --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Code_Evaluation.thy --- 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 \ term \ term" where "App _ _ = dummy_term" -code_datatype Const App +definition Abs :: "String.literal \ typerep \ term \ term" where + "Abs _ _ _ = dummy_term" + +code_datatype Const App Abs class term_of = typerep + fixes term_of :: "'a \ 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 \ String.literal \ 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Enum.thy --- /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 \ set enum" + unfolding enum_all by auto + +lemma enum_eq_I: + assumes "\x. x \ 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 \ (\x \ 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 :: _ \ _) f \ True" + by (fact equal_refl) + +lemma [code]: + "HOL.equal f g \ 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\enum \ 'b\order" + shows "f \ g \ list_all (\x. f x \ g x) enum" + and "f < g \ f \ g \ list_ex (\x. f x \ 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]: "(\x. P x) \ list_all P enum" + by (simp add: list_all_iff enum_all) + +lemma exists_code [code]: "(\x. P x) \ list_ex P enum" + by (simp add: list_ex_iff enum_all) + +lemma exists1_code[code]: "(\!x. P x) \ list_ex1 P enum" +unfolding list_ex1_iff enum_all by auto + + +subsection {* Default instances *} + +primrec n_lists :: "nat \ 'a list \ 'a list list" where + "n_lists 0 xs = [[]]" + | "n_lists (Suc n) xs = concat (map (\ys. map (\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 \ set (n_lists n xs) \ length ys = n" + by (induct n arbitrary: ys) auto + +lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \ set ys \ set xs}" +proof (rule set_eqI) + fix ys :: "'a list" + show "ys \ set (n_lists n xs) \ ys \ {ys. length ys = n \ set ys \ set xs}" + proof - + have "ys \ set (n_lists n xs) \ length ys = n" + by (induct n arbitrary: ys) auto + moreover have "\x. ys \ set (n_lists n xs) \ x \ set ys \ x \ set xs" + by (induct n arbitrary: ys) auto + moreover have "set ys \ set xs \ ys \ 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 (\ys\set (n_lists n xs). (\y. y # ys) ` set xs) + = (\ys\set (n_lists n xs). card ((\y. y # ys) ` set xs))" + by (rule card_UN_disjoint) auto + moreover have "\ys. card ((\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 "\ = 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 \ 'a\enum list)" + shows "\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y" +proof - + from assms have "x \ set (enum \ 'a\enum list) \ + (\y. map_of (zip (enum \ 'a\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\enum list" + assumes length: "length xs = length (enum \ 'a\enum list)" + "length ys = length (enum \ 'a\enum list)" + and map_of: "the \ map_of (zip (enum \ 'a\enum list) xs) = the \ map_of (zip (enum \ 'a\enum list) ys)" + shows "xs = ys" +proof - + have "map_of (zip (enum \ 'a list) xs) = map_of (zip (enum \ 'a list) ys)" + proof + fix x :: 'a + from length map_of_zip_enum_is_Some obtain y1 y2 + where "map_of (zip (enum \ 'a list) xs) x = Some y1" + and "map_of (zip (enum \ 'a list) ys) x = Some y2" by blast + moreover from map_of have "the (map_of (zip (enum \ 'a\enum list) xs) x) = the (map_of (zip (enum \ 'a\enum list) ys) x)" + by (auto dest: fun_cong) + ultimately show "map_of (zip (enum \ 'a\enum list) xs) x = map_of (zip (enum \ 'a\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 (\ys. the o map_of (zip (enum\'a list) ys)) (n_lists (length (enum\'a\enum list)) enum)" + +instance proof + show "UNIV = set (enum \ ('a \ 'b) list)" + proof (rule UNIV_eq_I) + fix f :: "'a \ 'b" + have "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" + by (auto simp add: map_of_zip_map fun_eq_iff) + then show "f \ set enum" + by (auto simp add: enum_fun_def set_n_lists) + qed +next + from map_of_zip_enum_inject + show "distinct (enum \ ('a \ '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 \ 'a\{enum, equal} list) + in map (\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 \ 'b list \ ('a \ '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 \ 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 \ '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\nat)) ^ length xs" + by (induct xs) (simp_all add: Let_def) + +lemma sublists_powset: + "set ` set (sublists xs) = Pow (set xs)" +proof - + have aux: "\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 \ finite_1 \ bool" +where + "less_eq_finite_1 x y = True" + +definition less_finite_1 :: "finite_1 \ finite_1 \ 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 \ finite_2 \ bool" +where + "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))" + +definition less_eq_finite_2 :: "finite_2 \ finite_2 \ bool" +where + "less_eq_finite_2 x y = ((x = y) \ (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 \ finite_3 \ bool" +where + "less_finite_3 x y = (case x of a\<^isub>1 => (y \ a\<^isub>1) + | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)" + +definition less_eq_finite_3 :: "finite_3 \ finite_3 \ bool" +where + "less_eq_finite_3 x y = ((x = y) \ (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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/IsaMakefile --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Library/Enum.thy --- 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 \ set enum" - unfolding enum_all by auto - -lemma enum_eq_I: - assumes "\x. x \ 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 \ (\x \ 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 :: _ \ _) f \ True" - by (fact equal_refl) - -lemma order_fun [code]: - fixes f g :: "'a\enum \ 'b\order" - shows "f \ g \ list_all (\x. f x \ g x) enum" - and "f < g \ f \ g \ list_ex (\x. f x \ 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]: "(\x. P x) \ list_all P enum" - by (simp add: list_all_iff enum_all) - -lemma exists_code [code]: "(\x. P x) \ list_ex P enum" - by (simp add: list_ex_iff enum_all) - - -subsection {* Default instances *} - -primrec n_lists :: "nat \ 'a list \ 'a list list" where - "n_lists 0 xs = [[]]" - | "n_lists (Suc n) xs = concat (map (\ys. map (\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 \ set (n_lists n xs) \ length ys = n" - by (induct n arbitrary: ys) auto - -lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \ set ys \ set xs}" -proof (rule set_eqI) - fix ys :: "'a list" - show "ys \ set (n_lists n xs) \ ys \ {ys. length ys = n \ set ys \ set xs}" - proof - - have "ys \ set (n_lists n xs) \ length ys = n" - by (induct n arbitrary: ys) auto - moreover have "\x. ys \ set (n_lists n xs) \ x \ set ys \ x \ set xs" - by (induct n arbitrary: ys) auto - moreover have "set ys \ set xs \ ys \ 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 (\ys\set (n_lists n xs). (\y. y # ys) ` set xs) - = (\ys\set (n_lists n xs). card ((\y. y # ys) ` set xs))" - by (rule card_UN_disjoint) auto - moreover have "\ys. card ((\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 "\ = 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 \ 'a\enum list)" - shows "\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y" -proof - - from assms have "x \ set (enum \ 'a\enum list) \ - (\y. map_of (zip (enum \ 'a\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\enum list" - assumes length: "length xs = length (enum \ 'a\enum list)" - "length ys = length (enum \ 'a\enum list)" - and map_of: "the \ map_of (zip (enum \ 'a\enum list) xs) = the \ map_of (zip (enum \ 'a\enum list) ys)" - shows "xs = ys" -proof - - have "map_of (zip (enum \ 'a list) xs) = map_of (zip (enum \ 'a list) ys)" - proof - fix x :: 'a - from length map_of_zip_enum_is_Some obtain y1 y2 - where "map_of (zip (enum \ 'a list) xs) x = Some y1" - and "map_of (zip (enum \ 'a list) ys) x = Some y2" by blast - moreover from map_of have "the (map_of (zip (enum \ 'a\enum list) xs) x) = the (map_of (zip (enum \ 'a\enum list) ys) x)" - by (auto dest: fun_cong) - ultimately show "map_of (zip (enum \ 'a\enum list) xs) x = map_of (zip (enum \ 'a\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 (\ys. the o map_of (zip (enum\'a list) ys)) (n_lists (length (enum\'a\enum list)) enum)" - -instance proof - show "UNIV = set (enum \ ('a \ 'b) list)" - proof (rule UNIV_eq_I) - fix f :: "'a \ 'b" - have "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" - by (auto simp add: map_of_zip_map fun_eq_iff) - then show "f \ set enum" - by (auto simp add: enum_fun_def set_n_lists) - qed -next - from map_of_zip_enum_inject - show "distinct (enum \ ('a \ '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 \ 'a\{enum, equal} list) - in map (\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 \ 'b list \ ('a \ '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 \ 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 \ '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\nat)) ^ length xs" - by (induct xs) (simp_all add: Let_def) - -lemma sublists_powset: - "set ` set (sublists xs) = Pow (set xs)" -proof - - have aux: "\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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Library/FuncSet.thy --- 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 \ B\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) \ (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 \ {}" + shows "extensional_funcset S {} = {}" +using assms unfolding extensional_funcset_def by auto + +lemma extensional_funcset_arb: + assumes "f \ extensional_funcset S T" "x \ S" + shows "f x = undefined" +using assms +unfolding extensional_funcset_def by auto (auto dest!: extensional_arb) + +lemma extensional_funcset_mem: "f \ extensional_funcset S T \ x \ S \ f x \ 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: "\ y \ T; f \ extensional_funcset S T\ \ f(x := y) \ extensional_funcset (insert x S) T" +unfolding extensional_funcset_def extensional_def by auto + +lemma extensional_funcset_restrict_domain: + "x \ S \ f \ extensional_funcset (insert x S) T \ f(x := undefined) \ extensional_funcset S T" +unfolding extensional_funcset_def extensional_def by auto + +lemma extensional_funcset_extend_domain_eq: + assumes "x \ S" + shows + "extensional_funcset (insert x S) T = (\(y, g). g(x := y)) ` {(y, g). y \ T \ g \ 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: "\ y \ S. f x \ 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 \ 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 \ 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 \ S" + shows"{f. f \ extensional_funcset (insert x S) T \ inj_on f (insert x S)} = + (%(y, g). g(x:=y)) ` {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ 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 \ S" + shows "inj_on (\(y, g). g(x := y)) {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ 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 \ extensional_funcset S T" + "g' \ extensional_funcset S T" + "y \ T" "y' \ 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 (\(y, g). g (x := y)) (T \ 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) \ 0) \ (S \ {} \ T = {})" + by auto + from this show ?thesis + proof + assume "card (extensional_funcset S T) \ 0" + from this show ?thesis + by (auto intro: card_ge_0_finite) + next + assume "S \ {} \ T = {}" + from this show ?thesis + by (auto simp add: extensional_funcset_empty_range) + qed +qed + end diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Library/Library.thy --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Library/Quickcheck_Types.thy --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/List.thy --- 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 \ bool) \ 'a list \ bool" where list_ex_iff [code_post]: "list_ex P xs \ (\x \ set xs. P x)" +definition list_ex1 +where + list_ex1_iff: "list_ex1 P xs \ (\! x. x \ set xs \ P x)" + text {* Usually you should prefer @{text "\x\set xs"} and @{text "\x\set xs"} over @{const list_all} and @{const list_ex} in specifications. @@ -4892,6 +4896,11 @@ "list_ex P [] \ 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 (\y. \ P y \ 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 \ list_all P xs" by (simp add: list_all_iff) diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Mirabelle/Mirabelle_Test.thy --- 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 {* diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML --- /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; diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Mutabelle/MutabelleExtra.thy --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Mutabelle/mutabelle.ML --- 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); diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Mutabelle/mutabelle_extra.ML --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy --- 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 \ 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Quickcheck.thy --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Smallcheck.thy --- 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) \ term list option) \ code_numeral \ 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 *} *) diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/Tools/smallvalue_generators.ML --- 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)); diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/ex/Birthday_Paradoxon.thy --- /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 "\x \ S. finite (T x)" + shows "card {(x, y). x \ S \ y \ T x} = (\x \ S. card (T x))" +proof - + note `finite S` + moreover + have "{(x, y). x \ S \ y \ T x} = (UN x : S. Pair x ` T x)" by auto + moreover + from `\x \ 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 \ S \ y \ 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 \ card T" + shows "card {f \ 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} \ (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: "\y \ T. card ({g. g \ extensional_funcset S (T - {y}) \ inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "\ _ \ T. _ = ?k") by auto + from extensional_funcset_extend_domain_inj_on_eq[OF `x \ 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 \ 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 \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S} = + card {(y, g). y \ T \ g \ {f \ extensional_funcset S (T - {y}). inj_on f S}}" by auto + also from `finite T` finite_delete have "... = (\y \ T. card {g. g \ extensional_funcset S (T - {y}) \ 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 \ card T" + shows "card {f \ extensional_funcset S T. \ 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 \ extensional_funcset S T. \ inj_on f S} = extensional_funcset S T - {f \ 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 \ extensional_funcset S T. \ inj_on f S} \ 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/ex/Quickcheck_Examples.thy --- 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 \ 'a list \ 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 ~= [] \ 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 \ 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 \ a=b \ 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.. f (lcm m i) = map f [m.. 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. {..x. P x) \ (\x. P x)" + quickcheck[expect = counterexample] +oops + +lemma "(\x. \y. P x y) \ (\y. \x. P x y)" + quickcheck[expect = counterexample] +oops + +lemma "(\x. P x) \ (EX! x. P x)" + quickcheck[expect = counterexample] +oops + end diff -r abd4e7358847 -r 3b9b39ac1f24 src/HOL/ex/ROOT.ML --- 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) diff -r abd4e7358847 -r 3b9b39ac1f24 src/Pure/Isar/proof.ML --- 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 diff -r abd4e7358847 -r 3b9b39ac1f24 src/Tools/quickcheck.ML --- 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);