src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
more robust sorted_entries;
     1 theory Context_Free_Grammar_Example
     2 imports "HOL-Library.Code_Prolog"
     3 begin
     4 (*
     5 declare mem_def[code_pred_inline]
     6 *)
     7 
     8 subsection \<open>Alternative rules for length\<close>
     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 \<open>
    23   Context.theory_map
    24     (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    25 \<close>
    26 
    27 datatype alphabet = a | b
    28 
    29 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
    30   "[] \<in> S\<^sub>1"
    31 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    32 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
    33 | "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
    34 | "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    35 | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
    36 
    37 lemma
    38   "S\<^sub>1p w \<Longrightarrow> w = []"
    39 quickcheck[tester = prolog, iterations=1, expect = counterexample]
    40 oops
    41 
    42 definition "filter_a = filter (\<lambda>x. x = a)"
    43 
    44 lemma [code_pred_def]: "filter_a [] = []"
    45 unfolding filter_a_def by simp
    46 
    47 lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
    48 unfolding filter_a_def by simp
    49 
    50 declare filter_a_def[symmetric, code_pred_inline]
    51 
    52 definition "filter_b = filter (\<lambda>x. x = b)"
    53 
    54 lemma [code_pred_def]: "filter_b [] = []"
    55 unfolding filter_b_def by simp
    56 
    57 lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
    58 unfolding filter_b_def by simp
    59 
    60 declare filter_b_def[symmetric, code_pred_inline]
    61 
    62 setup \<open>Code_Prolog.map_code_options (K
    63   {ensure_groundness = true,
    64   limit_globally = NONE,
    65   limited_types = [],
    66   limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
    67   replacing = [(("s1p", "limited_s1p"), "quickcheck")],
    68   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})\<close>
    69 
    70 
    71 theorem S\<^sub>1_sound:
    72 "S\<^sub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    73 quickcheck[tester = prolog, iterations=1, expect = counterexample]
    74 oops
    75 
    76 
    77 inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
    78   "[] \<in> S\<^sub>2"
    79 | "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
    80 | "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
    81 | "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
    82 | "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
    83 | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
    84 
    85 
    86 setup \<open>Code_Prolog.map_code_options (K
    87   {ensure_groundness = true,
    88   limit_globally = NONE,
    89   limited_types = [],
    90   limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
    91   replacing = [(("s2p", "limited_s2p"), "quickcheck")],
    92   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})\<close>
    93 
    94 
    95 theorem S\<^sub>2_sound:
    96   "S\<^sub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    97 quickcheck[tester = prolog, iterations=1, expect = counterexample]
    98 oops
    99 
   100 inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
   101   "[] \<in> S\<^sub>3"
   102 | "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
   103 | "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
   104 | "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
   105 | "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
   106 | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
   107 
   108 
   109 setup \<open>Code_Prolog.map_code_options (K
   110   {ensure_groundness = true,
   111   limit_globally = NONE,
   112   limited_types = [],
   113   limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
   114   replacing = [(("s3p", "limited_s3p"), "quickcheck")],
   115   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})\<close>
   116 
   117 lemma S\<^sub>3_sound:
   118   "S\<^sub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   119 quickcheck[tester = 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   limit_globally = NONE,
   127   limited_types = [],
   128   limited_predicates = [],
   129   replacing = [],
   130   manual_reorder = [],
   131   timeout = seconds 10.0,
   132   prolog_system = Code_Prolog.SWI_PROLOG}) *}
   133 
   134 
   135 theorem S\<^sub>3_complete:
   136 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>3"
   137 quickcheck[tester = prolog, size=1, iterations=1]
   138 oops
   139 *)
   140 
   141 inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
   142   "[] \<in> S\<^sub>4"
   143 | "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
   144 | "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
   145 | "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
   146 | "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
   147 | "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
   148 | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   149 
   150 
   151 setup \<open>Code_Prolog.map_code_options (K
   152   {ensure_groundness = true,
   153   limit_globally = NONE,
   154   limited_types = [],
   155   limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
   156   replacing = [(("s4p", "limited_s4p"), "quickcheck")],
   157   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]})\<close>
   158 
   159 
   160 theorem S\<^sub>4_sound:
   161   "S\<^sub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   162 quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
   163 oops
   164 
   165 (*
   166 theorem S\<^sub>4_complete:
   167 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^sub>4"
   168 oops
   169 *)
   170 
   171 hide_const a b
   172 
   173 
   174 end