src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
author bulwahn
Tue Sep 07 11:51:53 2010 +0200 (2010-09-07)
changeset 39189 d183bf90dabd
parent 38962 3917c2acaec4
child 39463 7ce0ed8dc4d6
permissions -rw-r--r--
adapting example files
     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   timeout = Time.fromSeconds 10,
    66   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    67 
    68 
    69 theorem S\<^isub>1_sound:
    70 "w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    71 quickcheck[generator = prolog, iterations=1, expect = counterexample]
    72 oops
    73 
    74 
    75 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
    76   "[] \<in> S\<^isub>2"
    77 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
    78 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
    79 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
    80 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
    81 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    82 
    83 
    84 setup {* Code_Prolog.map_code_options (K
    85   {ensure_groundness = true,
    86   limited_types = [],
    87   limited_predicates = [(["s2", "a2", "b2"], 3)],
    88   replacing = [(("s2", "limited_s2"), "quickcheck")],
    89   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
    90   timeout = Time.fromSeconds 10,
    91   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    92 
    93 
    94 theorem S\<^isub>2_sound:
    95 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    96 quickcheck[generator=prolog, iterations=1, expect = counterexample]
    97 oops
    98 
    99 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   100   "[] \<in> S\<^isub>3"
   101 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   102 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   103 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   104 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   105 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   106 
   107 
   108 setup {* Code_Prolog.map_code_options (K
   109   {ensure_groundness = true,
   110   limited_types = [],
   111   limited_predicates = [(["s3", "a3", "b3"], 6)],
   112   replacing = [(("s3", "limited_s3"), "quickcheck")],
   113   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   114   timeout = Time.fromSeconds 10,
   115   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   116 
   117 lemma S\<^isub>3_sound:
   118 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   119 quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
   120 oops
   121 
   122 
   123 (*
   124 setup {* Code_Prolog.map_code_options (K
   125   {ensure_groundness = true,
   126   limited_types = [],
   127   limited_predicates = [],
   128   replacing = [],
   129   manual_reorder = [],
   130   timeout = Time.fromSeconds 10,
   131   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   132 
   133 
   134 theorem S\<^isub>3_complete:
   135 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   136 quickcheck[generator = prolog, size=1, iterations=1]
   137 oops
   138 *)
   139 
   140 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   141   "[] \<in> S\<^isub>4"
   142 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   143 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   144 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   145 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   146 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   147 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   148 
   149 
   150 setup {* Code_Prolog.map_code_options (K
   151   {ensure_groundness = true,
   152   limited_types = [],
   153   limited_predicates = [(["s4", "a4", "b4"], 6)],
   154   replacing = [(("s4", "limited_s4"), "quickcheck")],
   155   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
   156   timeout = Time.fromSeconds 10,
   157   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   158 
   159 
   160 theorem S\<^isub>4_sound:
   161 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   162 quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
   163 oops
   164 
   165 (*
   166 theorem S\<^isub>4_complete:
   167 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   168 oops
   169 *)
   170 
   171 hide_const a b
   172 
   173 
   174 end