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