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 = [(🍋‹Sym›, 0), (🍋‹Sym list›, 2), (🍋‹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