adding further example for quickcheck with prolog code generation
authorbulwahn
Tue Aug 31 15:07:51 2010 +0200 (2010-08-31)
changeset 389623917c2acaec4
parent 38961 8c2f59171647
child 38963 b5d126d7be4b
adding further example for quickcheck with prolog code generation
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Aug 31 15:07:51 2010 +0200
     1.3 @@ -0,0 +1,169 @@
     1.4 +theory Context_Free_Grammar_Example
     1.5 +imports Code_Prolog
     1.6 +begin
     1.7 +
     1.8 +declare mem_def[code_pred_inline]
     1.9 +
    1.10 +
    1.11 +subsection {* Alternative rules for length *}
    1.12 +
    1.13 +definition size_list :: "'a list => nat"
    1.14 +where "size_list = size"
    1.15 +
    1.16 +lemma size_list_simps:
    1.17 +  "size_list [] = 0"
    1.18 +  "size_list (x # xs) = Suc (size_list xs)"
    1.19 +by (auto simp add: size_list_def)
    1.20 +
    1.21 +declare size_list_simps[code_pred_def]
    1.22 +declare size_list_def[symmetric, code_pred_inline]
    1.23 +
    1.24 +
    1.25 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    1.26 +
    1.27 +datatype alphabet = a | b
    1.28 +
    1.29 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
    1.30 +  "[] \<in> S\<^isub>1"
    1.31 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    1.32 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
    1.33 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
    1.34 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    1.35 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    1.36 +
    1.37 +lemma
    1.38 +  "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
    1.39 +quickcheck[generator = prolog, iterations=1, expect = counterexample]
    1.40 +oops
    1.41 +
    1.42 +definition "filter_a = filter (\<lambda>x. x = a)"
    1.43 +
    1.44 +lemma [code_pred_def]: "filter_a [] = []"
    1.45 +unfolding filter_a_def by simp
    1.46 +
    1.47 +lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
    1.48 +unfolding filter_a_def by simp
    1.49 +
    1.50 +declare filter_a_def[symmetric, code_pred_inline]
    1.51 +
    1.52 +definition "filter_b = filter (\<lambda>x. x = b)"
    1.53 +
    1.54 +lemma [code_pred_def]: "filter_b [] = []"
    1.55 +unfolding filter_b_def by simp
    1.56 +
    1.57 +lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
    1.58 +unfolding filter_b_def by simp
    1.59 +
    1.60 +declare filter_b_def[symmetric, code_pred_inline]
    1.61 +
    1.62 +setup {* Code_Prolog.map_code_options (K
    1.63 +  {ensure_groundness = true,
    1.64 +  limited_types = [],
    1.65 +  limited_predicates = [(["s1", "a1", "b1"], 2)],
    1.66 +  replacing = [(("s1", "limited_s1"), "quickcheck")],
    1.67 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.68 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.69 +
    1.70 +
    1.71 +theorem S\<^isub>1_sound:
    1.72 +"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.73 +quickcheck[generator = prolog, iterations=1, expect = counterexample]
    1.74 +oops
    1.75 +
    1.76 +
    1.77 +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
    1.78 +  "[] \<in> S\<^isub>2"
    1.79 +| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
    1.80 +| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
    1.81 +| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
    1.82 +| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
    1.83 +| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    1.84 +
    1.85 +
    1.86 +setup {* Code_Prolog.map_code_options (K
    1.87 +  {ensure_groundness = true,
    1.88 +  limited_types = [],
    1.89 +  limited_predicates = [(["s2", "a2", "b2"], 3)],
    1.90 +  replacing = [(("s2", "limited_s2"), "quickcheck")],
    1.91 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    1.92 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.93 +
    1.94 +
    1.95 +theorem S\<^isub>2_sound:
    1.96 +"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    1.97 +quickcheck[generator=prolog, iterations=1, expect = counterexample]
    1.98 +oops
    1.99 +
   1.100 +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   1.101 +  "[] \<in> S\<^isub>3"
   1.102 +| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   1.103 +| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   1.104 +| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   1.105 +| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   1.106 +| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   1.107 +
   1.108 +
   1.109 +setup {* Code_Prolog.map_code_options (K
   1.110 +  {ensure_groundness = true,
   1.111 +  limited_types = [],
   1.112 +  limited_predicates = [(["s3", "a3", "b3"], 6)],
   1.113 +  replacing = [(("s3", "limited_s3"), "quickcheck")],
   1.114 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   1.115 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
   1.116 +
   1.117 +lemma S\<^isub>3_sound:
   1.118 +"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   1.119 +quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
   1.120 +oops
   1.121 +
   1.122 +
   1.123 +(*
   1.124 +setup {* Code_Prolog.map_code_options (K
   1.125 +  {ensure_groundness = true,
   1.126 +  limited_types = [],
   1.127 +  limited_predicates = [],
   1.128 +  replacing = [],
   1.129 +  manual_reorder = [],
   1.130 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
   1.131 +
   1.132 +
   1.133 +theorem S\<^isub>3_complete:
   1.134 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   1.135 +quickcheck[generator = prolog, size=1, iterations=1]
   1.136 +oops
   1.137 +*)
   1.138 +
   1.139 +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   1.140 +  "[] \<in> S\<^isub>4"
   1.141 +| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   1.142 +| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   1.143 +| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   1.144 +| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   1.145 +| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   1.146 +| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   1.147 +
   1.148 +
   1.149 +setup {* Code_Prolog.map_code_options (K
   1.150 +  {ensure_groundness = true,
   1.151 +  limited_types = [],
   1.152 +  limited_predicates = [(["s4", "a4", "b4"], 6)],
   1.153 +  replacing = [(("s4", "limited_s4"), "quickcheck")],
   1.154 +  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   1.155 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
   1.156 +
   1.157 +
   1.158 +theorem S\<^isub>4_sound:
   1.159 +"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   1.160 +quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
   1.161 +oops
   1.162 +
   1.163 +(*
   1.164 +theorem S\<^isub>4_complete:
   1.165 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   1.166 +oops
   1.167 +*)
   1.168 +
   1.169 +hide_const a b
   1.170 +
   1.171 +
   1.172 +end
   1.173 \ No newline at end of file