src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61424 c3658c18b7bc
child 63167 0909deb8059b
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 theory Predicate_Compile_Quickcheck_Examples
     2 imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     3 begin
     4 
     5 (*
     6 section {* Sets *}
     7 
     8 lemma "x \<in> {(1::nat)} ==> False"
     9 quickcheck[generator=predicate_compile_wo_ff, iterations=10]
    10 oops
    11 
    12 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
    13 quickcheck[generator=predicate_compile_wo_ff]
    14 oops
    15 
    16 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
    17 quickcheck[generator=predicate_compile_wo_ff]
    18 oops
    19  
    20 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
    21 quickcheck[generator=predicate_compile_wo_ff]
    22 oops
    23 
    24 section {* Numerals *}
    25 
    26 lemma
    27   "x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
    28 quickcheck[generator=predicate_compile_wo_ff]
    29 oops
    30 
    31 lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
    32 quickcheck[generator=predicate_compile_wo_ff]
    33 oops
    34 
    35 lemma
    36   "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
    37 quickcheck[generator=predicate_compile_wo_ff]
    38 oops
    39 *)
    40 
    41 section {* Equivalences *}
    42 
    43 inductive is_ten :: "nat => bool"
    44 where
    45   "is_ten 10"
    46 
    47 inductive is_eleven :: "nat => bool"
    48 where
    49   "is_eleven 11"
    50 
    51 lemma
    52   "is_ten x = is_eleven x"
    53 quickcheck[tester = smart_exhaustive, iterations = 1, size = 1, expect = counterexample]
    54 oops
    55 
    56 section {* Context Free Grammar *}
    57 
    58 datatype alphabet = a | b
    59 
    60 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
    61   "[] \<in> S\<^sub>1"
    62 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    63 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
    64 | "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
    65 | "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    66 | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
    67 
    68 lemma
    69   "S\<^sub>1p w \<Longrightarrow> w = []"
    70 quickcheck[tester = smart_exhaustive, iterations=1]
    71 oops
    72 
    73 theorem S\<^sub>1_sound:
    74 "S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    75 quickcheck[tester=smart_exhaustive, size=15]
    76 oops
    77 
    78 
    79 inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
    80   "[] \<in> S\<^sub>2"
    81 | "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
    82 | "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
    83 | "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
    84 | "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
    85 | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
    86 (*
    87 code_pred [random_dseq inductify] S\<^sub>2 .
    88 thm S\<^sub>2.random_dseq_equation
    89 thm A\<^sub>2.random_dseq_equation
    90 thm B\<^sub>2.random_dseq_equation
    91 
    92 values [random_dseq 1, 2, 8] 10 "{x. S\<^sub>2 x}"
    93 
    94 lemma "w \<in> S\<^sub>2 ==> w \<noteq> [] ==> w \<noteq> [b, a] ==> w \<in> {}"
    95 quickcheck[generator=predicate_compile, size=8]
    96 oops
    97 
    98 lemma "[x <- w. x = a] = []"
    99 quickcheck[generator=predicate_compile]
   100 oops
   101 
   102 declare list.size(3,4)[code_pred_def]
   103 
   104 (*
   105 lemma "length ([x \<leftarrow> w. x = a]) = (0::nat)"
   106 quickcheck[generator=predicate_compile]
   107 oops
   108 *)
   109 
   110 lemma
   111 "w \<in> S\<^sub>2 ==> length [x \<leftarrow> w. x = a] <= Suc (Suc 0)"
   112 quickcheck[generator=predicate_compile, size = 10, iterations = 1]
   113 oops
   114 *)
   115 theorem S\<^sub>2_sound:
   116 "S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   117 quickcheck[tester=smart_exhaustive, size=5, iterations=10]
   118 oops
   119 
   120 inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
   121   "[] \<in> S\<^sub>3"
   122 | "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
   123 | "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
   124 | "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
   125 | "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
   126 | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
   127 
   128 code_pred [inductify, skip_proof] S\<^sub>3p .
   129 thm S\<^sub>3p.equation
   130 (*
   131 values 10 "{x. S\<^sub>3 x}"
   132 *)
   133 
   134 
   135 lemma S\<^sub>3_sound:
   136 "S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   137 quickcheck[tester=smart_exhaustive, size=10, iterations=10]
   138 oops
   139 
   140 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
   141 quickcheck[size=10, tester = smart_exhaustive]
   142 oops
   143 
   144 theorem S\<^sub>3_complete:
   145 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> S\<^sub>3p w"
   146 (*quickcheck[generator=SML]*)
   147 quickcheck[tester=smart_exhaustive, size=10, iterations=100]
   148 oops
   149 
   150 
   151 inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
   152   "[] \<in> S\<^sub>4"
   153 | "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
   154 | "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
   155 | "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
   156 | "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
   157 | "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
   158 | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   159 
   160 theorem S\<^sub>4_sound:
   161 "S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   162 quickcheck[tester = smart_exhaustive, size=5, iterations=1]
   163 oops
   164 
   165 theorem S\<^sub>4_complete:
   166 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> S\<^sub>4p w"
   167 quickcheck[tester = smart_exhaustive, size=5, iterations=1]
   168 oops
   169 
   170 hide_const a b
   171 
   172 subsection {* Lexicographic order *}
   173 (* TODO *)
   174 (*
   175 lemma
   176   "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r"
   177 oops
   178 *)
   179 subsection {* IMP *}
   180 
   181 type_synonym var = nat
   182 type_synonym state = "int list"
   183 
   184 datatype com =
   185   Skip |
   186   Ass var "int" |
   187   Seq com com |
   188   IF "state list" com com |
   189   While "state list" com
   190 
   191 inductive exec :: "com => state => state => bool" where
   192   "exec Skip s s" |
   193   "exec (Ass x e) s (s[x := e])" |
   194   "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
   195   "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
   196   "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
   197   "s \<notin> set b ==> exec (While b c) s s" |
   198   "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
   199 
   200 code_pred [random_dseq] exec .
   201 
   202 values [random_dseq 1, 2, 3] 10 "{(c, s, s'). exec c s s'}"
   203 
   204 lemma
   205   "exec c s s' ==> exec (Seq c c) s s'"
   206   quickcheck[tester = smart_exhaustive, size=2, iterations=20, expect = counterexample]
   207 oops
   208 
   209 subsection {* Lambda *}
   210 
   211 datatype type =
   212     Atom nat
   213   | Fun type type    (infixr "\<Rightarrow>" 200)
   214 
   215 datatype dB =
   216     Var nat
   217   | App dB dB (infixl "\<degree>" 200)
   218   | Abs type dB
   219 
   220 primrec
   221   nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
   222 where
   223   "[]\<langle>i\<rangle> = None"
   224 | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
   225 
   226 inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
   227 where
   228   "nth_el' (x # xs) 0 x"
   229 | "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
   230 
   231 inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   232   where
   233     Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
   234   | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
   235   | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
   236 
   237 primrec
   238   lift :: "[dB, nat] => dB"
   239 where
   240     "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
   241   | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
   242   | "lift (Abs T s) k = Abs T (lift s (k + 1))"
   243 
   244 primrec
   245   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
   246 where
   247     subst_Var: "(Var i)[s/k] =
   248       (if k < i then Var (i - 1) else if i = k then s else Var i)"
   249   | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
   250   | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
   251 
   252 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   253   where
   254     beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
   255   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
   256   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
   257   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
   258 
   259 lemma
   260   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
   261 quickcheck[tester = smart_exhaustive, size = 7, iterations = 10]
   262 oops
   263 
   264 subsection {* JAD *}
   265 
   266 definition matrix :: "('a :: semiring_0) list list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   267   "matrix M rs cs \<longleftrightarrow> (\<forall> row \<in> set M. length row = cs) \<and> length M = rs"
   268 (*
   269 code_pred [random_dseq inductify] matrix .
   270 thm matrix.random_dseq_equation
   271 
   272 thm matrix_aux.random_dseq_equation
   273 
   274 values [random_dseq 3, 2] 10 "{(M, rs, cs). matrix (M:: int list list) rs cs}"
   275 *)
   276 lemma [code_pred_intro]:
   277   "matrix [] 0 m"
   278   "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
   279 proof -
   280   show "matrix [] 0 m" unfolding matrix_def by auto
   281 next
   282   show "matrix xss n m ==> length xs = m ==> matrix (xs # xss) (Suc n) m"
   283     unfolding matrix_def by auto
   284 qed
   285 
   286 code_pred [random_dseq] matrix
   287   apply (cases x)
   288   unfolding matrix_def apply fastforce
   289   apply fastforce done
   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 :: 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 :: 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 :: 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 :: 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 case_prod 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 = smart_exhaustive, 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 = smart_exhaustive]
   350 oops
   351 
   352 end