src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
author bulwahn
Tue Jul 26 08:07:01 2011 +0200 (2011-07-26)
changeset 43974 30f4d346b204
parent 43953 3b69f057ef2e
child 45451 74515e8e6046
permissions -rw-r--r--
removing expectations from quickcheck example
bulwahn@39189
     1
theory Reg_Exp_Example
wenzelm@41956
     2
imports
wenzelm@41956
     3
  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
wenzelm@41956
     4
  "~~/src/HOL/Library/Code_Prolog"
bulwahn@39188
     5
begin
bulwahn@39188
     6
bulwahn@39188
     7
text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
bulwahn@39188
     8
text {* The example (original in Haskell) was imported with Haskabelle and
bulwahn@39188
     9
  manually slightly adapted.
bulwahn@39188
    10
*}
bulwahn@39188
    11
 
bulwahn@39188
    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
bulwahn@39188
    23
datatype Sym = N0
bulwahn@39188
    24
             | N1 Sym
bulwahn@39188
    25
bulwahn@39188
    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
bulwahn@39188
    88
  "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
bulwahn@39188
    89
bulwahn@39188
    90
bulwahn@39188
    91
bulwahn@39188
    92
lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
bulwahn@39188
    93
(*nitpick
bulwahn@40924
    94
quickcheck[tester = random, iterations = 10000]
bulwahn@40924
    95
quickcheck[tester = predicate_compile_wo_ff]
bulwahn@40924
    96
quickcheck[tester = predicate_compile_ff_fs]
bulwahn@39188
    97
oops*)
bulwahn@39188
    98
oops
bulwahn@39188
    99
bulwahn@39188
   100
bulwahn@43953
   101
setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
bulwahn@39188
   102
bulwahn@39188
   103
setup {* Code_Prolog.map_code_options (K 
bulwahn@39188
   104
  {ensure_groundness = true,
bulwahn@39800
   105
   limit_globally = NONE,
bulwahn@39188
   106
   limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
bulwahn@39188
   107
   limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
bulwahn@39725
   108
    (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
bulwahn@39188
   109
   replacing =
bulwahn@39188
   110
     [(("repP", "limited_repP"), "lim_repIntPa"),
bulwahn@39188
   111
      (("subP", "limited_subP"), "repIntP"),
bulwahn@39188
   112
      (("repIntPa", "limited_repIntPa"), "repIntP"),
bulwahn@39188
   113
      (("accepts", "limited_accepts"), "quickcheck")],  
bulwahn@39463
   114
   manual_reorder = []}) *}
bulwahn@39188
   115
bulwahn@39188
   116
text {* Finding the counterexample still seems out of reach for the
bulwahn@39188
   117
 prolog-style generation. *}
bulwahn@39188
   118
bulwahn@39188
   119
lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
bulwahn@43974
   120
quickcheck[tester = random, iterations = 100000]
bulwahn@40924
   121
(*quickcheck[tester = predicate_compile_wo_ff]*)
bulwahn@40924
   122
(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
bulwahn@40924
   123
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
bulwahn@39188
   124
oops
bulwahn@39188
   125
bulwahn@39188
   126
section {* Given a partial solution *}
bulwahn@39188
   127
bulwahn@39188
   128
lemma
bulwahn@39188
   129
(*  assumes "n = Zer"
bulwahn@39188
   130
  assumes "k = Suc (Suc Zer)"*)
bulwahn@39188
   131
  assumes "p = Sym N0"
bulwahn@39188
   132
  assumes "q = Seq (Sym N0) (Sym N0)"
bulwahn@39188
   133
(*  assumes "s = [N0, N0]"*)
bulwahn@39188
   134
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
bulwahn@40924
   135
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
bulwahn@43974
   136
quickcheck[tester = prolog, iterations = 1, size = 1]
bulwahn@39188
   137
oops
bulwahn@39188
   138
bulwahn@39188
   139
section {* Checking the counterexample *}
bulwahn@39188
   140
bulwahn@39188
   141
definition a_sol
bulwahn@39188
   142
where
bulwahn@39188
   143
  "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"
bulwahn@39188
   144
bulwahn@39188
   145
lemma 
bulwahn@39188
   146
  assumes "n = Zer"
bulwahn@39188
   147
  assumes "k = Suc (Suc Zer)"
bulwahn@39188
   148
  assumes "p = Sym N0"
bulwahn@39188
   149
  assumes "q = Seq (Sym N0) (Sym N0)"
bulwahn@39188
   150
  assumes "s = [N0, N0]"
bulwahn@39188
   151
  shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
bulwahn@40924
   152
(*quickcheck[tester = predicate_compile_wo_ff]*)
bulwahn@39188
   153
oops
bulwahn@39188
   154
bulwahn@39188
   155
lemma
bulwahn@39188
   156
  assumes "n = Zer"
bulwahn@39188
   157
  assumes "k = Suc (Suc Zer)"
bulwahn@39188
   158
  assumes "p = Sym N0"
bulwahn@39188
   159
  assumes "q = Seq (Sym N0) (Sym N0)"
bulwahn@39188
   160
  assumes "s = [N0, N0]"
bulwahn@39188
   161
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
bulwahn@40924
   162
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
bulwahn@43974
   163
quickcheck[tester = prolog, iterations = 1, size = 1]
bulwahn@39188
   164
oops
bulwahn@39188
   165
bulwahn@39188
   166
lemma
bulwahn@39188
   167
  assumes "n = Zer"
bulwahn@39188
   168
  assumes "k = Suc (Suc Zer)"
bulwahn@39188
   169
  assumes "p = Sym N0"
bulwahn@39188
   170
  assumes "q = Seq (Sym N0) (Sym N0)"
bulwahn@39188
   171
  assumes "s = [N0, N0]"
bulwahn@39188
   172
shows "prop_regex (n, (k, (p, (q, s))))"
bulwahn@40924
   173
quickcheck[tester = predicate_compile_wo_ff]
bulwahn@43974
   174
quickcheck[tester = prolog]
bulwahn@39188
   175
oops
bulwahn@39188
   176
bulwahn@39188
   177
lemma "prop_regex a_sol"
bulwahn@43974
   178
quickcheck[tester = random]
bulwahn@40924
   179
quickcheck[tester = predicate_compile_ff_fs]
bulwahn@39188
   180
oops
bulwahn@39188
   181
bulwahn@39188
   182
value [code] "prop_regex a_sol"
bulwahn@39188
   183
bulwahn@39188
   184
bulwahn@39188
   185
end