author | bulwahn |
Tue, 03 Nov 2009 10:36:20 +0100 | |
changeset 33405 | 5c1928d5db38 |
parent 33375 | fd3e861f8d31 |
child 33475 | 42fed8eac357 |
permissions | -rw-r--r-- |
33257 | 1 |
theory Predicate_Compile_Quickcheck_ex |
2 |
imports Predicate_Compile_Quickcheck |
|
3 |
Predicate_Compile_Alternative_Defs |
|
4 |
begin |
|
5 |
||
6 |
section {* Sets *} |
|
7 |
||
33405
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
8 |
lemma "x \<in> {(1::nat)} ==> False" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
9 |
quickcheck[generator=predicate_compile] |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
10 |
oops |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
11 |
|
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
12 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
13 |
oops |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
14 |
|
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
15 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
16 |
quickcheck[generator=predicate_compile] |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
17 |
oops |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
18 |
|
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
19 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
20 |
quickcheck[generator=predicate_compile] |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
21 |
oops |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
22 |
|
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
23 |
section {* Numerals *} |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
24 |
|
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
25 |
lemma |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
26 |
"x \<in> {1, 2, (3::nat)} ==> x < 3" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
27 |
(*quickcheck[generator=predicate_compile]*) |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
28 |
oops |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
29 |
lemma |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
30 |
"x \<in> {1, 2} \<union> {3, 4} ==> x > 4" |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
31 |
(*quickcheck[generator=predicate_compile]*) |
5c1928d5db38
adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
bulwahn
parents:
33375
diff
changeset
|
32 |
oops |
33257 | 33 |
|
34 |
section {* Context Free Grammar *} |
|
35 |
||
36 |
datatype alphabet = a | b |
|
37 |
||
38 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
|
39 |
"[] \<in> S\<^isub>1" |
|
40 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
41 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
|
42 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
|
43 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
44 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
|
45 |
||
46 |
theorem S\<^isub>1_sound: |
|
47 |
"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
48 |
(*quickcheck[generator=predicate_compile, size=15]*) |
|
49 |
oops |
|
50 |
||
51 |
||
52 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
|
53 |
"[] \<in> S\<^isub>2" |
|
54 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
|
55 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
|
56 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
|
57 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
|
58 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
|
59 |
||
33375 | 60 |
code_pred [inductify, random] S\<^isub>2 . |
61 |
thm S\<^isub>2.random_equation |
|
62 |
thm A\<^isub>2.random_equation |
|
63 |
thm B\<^isub>2.random_equation |
|
33257 | 64 |
|
65 |
values [random] 10 "{x. S\<^isub>2 x}" |
|
66 |
||
67 |
lemma "w \<in> S\<^isub>2 ==> w \<noteq> [] ==> w \<noteq> [b, a] ==> w \<in> {}" |
|
68 |
quickcheck[generator=predicate_compile] |
|
69 |
oops |
|
70 |
||
71 |
lemma "[x <- w. x = a] = []" |
|
72 |
quickcheck[generator=predicate_compile] |
|
73 |
oops |
|
74 |
||
75 |
||
76 |
lemma "length ([x \<leftarrow> w. x = a]) = (0::nat)" |
|
77 |
(*quickcheck[generator=predicate_compile]*) |
|
78 |
oops |
|
79 |
||
80 |
||
81 |
||
82 |
lemma |
|
83 |
"w \<in> S\<^isub>2 ==> length [x \<leftarrow> w. x = a] < Suc (Suc 0)" |
|
84 |
(*quickcheck[generator=predicate_compile]*) |
|
85 |
oops |
|
86 |
||
87 |
||
88 |
theorem S\<^isub>2_sound: |
|
89 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
90 |
(*quickcheck[generator=predicate_compile, size=15, iterations=100]*) |
|
91 |
oops |
|
92 |
||
93 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
|
94 |
"[] \<in> S\<^isub>3" |
|
95 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
|
96 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
|
97 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
|
98 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
|
99 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
|
100 |
||
101 |
code_pred [inductify] S\<^isub>3 . |
|
102 |
thm S\<^isub>3.equation |
|
103 |
||
104 |
values 10 "{x. S\<^isub>3 x}" |
|
105 |
||
106 |
lemma S\<^isub>3_sound: |
|
107 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
108 |
(*quickcheck[generator=predicate_compile, size=10, iterations=1]*) |
|
109 |
oops |
|
110 |
||
111 |
||
112 |
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])" |
|
113 |
(*quickcheck[size=10, generator = pred_compile]*) |
|
114 |
oops |
|
115 |
||
116 |
theorem S\<^isub>3_complete: |
|
117 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3" |
|
118 |
(*quickcheck[generator=SML]*) |
|
119 |
(*quickcheck[generator=predicate_compile, size=10, iterations=100]*) |
|
120 |
oops |
|
121 |
||
122 |
||
123 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
|
124 |
"[] \<in> S\<^isub>4" |
|
125 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
|
126 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
|
127 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
|
128 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
|
129 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
|
130 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
|
131 |
||
132 |
theorem S\<^isub>4_sound: |
|
133 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
134 |
(*quickcheck[generator = predicate_compile, size=2, iterations=1]*) |
|
135 |
oops |
|
136 |
||
137 |
theorem S\<^isub>4_complete: |
|
138 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4" |
|
139 |
(*quickcheck[generator = pred_compile, size=5, iterations=1]*) |
|
140 |
oops |
|
141 |
||
142 |
||
143 |
end |