src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 68224 1f7308050349
permissions -rw-r--r--
more robust sorted_entries;
     1 theory Reg_Exp_Example
     2 imports
     3   "HOL-Library.Predicate_Compile_Quickcheck"
     4   "HOL-Library.Code_Prolog"
     5 begin
     6 
     7 text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
     8 text \<open>The example (original in Haskell) was imported with Haskabelle and
     9   manually slightly adapted.
    10 \<close>
    11  
    12 datatype Nat = Zer
    13              | Suc Nat
    14 
    15 fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
    16 where
    17   "sub x y = (case y of
    18                  Zer \<Rightarrow> x
    19                | Suc y' \<Rightarrow> case x of
    20                                          Zer \<Rightarrow> Zer
    21                                        | Suc x' \<Rightarrow> sub x' y')"
    22 
    23 datatype Sym = N0
    24              | N1 Sym
    25 
    26 datatype RE = Sym Sym
    27             | Or RE RE
    28             | Seq RE RE
    29             | And RE RE
    30             | Star RE
    31             | Empty
    32 
    33  
    34 function accepts :: "RE \<Rightarrow> Sym list \<Rightarrow> bool" and 
    35     seqSplit :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and 
    36     seqSplit'' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and 
    37     seqSplit' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool"
    38 where
    39   "accepts re ss = (case re of
    40                        Sym n \<Rightarrow> case ss of
    41                                               Nil \<Rightarrow> False
    42                                             | (n' # ss') \<Rightarrow> n = n' & List.null ss'
    43                      | Or re1 re2 \<Rightarrow> accepts re1 ss | accepts re2 ss
    44                      | Seq re1 re2 \<Rightarrow> seqSplit re1 re2 Nil ss
    45                      | And re1 re2 \<Rightarrow> accepts re1 ss & accepts re2 ss
    46                      | Star re' \<Rightarrow> case ss of
    47                                                  Nil \<Rightarrow> True
    48                                                | (s # ss') \<Rightarrow> seqSplit re' re [s] ss'
    49                      | Empty \<Rightarrow> List.null ss)"
    50 | "seqSplit re1 re2 ss2 ss = (seqSplit'' re1 re2 ss2 ss | seqSplit' re1 re2 ss2 ss)"
    51 | "seqSplit'' re1 re2 ss2 ss = (accepts re1 ss2 & accepts re2 ss)"
    52 | "seqSplit' re1 re2 ss2 ss = (case ss of
    53                                   Nil \<Rightarrow> False
    54                                 | (n # ss') \<Rightarrow> seqSplit re1 re2 (ss2 @ [n]) ss')"
    55 by pat_completeness auto
    56 
    57 termination
    58   sorry
    59  
    60 fun rep :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
    61 where
    62   "rep n re = (case n of
    63                   Zer \<Rightarrow> Empty
    64                 | Suc n' \<Rightarrow> Seq re (rep n' re))"
    65 
    66  
    67 fun repMax :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
    68 where
    69   "repMax n re = (case n of
    70                      Zer \<Rightarrow> Empty
    71                    | Suc n' \<Rightarrow> Or (rep n re) (repMax n' re))"
    72 
    73  
    74 fun repInt' :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
    75 where
    76   "repInt' n k re = (case k of
    77                         Zer \<Rightarrow> rep n re
    78                       | Suc k' \<Rightarrow> Or (rep n re) (repInt' (Suc n) k' re))"
    79 
    80  
    81 fun repInt :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
    82 where
    83   "repInt n k re = repInt' n (sub k n) re"
    84 
    85  
    86 fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
    87 where
    88   "prop_regex (n, (k, (p, (q, s)))) =
    89     ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
    90 
    91 
    92 
    93 lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
    94 (*nitpick
    95 quickcheck[tester = random, iterations = 10000]
    96 quickcheck[tester = predicate_compile_wo_ff]
    97 quickcheck[tester = predicate_compile_ff_fs]*)
    98 oops
    99 
   100 
   101 setup \<open>
   102   Context.theory_map
   103     (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
   104 \<close>
   105 
   106 setup \<open>Code_Prolog.map_code_options (K 
   107   {ensure_groundness = true,
   108    limit_globally = NONE,
   109    limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
   110    limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
   111     (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
   112    replacing =
   113      [(("repP", "limited_repP"), "lim_repIntPa"),
   114       (("subP", "limited_subP"), "repIntP"),
   115       (("repIntPa", "limited_repIntPa"), "repIntP"),
   116       (("accepts", "limited_accepts"), "quickcheck")],  
   117    manual_reorder = []})\<close>
   118 
   119 text \<open>Finding the counterexample still seems out of reach for the
   120  prolog-style generation.\<close>
   121 
   122 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
   123 quickcheck[exhaustive]
   124 quickcheck[tester = random, iterations = 1000]
   125 (*quickcheck[tester = predicate_compile_wo_ff]*)
   126 (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
   127 (*quickcheck[tester = prolog, iterations = 1, size = 1]*)
   128 oops
   129 
   130 section \<open>Given a partial solution\<close>
   131 
   132 lemma
   133 (*  assumes "n = Zer"
   134   assumes "k = Suc (Suc Zer)"*)
   135   assumes "p = Sym N0"
   136   assumes "q = Seq (Sym N0) (Sym N0)"
   137 (*  assumes "s = [N0, N0]"*)
   138   shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
   139 (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
   140 quickcheck[tester = prolog, iterations = 1, size = 1]
   141 oops
   142 
   143 section \<open>Checking the counterexample\<close>
   144 
   145 definition a_sol
   146 where
   147   "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"
   148 
   149 lemma 
   150   assumes "n = Zer"
   151   assumes "k = Suc (Suc Zer)"
   152   assumes "p = Sym N0"
   153   assumes "q = Seq (Sym N0) (Sym N0)"
   154   assumes "s = [N0, N0]"
   155   shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
   156 (*quickcheck[tester = predicate_compile_wo_ff]*)
   157 oops
   158 
   159 lemma
   160   assumes "n = Zer"
   161   assumes "k = Suc (Suc Zer)"
   162   assumes "p = Sym N0"
   163   assumes "q = Seq (Sym N0) (Sym N0)"
   164   assumes "s = [N0, N0]"
   165   shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
   166 (*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
   167 quickcheck[tester = prolog, iterations = 1, size = 1]
   168 oops
   169 
   170 lemma
   171   assumes "n = Zer"
   172   assumes "k = Suc (Suc Zer)"
   173   assumes "p = Sym N0"
   174   assumes "q = Seq (Sym N0) (Sym N0)"
   175   assumes "s = [N0, N0]"
   176 shows "prop_regex (n, (k, (p, (q, s))))"
   177 quickcheck[tester = smart_exhaustive, depth = 30]
   178 quickcheck[tester = prolog]
   179 oops
   180 
   181 lemma "prop_regex a_sol"
   182 quickcheck[tester = random]
   183 quickcheck[tester = smart_exhaustive]
   184 oops
   185 
   186 value "prop_regex a_sol"
   187 
   188 
   189 end