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