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