1.1 --- a/src/HOL/IsaMakefile Tue Sep 07 11:51:53 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Sep 07 11:51:53 2010 +0200
1.3 @@ -1332,7 +1332,8 @@
1.4 Predicate_Compile_Examples/IMP_3.thy \
1.5 Predicate_Compile_Examples/IMP_4.thy \
1.6 Predicate_Compile_Examples/Lambda_Example.thy \
1.7 - Predicate_Compile_Examples/List_Examples.thy
1.8 + Predicate_Compile_Examples/List_Examples.thy \
1.9 + Predicate_Compile_Examples/Reg_Exp_Example.thy
1.10 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
1.11
1.12
2.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Sep 07 11:51:53 2010 +0200
2.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Sep 07 11:51:53 2010 +0200
2.3 @@ -1,2 +1,3 @@
2.4 use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
2.5 if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"];
2.6 +setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"];
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 07 11:51:53 2010 +0200
3.3 @@ -0,0 +1,184 @@
3.4 +theory RegExp_Example
3.5 +imports Predicate_Compile_Quickcheck Code_Prolog
3.6 +begin
3.7 +
3.8 +text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
3.9 +text {* The example (original in Haskell) was imported with Haskabelle and
3.10 + manually slightly adapted.
3.11 +*}
3.12 +
3.13 +datatype Nat = Zer
3.14 + | Suc Nat
3.15 +
3.16 +fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
3.17 +where
3.18 + "sub x y = (case y of
3.19 + Zer \<Rightarrow> x
3.20 + | Suc y' \<Rightarrow> case x of
3.21 + Zer \<Rightarrow> Zer
3.22 + | Suc x' \<Rightarrow> sub x' y')"
3.23 +
3.24 +datatype Sym = N0
3.25 + | N1 Sym
3.26 +
3.27 +datatype RE = Sym Sym
3.28 + | Or RE RE
3.29 + | Seq RE RE
3.30 + | And RE RE
3.31 + | Star RE
3.32 + | Empty
3.33 +
3.34 +
3.35 +function accepts :: "RE \<Rightarrow> Sym list \<Rightarrow> bool" and
3.36 + seqSplit :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
3.37 + seqSplit'' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
3.38 + seqSplit' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool"
3.39 +where
3.40 + "accepts re ss = (case re of
3.41 + Sym n \<Rightarrow> case ss of
3.42 + Nil \<Rightarrow> False
3.43 + | (n' # ss') \<Rightarrow> n = n' & List.null ss'
3.44 + | Or re1 re2 \<Rightarrow> accepts re1 ss | accepts re2 ss
3.45 + | Seq re1 re2 \<Rightarrow> seqSplit re1 re2 Nil ss
3.46 + | And re1 re2 \<Rightarrow> accepts re1 ss & accepts re2 ss
3.47 + | Star re' \<Rightarrow> case ss of
3.48 + Nil \<Rightarrow> True
3.49 + | (s # ss') \<Rightarrow> seqSplit re' re [s] ss'
3.50 + | Empty \<Rightarrow> List.null ss)"
3.51 +| "seqSplit re1 re2 ss2 ss = (seqSplit'' re1 re2 ss2 ss | seqSplit' re1 re2 ss2 ss)"
3.52 +| "seqSplit'' re1 re2 ss2 ss = (accepts re1 ss2 & accepts re2 ss)"
3.53 +| "seqSplit' re1 re2 ss2 ss = (case ss of
3.54 + Nil \<Rightarrow> False
3.55 + | (n # ss') \<Rightarrow> seqSplit re1 re2 (ss2 @ [n]) ss')"
3.56 +by pat_completeness auto
3.57 +
3.58 +termination
3.59 + sorry
3.60 +
3.61 +fun rep :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
3.62 +where
3.63 + "rep n re = (case n of
3.64 + Zer \<Rightarrow> Empty
3.65 + | Suc n' \<Rightarrow> Seq re (rep n' re))"
3.66 +
3.67 +
3.68 +fun repMax :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
3.69 +where
3.70 + "repMax n re = (case n of
3.71 + Zer \<Rightarrow> Empty
3.72 + | Suc n' \<Rightarrow> Or (rep n re) (repMax n' re))"
3.73 +
3.74 +
3.75 +fun repInt' :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
3.76 +where
3.77 + "repInt' n k re = (case k of
3.78 + Zer \<Rightarrow> rep n re
3.79 + | Suc k' \<Rightarrow> Or (rep n re) (repInt' (Suc n) k' re))"
3.80 +
3.81 +
3.82 +fun repInt :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
3.83 +where
3.84 + "repInt n k re = repInt' n (sub k n) re"
3.85 +
3.86 +
3.87 +fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
3.88 +where
3.89 + "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))"
3.90 +
3.91 +
3.92 +
3.93 +lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
3.94 +(*nitpick
3.95 +quickcheck[generator = code, iterations = 10000]
3.96 +quickcheck[generator = predicate_compile_wo_ff]
3.97 +quickcheck[generator = predicate_compile_ff_fs]
3.98 +oops*)
3.99 +oops
3.100 +
3.101 +
3.102 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
3.103 +
3.104 +setup {* Code_Prolog.map_code_options (K
3.105 + {ensure_groundness = true,
3.106 + limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
3.107 + limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
3.108 + (["accepts", "acceptsaux", "acceptsauxauxa", "acceptsauxaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
3.109 + replacing =
3.110 + [(("repP", "limited_repP"), "lim_repIntPa"),
3.111 + (("subP", "limited_subP"), "repIntP"),
3.112 + (("repIntPa", "limited_repIntPa"), "repIntP"),
3.113 + (("accepts", "limited_accepts"), "quickcheck")],
3.114 + manual_reorder = [],
3.115 + timeout = Time.fromSeconds 10,
3.116 + prolog_system = Code_Prolog.SWI_PROLOG}) *}
3.117 +
3.118 +text {* Finding the counterexample still seems out of reach for the
3.119 + prolog-style generation. *}
3.120 +
3.121 +lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
3.122 +quickcheck[generator = code, iterations = 100000, expect = counterexample]
3.123 +(*quickcheck[generator = predicate_compile_wo_ff]*)
3.124 +(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
3.125 +(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
3.126 +oops
3.127 +
3.128 +section {* Given a partial solution *}
3.129 +
3.130 +lemma
3.131 +(* assumes "n = Zer"
3.132 + assumes "k = Suc (Suc Zer)"*)
3.133 + assumes "p = Sym N0"
3.134 + assumes "q = Seq (Sym N0) (Sym N0)"
3.135 +(* assumes "s = [N0, N0]"*)
3.136 + shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
3.137 +(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*)
3.138 +quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
3.139 +oops
3.140 +
3.141 +section {* Checking the counterexample *}
3.142 +
3.143 +definition a_sol
3.144 +where
3.145 + "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"
3.146 +
3.147 +lemma
3.148 + assumes "n = Zer"
3.149 + assumes "k = Suc (Suc Zer)"
3.150 + assumes "p = Sym N0"
3.151 + assumes "q = Seq (Sym N0) (Sym N0)"
3.152 + assumes "s = [N0, N0]"
3.153 + shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
3.154 +(*quickcheck[generator = predicate_compile_wo_ff]*)
3.155 +oops
3.156 +
3.157 +lemma
3.158 + assumes "n = Zer"
3.159 + assumes "k = Suc (Suc Zer)"
3.160 + assumes "p = Sym N0"
3.161 + assumes "q = Seq (Sym N0) (Sym N0)"
3.162 + assumes "s = [N0, N0]"
3.163 + shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
3.164 +quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
3.165 +quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
3.166 +oops
3.167 +
3.168 +lemma
3.169 + assumes "n = Zer"
3.170 + assumes "k = Suc (Suc Zer)"
3.171 + assumes "p = Sym N0"
3.172 + assumes "q = Seq (Sym N0) (Sym N0)"
3.173 + assumes "s = [N0, N0]"
3.174 +shows "prop_regex (n, (k, (p, (q, s))))"
3.175 +quickcheck[generator = predicate_compile_wo_ff, expect = counterexample]
3.176 +quickcheck[generator = prolog, expect = counterexample]
3.177 +oops
3.178 +
3.179 +lemma "prop_regex a_sol"
3.180 +quickcheck[generator = code, expect = counterexample]
3.181 +quickcheck[generator = predicate_compile_ff_fs, expect = counterexample]
3.182 +oops
3.183 +
3.184 +value [code] "prop_regex a_sol"
3.185 +
3.186 +
3.187 +end