diff -r 1d26c4006c14 -r cd6558ed65d7 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,184 @@
+theory RegExp_Example
+imports Predicate_Compile_Quickcheck Code_Prolog
+begin
+
+text {* An example from the experiments from SmallCheck (http://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 \<Rightarrow> Nat \<Rightarrow> Nat"
+where
+  "sub x y = (case y of
+                 Zer \<Rightarrow> x
+               | Suc y' \<Rightarrow> case x of
+                                         Zer \<Rightarrow> Zer
+                                       | Suc x' \<Rightarrow> 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 \<Rightarrow> Sym list \<Rightarrow> bool" and 
+    seqSplit :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and 
+    seqSplit'' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and 
+    seqSplit' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool"
+where
+  "accepts re ss = (case re of
+                       Sym n \<Rightarrow> case ss of
+                                              Nil \<Rightarrow> False
+                                            | (n' # ss') \<Rightarrow> n = n' & List.null ss'
+                     | Or re1 re2 \<Rightarrow> accepts re1 ss | accepts re2 ss
+                     | Seq re1 re2 \<Rightarrow> seqSplit re1 re2 Nil ss
+                     | And re1 re2 \<Rightarrow> accepts re1 ss & accepts re2 ss
+                     | Star re' \<Rightarrow> case ss of
+                                                 Nil \<Rightarrow> True
+                                               | (s # ss') \<Rightarrow> seqSplit re' re [s] ss'
+                     | Empty \<Rightarrow> 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 \<Rightarrow> False
+                                | (n # ss') \<Rightarrow> seqSplit re1 re2 (ss2 @ [n]) ss')"
+by pat_completeness auto
+
+termination
+  sorry
+ 
+fun rep :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+  "rep n re = (case n of
+                  Zer \<Rightarrow> Empty
+                | Suc n' \<Rightarrow> Seq re (rep n' re))"
+
+ 
+fun repMax :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+  "repMax n re = (case n of
+                     Zer \<Rightarrow> Empty
+                   | Suc n' \<Rightarrow> Or (rep n re) (repMax n' re))"
+
+ 
+fun repInt' :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+  "repInt' n k re = (case k of
+                        Zer \<Rightarrow> rep n re
+                      | Suc k' \<Rightarrow> Or (rep n re) (repInt' (Suc n) k' re))"
+
+ 
+fun repInt :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+  "repInt n k re = repInt' n (sub k n) re"
+
+ 
+fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> 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[generator = code, iterations = 10000]
+quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[generator = predicate_compile_ff_fs]
+oops*)
+oops
+
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K 
+  {ensure_groundness = true,
+   limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
+   limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
+    (["accepts", "acceptsaux", "acceptsauxauxa", "acceptsauxaux", "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 = [],
+   timeout = Time.fromSeconds 10,
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+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[generator = code, iterations = 100000, expect = counterexample]
+(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[generator = 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[generator = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+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[generator = 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[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+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[generator = predicate_compile_wo_ff, expect = counterexample]
+quickcheck[generator = prolog, expect = counterexample]
+oops
+
+lemma "prop_regex a_sol"
+quickcheck[generator = code, expect = counterexample]
+quickcheck[generator = predicate_compile_ff_fs, expect = counterexample]
+oops
+
+value [code] "prop_regex a_sol"
+
+
+end