Theory Reg_Exp_Example

theory Reg_Exp_Example
  imports
    "HOL-Library.Predicate_Compile_Quickcheck"
    "HOL-Library.Code_Prolog"
  options [condition = "$ISABELLE_SWIPL", quick_and_dirty]
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