src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
author haftmann
Sat Dec 24 15:53:10 2011 +0100 (2011-12-24)
changeset 45970 b6d0cff57d96
parent 43913 003f8c5f3e37
child 52666 391913d17d15
permissions -rw-r--r--
adjusted to set/pred distinction by means of type constructor `set`
     1 theory Context_Free_Grammar_Example
     2 imports "~~/src/HOL/Library/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_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
    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   "S\<^isub>1p w \<Longrightarrow> w = []"
    36 quickcheck[tester = 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   limit_globally = NONE,
    62   limited_types = [],
    63   limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
    64   replacing = [(("s1p", "limited_s1p"), "quickcheck")],
    65   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    66 
    67 
    68 theorem S\<^isub>1_sound:
    69 "S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    70 quickcheck[tester = 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   limit_globally = NONE,
    86   limited_types = [],
    87   limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
    88   replacing = [(("s2p", "limited_s2p"), "quickcheck")],
    89   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    90 
    91 
    92 theorem S\<^isub>2_sound:
    93   "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    94 quickcheck[tester = 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   limit_globally = NONE,
   109   limited_types = [],
   110   limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
   111   replacing = [(("s3p", "limited_s3p"), "quickcheck")],
   112   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   113 
   114 lemma S\<^isub>3_sound:
   115   "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   116 quickcheck[tester = 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   limit_globally = NONE,
   124   limited_types = [],
   125   limited_predicates = [],
   126   replacing = [],
   127   manual_reorder = [],
   128   timeout = seconds 10.0,
   129   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   130 
   131 
   132 theorem S\<^isub>3_complete:
   133 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   134 quickcheck[tester = prolog, size=1, iterations=1]
   135 oops
   136 *)
   137 
   138 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   139   "[] \<in> S\<^isub>4"
   140 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   141 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   142 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   143 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   144 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   145 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   146 
   147 
   148 setup {* Code_Prolog.map_code_options (K
   149   {ensure_groundness = true,
   150   limit_globally = NONE,
   151   limited_types = [],
   152   limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
   153   replacing = [(("s4p", "limited_s4p"), "quickcheck")],
   154   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   155 
   156 
   157 theorem S\<^isub>4_sound:
   158   "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   159 quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
   160 oops
   161 
   162 (*
   163 theorem S\<^isub>4_complete:
   164 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   165 oops
   166 *)
   167 
   168 hide_const a b
   169 
   170 
   171 end