src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
author bulwahn
Tue Aug 31 15:07:51 2010 +0200 (2010-08-31)
changeset 38962 3917c2acaec4
child 39189 d183bf90dabd
permissions -rw-r--r--
adding further example for quickcheck with prolog code generation
     1 theory Context_Free_Grammar_Example
     2 imports Code_Prolog
     3 begin
     4 
     5 declare mem_def[code_pred_inline]
     6 
     7 
     8 subsection {* Alternative rules for length *}
     9 
    10 definition size_list :: "'a list => nat"
    11 where "size_list = size"
    12 
    13 lemma size_list_simps:
    14   "size_list [] = 0"
    15   "size_list (x # xs) = Suc (size_list xs)"
    16 by (auto simp add: size_list_def)
    17 
    18 declare size_list_simps[code_pred_def]
    19 declare size_list_def[symmetric, code_pred_inline]
    20 
    21 
    22 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    23 
    24 datatype alphabet = a | b
    25 
    26 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
    27   "[] \<in> S\<^isub>1"
    28 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    29 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
    30 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
    31 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    32 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    33 
    34 lemma
    35   "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
    36 quickcheck[generator = prolog, iterations=1, expect = counterexample]
    37 oops
    38 
    39 definition "filter_a = filter (\<lambda>x. x = a)"
    40 
    41 lemma [code_pred_def]: "filter_a [] = []"
    42 unfolding filter_a_def by simp
    43 
    44 lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
    45 unfolding filter_a_def by simp
    46 
    47 declare filter_a_def[symmetric, code_pred_inline]
    48 
    49 definition "filter_b = filter (\<lambda>x. x = b)"
    50 
    51 lemma [code_pred_def]: "filter_b [] = []"
    52 unfolding filter_b_def by simp
    53 
    54 lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
    55 unfolding filter_b_def by simp
    56 
    57 declare filter_b_def[symmetric, code_pred_inline]
    58 
    59 setup {* Code_Prolog.map_code_options (K
    60   {ensure_groundness = true,
    61   limited_types = [],
    62   limited_predicates = [(["s1", "a1", "b1"], 2)],
    63   replacing = [(("s1", "limited_s1"), "quickcheck")],
    64   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    65   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    66 
    67 
    68 theorem S\<^isub>1_sound:
    69 "w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    70 quickcheck[generator = prolog, iterations=1, expect = counterexample]
    71 oops
    72 
    73 
    74 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
    75   "[] \<in> S\<^isub>2"
    76 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
    77 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
    78 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
    79 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
    80 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    81 
    82 
    83 setup {* Code_Prolog.map_code_options (K
    84   {ensure_groundness = true,
    85   limited_types = [],
    86   limited_predicates = [(["s2", "a2", "b2"], 3)],
    87   replacing = [(("s2", "limited_s2"), "quickcheck")],
    88   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    89   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    90 
    91 
    92 theorem S\<^isub>2_sound:
    93 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    94 quickcheck[generator=prolog, iterations=1, expect = counterexample]
    95 oops
    96 
    97 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
    98   "[] \<in> S\<^isub>3"
    99 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   100 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   101 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   102 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   103 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   104 
   105 
   106 setup {* Code_Prolog.map_code_options (K
   107   {ensure_groundness = true,
   108   limited_types = [],
   109   limited_predicates = [(["s3", "a3", "b3"], 6)],
   110   replacing = [(("s3", "limited_s3"), "quickcheck")],
   111   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   112   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   113 
   114 lemma S\<^isub>3_sound:
   115 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   116 quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
   117 oops
   118 
   119 
   120 (*
   121 setup {* Code_Prolog.map_code_options (K
   122   {ensure_groundness = true,
   123   limited_types = [],
   124   limited_predicates = [],
   125   replacing = [],
   126   manual_reorder = [],
   127   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   128 
   129 
   130 theorem S\<^isub>3_complete:
   131 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   132 quickcheck[generator = prolog, size=1, iterations=1]
   133 oops
   134 *)
   135 
   136 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   137   "[] \<in> S\<^isub>4"
   138 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   139 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   140 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   141 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   142 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   143 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   144 
   145 
   146 setup {* Code_Prolog.map_code_options (K
   147   {ensure_groundness = true,
   148   limited_types = [],
   149   limited_predicates = [(["s4", "a4", "b4"], 6)],
   150   replacing = [(("s4", "limited_s4"), "quickcheck")],
   151   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   152   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   153 
   154 
   155 theorem S\<^isub>4_sound:
   156 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   157 quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
   158 oops
   159 
   160 (*
   161 theorem S\<^isub>4_complete:
   162 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   163 oops
   164 *)
   165 
   166 hide_const a b
   167 
   168 
   169 end