# HG changeset patch # User wenzelm # Date 1441828304 -7200 # Node ID 497eb43a306496f857ce10cb0a9571a4c8f3d7a2 # Parent 92858a52e45b7ed4c9c3bce8c06a2bde53fac676# Parent 5e94dfead1c2f370d6120350ad04df3577c610c4 merged diff -r 5e94dfead1c2 -r 497eb43a3064 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 09 20:57:21 2015 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 09 21:51:44 2015 +0200 @@ -212,6 +212,18 @@ done qed +subsection \Alternative rules for membership in lists\ + +declare in_set_member[code_pred_inline] + +lemma member_intros [code_pred_intro]: + "List.member (x#xs) x" + "List.member xs x \ List.member (y#xs) x" +by(simp_all add: List.member_def) + +code_pred List.member + by(auto simp add: List.member_def elim: list.set_cases) + section \Setup for String.literal\ setup \Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\ diff -r 5e94dfead1c2 -r 497eb43a3064 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Sep 09 20:57:21 2015 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Wed Sep 09 21:51:44 2015 +0200 @@ -2,6 +2,7 @@ imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" begin +(* section {* Sets *} lemma "x \ {(1::nat)} ==> False" @@ -35,6 +36,7 @@ "x \ {1, 2} \ {3, 4} ==> x = (1::nat) \ x = (2::nat)" quickcheck[generator=predicate_compile_wo_ff] oops +*) section {* Equivalences *} @@ -48,7 +50,7 @@ lemma "is_ten x = is_eleven x" -quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample] +quickcheck[tester = smart_exhaustive, iterations = 1, size = 1, expect = counterexample] oops section {* Context Free Grammar *} @@ -64,13 +66,13 @@ | "\v \ B\<^sub>1; v \ B\<^sub>1\ \ a # v @ w \ B\<^sub>1" lemma - "w \ S\<^sub>1 \ w = []" -quickcheck[tester = predicate_compile_ff_nofs, iterations=1] + "S\<^sub>1p w \ w = []" +quickcheck[tester = smart_exhaustive, iterations=1] oops theorem S\<^sub>1_sound: -"w \ S\<^sub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile_ff_nofs, size=15] +"S\<^sub>1p w \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[tester=smart_exhaustive, size=15] oops @@ -111,8 +113,8 @@ oops *) theorem S\<^sub>2_sound: -"w \ S\<^sub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile_ff_nofs, size=5, iterations=10] +"S\<^sub>2p w \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[tester=smart_exhaustive, size=5, iterations=10] oops inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where @@ -123,26 +125,26 @@ | "w \ S\<^sub>3 \ b # w \ B\<^sub>3" | "\v \ B\<^sub>3; w \ B\<^sub>3\ \ a # v @ w \ B\<^sub>3" -code_pred [inductify, skip_proof] S\<^sub>3 . -thm S\<^sub>3.equation +code_pred [inductify, skip_proof] S\<^sub>3p . +thm S\<^sub>3p.equation (* values 10 "{x. S\<^sub>3 x}" *) lemma S\<^sub>3_sound: -"w \ S\<^sub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=10] +"S\<^sub>3p w \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[tester=smart_exhaustive, size=10, iterations=10] oops lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" -quickcheck[size=10, tester = predicate_compile_ff_fs] +quickcheck[size=10, tester = smart_exhaustive] oops theorem S\<^sub>3_complete: -"length [x \ w. x = a] = length [x \ w. b = x] \ w \ S\<^sub>3" +"length [x \ w. x = a] = length [x \ w. b = x] \ S\<^sub>3p w" (*quickcheck[generator=SML]*) -quickcheck[generator=predicate_compile_ff_fs, size=10, iterations=100] +quickcheck[tester=smart_exhaustive, size=10, iterations=100] oops @@ -156,13 +158,13 @@ | "\v \ B\<^sub>4; w \ B\<^sub>4\ \ a # v @ w \ B\<^sub>4" theorem S\<^sub>4_sound: -"w \ S\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1] +"S\<^sub>4p w \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[tester = smart_exhaustive, size=5, iterations=1] oops theorem S\<^sub>4_complete: -"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^sub>4" -quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1] +"length [x \ w. x = a] = length [x \ w. x = b] \ S\<^sub>4p w" +quickcheck[tester = smart_exhaustive, size=5, iterations=1] oops hide_const a b @@ -201,7 +203,7 @@ lemma "exec c s s' ==> exec (Seq c c) s s'" - quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample] + quickcheck[tester = smart_exhaustive, size=2, iterations=20, expect = counterexample] oops subsection {* Lambda *} @@ -256,7 +258,7 @@ lemma "\ \ t : U \ t \\<^sub>\ t' \ \ \ t' : U" -quickcheck[tester = predicate_compile_ff_fs, size = 7, iterations = 10] +quickcheck[tester = smart_exhaustive, size = 7, iterations = 10] oops subsection {* JAD *} @@ -281,12 +283,11 @@ unfolding matrix_def by auto qed -code_pred [random_dseq inductify] matrix +code_pred [random_dseq] matrix apply (cases x) unfolding matrix_def apply fastforce apply fastforce done - values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" definition "scalar_product v w = (\ (x, y)\zip v w. x * y)" @@ -340,12 +341,12 @@ "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\ (i, x). v ! i * x)))" lemma "matrix (M::int list list) rs cs \ False" -quickcheck[tester = predicate_compile_ff_nofs, size = 6] +quickcheck[tester = smart_exhaustive, size = 6] oops lemma "\ matrix M rs cs ; length v = cs \ \ jad_mv v (jad M) = mv M v" -quickcheck[tester = predicate_compile_wo_ff] +quickcheck[tester = smart_exhaustive] oops end diff -r 5e94dfead1c2 -r 497eb43a3064 src/HOL/ROOT --- a/src/HOL/ROOT Wed Sep 09 20:57:21 2015 +0200 +++ b/src/HOL/ROOT Wed Sep 09 21:51:44 2015 +0200 @@ -975,15 +975,14 @@ theories Examples Predicate_Compile_Tests - (* FIXME - Predicate_Compile_Quickcheck_Examples -- should be added again soon (since 21-Oct-2010) *) + Predicate_Compile_Quickcheck_Examples Specialisation_Examples IMP_1 IMP_2 (* FIXME since 21-Jul-2011 - Hotel_Example_Small_Generator + Hotel_Example_Small_Generator *) IMP_3 - IMP_4 *) + IMP_4 theories [condition = "ISABELLE_SWIPL"] Code_Prolog_Examples Context_Free_Grammar_Example diff -r 5e94dfead1c2 -r 497eb43a3064 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 09 20:57:21 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Sep 09 21:51:44 2015 +0200 @@ -26,7 +26,7 @@ val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) -> Proof.context -> Proof.context val test_goals : (Predicate_Compile_Aux.compilation * bool) -> - Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> + Proof.context -> bool -> (string * typ) list -> (term * term list) list -> Quickcheck.result list val nrandom : int Unsynchronized.ref val debug : bool Unsynchronized.ref