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