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