author | bulwahn |
Fri, 06 Nov 2009 08:11:58 +0100 | |
changeset 33475 | 42fed8eac357 |
parent 33405 | 5c1928d5db38 |
child 34948 | 2d5f2a9f7601 |
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 |
|
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
12 |
(* TODO: some error with doubled negation *) |
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
|
13 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0" |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
14 |
(*quickcheck[generator=predicate_compile]*) |
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
|
15 |
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
|
16 |
|
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 |
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
|
18 |
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
|
19 |
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
|
20 |
|
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 |
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
|
22 |
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
|
23 |
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
|
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 |
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
|
26 |
|
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 |
lemma |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
28 |
"x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2" |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
29 |
quickcheck[generator=predicate_compile] |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
30 |
oops |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
31 |
|
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
32 |
lemma "x \<in> {1, 2, (3::nat)} ==> x < 3" |
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
|
33 |
(*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
|
34 |
oops |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
35 |
|
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
|
36 |
lemma |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
37 |
"x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)" |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
38 |
quickcheck[generator=predicate_compile] |
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
|
39 |
oops |
33257 | 40 |
|
41 |
section {* Context Free Grammar *} |
|
42 |
||
43 |
datatype alphabet = a | b |
|
44 |
||
45 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
|
46 |
"[] \<in> S\<^isub>1" |
|
47 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
48 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
|
49 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
|
50 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
51 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
|
52 |
||
53 |
theorem S\<^isub>1_sound: |
|
54 |
"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
55 |
(*quickcheck[generator=predicate_compile, size=15]*) |
|
56 |
oops |
|
57 |
||
58 |
||
59 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
|
60 |
"[] \<in> S\<^isub>2" |
|
61 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
|
62 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
|
63 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
|
64 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
|
65 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
|
66 |
||
33375 | 67 |
code_pred [inductify, random] S\<^isub>2 . |
68 |
thm S\<^isub>2.random_equation |
|
69 |
thm A\<^isub>2.random_equation |
|
70 |
thm B\<^isub>2.random_equation |
|
33257 | 71 |
|
72 |
values [random] 10 "{x. S\<^isub>2 x}" |
|
73 |
||
74 |
lemma "w \<in> S\<^isub>2 ==> w \<noteq> [] ==> w \<noteq> [b, a] ==> w \<in> {}" |
|
75 |
quickcheck[generator=predicate_compile] |
|
76 |
oops |
|
77 |
||
78 |
lemma "[x <- w. x = a] = []" |
|
79 |
quickcheck[generator=predicate_compile] |
|
80 |
oops |
|
81 |
||
82 |
||
83 |
lemma "length ([x \<leftarrow> w. x = a]) = (0::nat)" |
|
84 |
(*quickcheck[generator=predicate_compile]*) |
|
85 |
oops |
|
86 |
||
87 |
||
88 |
||
89 |
lemma |
|
90 |
"w \<in> S\<^isub>2 ==> length [x \<leftarrow> w. x = a] < Suc (Suc 0)" |
|
91 |
(*quickcheck[generator=predicate_compile]*) |
|
92 |
oops |
|
93 |
||
94 |
||
95 |
theorem S\<^isub>2_sound: |
|
96 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
97 |
(*quickcheck[generator=predicate_compile, size=15, iterations=100]*) |
|
98 |
oops |
|
99 |
||
100 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
|
101 |
"[] \<in> S\<^isub>3" |
|
102 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
|
103 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
|
104 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
|
105 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
|
106 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
|
107 |
||
108 |
code_pred [inductify] S\<^isub>3 . |
|
109 |
thm S\<^isub>3.equation |
|
110 |
||
111 |
values 10 "{x. S\<^isub>3 x}" |
|
112 |
||
113 |
lemma S\<^isub>3_sound: |
|
114 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
115 |
(*quickcheck[generator=predicate_compile, size=10, iterations=1]*) |
|
116 |
oops |
|
117 |
||
118 |
||
119 |
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])" |
|
120 |
(*quickcheck[size=10, generator = pred_compile]*) |
|
121 |
oops |
|
122 |
||
123 |
theorem S\<^isub>3_complete: |
|
124 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3" |
|
125 |
(*quickcheck[generator=SML]*) |
|
126 |
(*quickcheck[generator=predicate_compile, size=10, iterations=100]*) |
|
127 |
oops |
|
128 |
||
129 |
||
130 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
|
131 |
"[] \<in> S\<^isub>4" |
|
132 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
|
133 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
|
134 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
|
135 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
|
136 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
|
137 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
|
138 |
||
139 |
theorem S\<^isub>4_sound: |
|
140 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
141 |
(*quickcheck[generator = predicate_compile, size=2, iterations=1]*) |
|
142 |
oops |
|
143 |
||
144 |
theorem S\<^isub>4_complete: |
|
145 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4" |
|
146 |
(*quickcheck[generator = pred_compile, size=5, iterations=1]*) |
|
147 |
oops |
|
148 |
||
149 |
||
150 |
end |