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