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