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