Quelle  Reg_Exp_Example.thy

theory Reg_Exp_Example
imports
  "HOL-Library.Predicate_Compile_Quickcheck"
  "HOL-Library.Code_Prolog"
begin

text ‹An example from the experiments from SmallCheck (🌐‹https://www.cs.york.ac.uk/fp/smallcheck›)›
text ‹The example (original in Haskell) was imported with Haskabelle and
 manually slightly adapted.
 ›
 
datatype Nat = Zer
             | Suc Nat

fun sub :: "Nat → Nat → Nat"
where
  "sub x y = (case y of
                 Zer → x
               | Suc y' → case x of
                                         Zer → Zer
                                       | Suc x' → sub x' y')"

datatype Sym = N0
             | N1 Sym

datatype RE = Sym Sym
            | Or RE RE
            | Seq RE RE
            | And RE RE
            | Star RE
            | Empty

 
function accepts :: "RE → Sym list → bool" and 
    seqSplit :: "RE → RE → Sym list → Sym list → bool" and 
    seqSplit'' :: "RE → RE → Sym list → Sym list → bool" and 
    seqSplit' :: "RE → RE → Sym list → Sym list → bool"
where
  "accepts re ss = (case re of
                       Sym n → case ss of
                                              Nil → False
                                            | (n' # ss') → n = n' & List.null ss'
                     | Or re1 re2 → accepts re1 ss | accepts re2 ss
                     | Seq re1 re2 → seqSplit re1 re2 Nil ss
                     | And re1 re2 → accepts re1 ss & accepts re2 ss
                     | Star re' → case ss of
                                                 Nil → True
                                               | (s # ss') → seqSplit re' re [s] ss'
                     | Empty → List.null ss)"
| "seqSplit re1 re2 ss2 ss = (seqSplit'' re1 re2 ss2 ss | seqSplit' re1 re2 ss2 ss)"
| "seqSplit'' re1 re2 ss2 ss = (accepts re1 ss2 & accepts re2 ss)"
| "seqSplit' re1 re2 ss2 ss = (case ss of
                                  Nil → False
                                | (n # ss') → seqSplit re1 re2 (ss2 @ [n]) ss')"
by pat_completeness auto

termination
  sorry
 
fun rep :: "Nat → RE → RE"
where
  "rep n re = (case n of
                  Zer → Empty
                | Suc n' → Seq re (rep n' re))"

 
fun repMax :: "Nat → RE → RE"
where
  "repMax n re = (case n of
                     Zer → Empty
                   | Suc n' → Or (rep n re) (repMax n' re))"

 
fun repInt' :: "Nat → Nat → RE → RE"
where
  "repInt' n k re = (case k of
                        Zer → rep n re
                      | Suc k' → Or (rep n re) (repInt' (Suc n) k' re))"

 
fun repInt :: "Nat → Nat → RE → RE"
where
  "repInt n k re = repInt' n (sub k n) re"

 
fun prop_regex :: "Nat * Nat * RE * RE * Sym list → bool"
where
  "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))"



lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*nitpick
quickcheck[tester = random, iterations = 10000]
quickcheck[tester = predicate_compile_wo_ff]
quickcheck[tester = predicate_compile_ff_fs]*)
oops


setup ‹
 Context.theory_map
 (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
 ›

setup ‹Code_Prolog.map_code_options (K
 {ensure_groundness = true,
 limit_globally = NONE,
 limited_types = [(typ‹Sym›, 0), (typ‹Sym list›, 2), (typ‹RE›, 6)],
 limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
 (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
 replacing =
 [(("repP", "limited_repP"), "lim_repIntPa"),
 (("subP", "limited_subP"), "repIntP"),
 (("repIntPa", "limited_repIntPa"), "repIntP"),
 (("accepts", "limited_accepts"), "quickcheck")],
 manual_reorder = []})›

text ‹Finding the counterexample still seems out of reach for the
 prolog-style generation.›

lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
quickcheck[exhaustive]
quickcheck[tester = random, iterations = 1000]
(*quickcheck[tester = predicate_compile_wo_ff]*)
(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
oops

section ‹Given a partial solution›

lemma
(*  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"*)
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
(*  assumes "s = [N0, N0]"*)
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
quickcheck[tester = prolog, iterations = 1, size = 1]
oops

section ‹Checking the counterexample›

definition a_sol
where
  "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"

lemma 
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
  shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*quickcheck[tester = predicate_compile_wo_ff]*)
oops

lemma
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
quickcheck[tester = prolog, iterations = 1, size = 1]
oops

lemma
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
quickcheck[tester = smart_exhaustive, depth = 30]
quickcheck[tester = prolog]
oops

lemma "prop_regex a_sol"
quickcheck[tester = random]
quickcheck[tester = smart_exhaustive]
oops

value "prop_regex a_sol"


end