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