author | blanchet |
Thu, 18 Feb 2010 18:48:07 +0100 | |
changeset 35220 | 2bcdae5f4fdb |
parent 34948 | 2d5f2a9f7601 |
child 35324 | c9f428269b38 |
permissions | -rw-r--r-- |
33257 | 1 |
theory Predicate_Compile_Quickcheck_ex |
2 |
imports Predicate_Compile_Quickcheck |
|
3 |
Predicate_Compile_Alternative_Defs |
|
4 |
begin |
|
5 |
||
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
6 |
ML {* Predicate_Compile_Alternative_Defs.get *} |
33257 | 7 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
8 |
section {* Sets *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
9 |
(* |
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
|
10 |
lemma "x \<in> {(1::nat)} ==> False" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
11 |
quickcheck[generator=predicate_compile, iterations=10] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
12 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
13 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
14 |
(* TODO: some error with doubled negation *) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
15 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
16 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0" |
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
|
17 |
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
|
18 |
oops |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
19 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
20 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
21 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
22 |
quickcheck[generator=predicate_compile] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
23 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
24 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
25 |
lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
26 |
(*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
|
27 |
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
|
28 |
|
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 |
section {* Numerals *} |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
30 |
(* |
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
|
31 |
lemma |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
32 |
"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
|
33 |
quickcheck[generator=predicate_compile] |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
34 |
oops |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
35 |
*) |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
36 |
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
|
37 |
(*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
|
38 |
oops |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
39 |
|
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
|
40 |
lemma |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33405
diff
changeset
|
41 |
"x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
42 |
(*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
|
43 |
oops |
33257 | 44 |
|
45 |
section {* Context Free Grammar *} |
|
46 |
||
47 |
datatype alphabet = a | b |
|
48 |
||
49 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
|
50 |
"[] \<in> S\<^isub>1" |
|
51 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
52 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
|
53 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
|
54 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
|
55 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
56 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
57 |
code_pred [random_dseq inductify] "S\<^isub>1p" . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
58 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
59 |
(*thm B\<^isub>1p.random_dseq_equation*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
60 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
61 |
values [random_dseq 2, 2, 4] 10 "{x. S\<^isub>1p x}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
62 |
values [random_dseq 1, 1, 5] 20 "{x. S\<^isub>1p x}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
63 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
64 |
ML {* set ML_Context.trace *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
65 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
66 |
ML {* set Toplevel.debug *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
67 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
68 |
quickcheck[generator = predicate_compile, size = 10, iterations = 1] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
69 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
70 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
71 |
ML {* Spec_Rules.get *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
72 |
ML {* Item_Net.retrieve *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
73 |
local_setup {* Local_Theory.checkpoint *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
74 |
ML {* Predicate_Compile_Data.get_specification @{theory} @{term "append"} *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
75 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
76 |
"w \<in> S\<^isub>1p \<Longrightarrow> w = []" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
77 |
quickcheck[generator = predicate_compile, iterations=1] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
78 |
oops |
33257 | 79 |
|
80 |
theorem S\<^isub>1_sound: |
|
81 |
"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
82 |
quickcheck[generator=predicate_compile, size=15] |
33257 | 83 |
oops |
84 |
||
85 |
||
86 |
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where |
|
87 |
"[] \<in> S\<^isub>2" |
|
88 |
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2" |
|
89 |
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2" |
|
90 |
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2" |
|
91 |
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2" |
|
92 |
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2" |
|
93 |
||
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
94 |
code_pred [random_dseq inductify] S\<^isub>2 . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
95 |
thm S\<^isub>2.random_dseq_equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
96 |
thm A\<^isub>2.random_dseq_equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
97 |
thm B\<^isub>2.random_dseq_equation |
33257 | 98 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
99 |
values [random_dseq 1, 2, 8] 10 "{x. S\<^isub>2 x}" |
33257 | 100 |
|
101 |
lemma "w \<in> S\<^isub>2 ==> w \<noteq> [] ==> w \<noteq> [b, a] ==> w \<in> {}" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
102 |
quickcheck[generator=predicate_compile, size=8] |
33257 | 103 |
oops |
104 |
||
105 |
lemma "[x <- w. x = a] = []" |
|
106 |
quickcheck[generator=predicate_compile] |
|
107 |
oops |
|
108 |
||
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
109 |
declare list.size(3,4)[code_pred_def] |
33257 | 110 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
111 |
(* |
33257 | 112 |
lemma "length ([x \<leftarrow> w. x = a]) = (0::nat)" |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
113 |
quickcheck[generator=predicate_compile] |
33257 | 114 |
oops |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
115 |
*) |
33257 | 116 |
|
117 |
lemma |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
118 |
"w \<in> S\<^isub>2 ==> length [x \<leftarrow> w. x = a] <= Suc (Suc 0)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
119 |
quickcheck[generator=predicate_compile, size = 10, iterations = 1] |
33257 | 120 |
oops |
121 |
||
122 |
theorem S\<^isub>2_sound: |
|
123 |
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
124 |
quickcheck[generator=predicate_compile, size=15, iterations=1] |
33257 | 125 |
oops |
126 |
||
127 |
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where |
|
128 |
"[] \<in> S\<^isub>3" |
|
129 |
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3" |
|
130 |
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3" |
|
131 |
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3" |
|
132 |
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3" |
|
133 |
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3" |
|
134 |
||
135 |
code_pred [inductify] S\<^isub>3 . |
|
136 |
thm S\<^isub>3.equation |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
137 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
138 |
values 10 "{x. S\<^isub>3 x}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
139 |
*) |
33257 | 140 |
|
141 |
||
142 |
lemma S\<^isub>3_sound: |
|
143 |
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
144 |
quickcheck[generator=predicate_compile, size=10, iterations=10] |
33257 | 145 |
oops |
146 |
||
147 |
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
148 |
quickcheck[size=10, generator = predicate_compile] |
33257 | 149 |
oops |
150 |
||
151 |
theorem S\<^isub>3_complete: |
|
152 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3" |
|
153 |
(*quickcheck[generator=SML]*) |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
154 |
quickcheck[generator=predicate_compile, size=10, iterations=100] |
33257 | 155 |
oops |
156 |
||
157 |
||
158 |
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where |
|
159 |
"[] \<in> S\<^isub>4" |
|
160 |
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4" |
|
161 |
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4" |
|
162 |
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4" |
|
163 |
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4" |
|
164 |
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4" |
|
165 |
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4" |
|
166 |
||
167 |
theorem S\<^isub>4_sound: |
|
168 |
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
169 |
quickcheck[generator = predicate_compile, size=5, iterations=1] |
33257 | 170 |
oops |
171 |
||
172 |
theorem S\<^isub>4_complete: |
|
173 |
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4" |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
174 |
quickcheck[generator = predicate_compile, size=5, iterations=1] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
175 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
176 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
177 |
hide const b |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
178 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
179 |
subsection {* Lexicographic order *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
180 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
181 |
"(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
182 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
183 |
subsection {* IMP *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
184 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
185 |
types |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
186 |
var = nat |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
187 |
state = "int list" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
188 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
189 |
datatype com = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
190 |
Skip | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
191 |
Ass var "int" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
192 |
Seq com com | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
193 |
IF "state list" com com | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
194 |
While "state list" com |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
195 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
196 |
inductive exec :: "com => state => state => bool" where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
197 |
"exec Skip s s" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
198 |
"exec (Ass x e) s (s[x := e])" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
199 |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
200 |
"s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
201 |
"s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
202 |
"s \<notin> set b ==> exec (While b c) s s" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
203 |
"s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
204 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
205 |
code_pred [random_dseq] exec . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
206 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
207 |
values [random_dseq 1, 2, 3] 10 "{(c, s, s'). exec c s s'}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
208 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
209 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
210 |
"exec c s s' ==> exec (Seq c c) s s'" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
211 |
quickcheck[generator = predicate_compile, size=3, iterations=1] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
212 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
213 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
214 |
subsection {* Lambda *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
215 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
216 |
datatype type = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
217 |
Atom nat |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
218 |
| Fun type type (infixr "\<Rightarrow>" 200) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
219 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
220 |
datatype dB = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
221 |
Var nat |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
222 |
| App dB dB (infixl "\<degree>" 200) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
223 |
| Abs type dB |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
224 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
225 |
primrec |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
226 |
nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
227 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
228 |
"[]\<langle>i\<rangle> = None" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
229 |
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
230 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
231 |
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
232 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
233 |
"nth_el' (x # xs) 0 x" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
234 |
| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
235 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
236 |
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
237 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
238 |
Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
239 |
| Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
240 |
| App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
241 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
242 |
primrec |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
243 |
lift :: "[dB, nat] => dB" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
244 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
245 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
246 |
| "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
247 |
| "lift (Abs T s) k = Abs T (lift s (k + 1))" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
248 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
249 |
primrec |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
250 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
251 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
252 |
subst_Var: "(Var i)[s/k] = |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
253 |
(if k < i then Var (i - 1) else if i = k then s else Var i)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
254 |
| subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
255 |
| subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
256 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
257 |
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
258 |
where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
259 |
beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
260 |
| appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
261 |
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
262 |
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
263 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
264 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
265 |
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
266 |
quickcheck[generator = predicate_compile, size = 7, iterations = 10] |
33257 | 267 |
oops |
268 |
||
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
269 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
270 |
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
271 |
thm typing.equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
272 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
273 |
code_pred (modes: i => i => bool, i => o => bool as reduce') beta . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
274 |
thm beta.equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
275 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
276 |
values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
277 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
278 |
definition "reduce t = Predicate.the (reduce' t)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
279 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
280 |
value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
281 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
282 |
code_pred [random] typing . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
283 |
code_pred [random_dseq] typing . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
284 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
285 |
(*values [random] 1 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
286 |
*)*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
287 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
288 |
subsection {* JAD *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
289 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
290 |
definition matrix :: "('a :: semiring_0) list list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
291 |
"matrix M rs cs \<longleftrightarrow> (\<forall> row \<in> set M. length row = cs) \<and> length M = rs" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
292 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
293 |
code_pred [random_dseq inductify] matrix . |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
294 |
thm matrix.random_dseq_equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
295 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
296 |
thm matrix_aux.random_dseq_equation |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
297 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
298 |
values [random_dseq 3, 2] 10 "{(M, rs, cs). matrix (M:: int list list) rs cs}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
299 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
300 |
lemma [code_pred_intro]: |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
301 |
"matrix [] 0 m" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
302 |
"matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
303 |
sorry |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
304 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
305 |
code_pred [random_dseq inductify] matrix sorry |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
306 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
307 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
308 |
values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
309 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
310 |
definition "scalar_product v w = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
311 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
312 |
definition mv :: "('a \<Colon> semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
313 |
where [simp]: "mv M v = map (scalar_product v) M" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
314 |
text {* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
315 |
This defines the matrix vector multiplication. To work properly @{term |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
316 |
"matrix M m n \<and> length v = n"} must hold. |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
317 |
*} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
318 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
319 |
subsection "Compressed matrix" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
320 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
321 |
definition "sparsify xs = [i \<leftarrow> zip [0..<length xs] xs. snd i \<noteq> 0]" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
322 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
323 |
lemma sparsify_length: "(i, x) \<in> set (sparsify xs) \<Longrightarrow> i < length xs" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
324 |
by (auto simp: sparsify_def set_zip) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
325 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
326 |
lemma listsum_sparsify[simp]: |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
327 |
fixes v :: "('a \<Colon> semiring_0) list" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
328 |
assumes "length w = length v" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
329 |
shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
330 |
(is "(\<Sum>x\<leftarrow>_. ?f x) = _") |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
331 |
unfolding sparsify_def scalar_product_def |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
332 |
using assms listsum_map_filter[where f="?f" and P="\<lambda> i. snd i \<noteq> (0::'a)"] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
333 |
by (simp add: listsum_setsum) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
334 |
*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
335 |
definition [simp]: "unzip w = (map fst w, map snd w)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
336 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
337 |
primrec insert :: "('a \<Rightarrow> 'b \<Colon> linorder) => 'a \<Rightarrow> 'a list => 'a list" where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
338 |
"insert f x [] = [x]" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
339 |
"insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
340 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
341 |
primrec sort :: "('a \<Rightarrow> 'b \<Colon> linorder) \<Rightarrow> 'a list => 'a list" where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
342 |
"sort f [] = []" | |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
343 |
"sort f (x # xs) = insert f x (sort f xs)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
344 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
345 |
definition |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
346 |
"length_permutate M = (unzip o sort (length o snd)) (zip [0 ..< length M] M)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
347 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
348 |
definition |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
349 |
"transpose M = [map (\<lambda> xs. xs ! i) (takeWhile (\<lambda> xs. i < length xs) M). i \<leftarrow> [0 ..< length (M ! 0)]]" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
350 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
351 |
definition |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
352 |
"inflate upds = foldr (\<lambda> (i, x) upds. upds[i := x]) upds (replicate (length upds) 0)" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
353 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
354 |
definition |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
355 |
"jad = apsnd transpose o length_permutate o map sparsify" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
356 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
357 |
definition |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
358 |
"jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
359 |
ML {* ML_Context.trace := false *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
360 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
361 |
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
362 |
quickcheck[generator = predicate_compile, size = 6] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
363 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
364 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
365 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
366 |
"\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
367 |
(*quickcheck[generator = predicate_compile]*) |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33475
diff
changeset
|
368 |
oops |
33257 | 369 |
|
370 |
end |