| author | bulwahn |
| Fri, 22 Oct 2010 18:38:59 +0200 | |
| changeset 40104 | 82873a6f2b81 |
| child 40137 | 9eabcb1bfe50 |
| permissions | -rw-r--r-- |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
1 |
theory Hotel_Example_Small_Generator |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
2 |
imports Hotel_Example Predicate_Compile_Alternative_Defs |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
3 |
uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
4 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
5 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
6 |
declare Let_def[code_pred_inline] |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
7 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
8 |
instantiation room :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
9 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
10 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
11 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
12 |
"small_lazy i = Lazy_Sequence.single Room0" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
13 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
14 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
15 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
16 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
17 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
18 |
instantiation key :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
19 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
20 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
21 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
22 |
"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Key0) (Lazy_Sequence.append (Lazy_Sequence.single Key1) (Lazy_Sequence.append (Lazy_Sequence.single Key2) (Lazy_Sequence.single Key3)))" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
23 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
24 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
25 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
26 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
27 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
28 |
instantiation guest :: small_lazy |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
29 |
begin |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
30 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
31 |
definition |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
32 |
"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
33 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
34 |
instance .. |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
35 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
36 |
end |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
37 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
38 |
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
39 |
Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *} |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
40 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
41 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
42 |
setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
43 |
Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *} |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
44 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
45 |
lemma |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
46 |
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g" |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
47 |
quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample] |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
48 |
quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample] |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
49 |
oops |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
50 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
51 |
|
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
diff
changeset
|
52 |
end |