src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
author wenzelm
Mon, 15 Jul 2013 20:36:27 +0200
changeset 52666 391913d17d15
parent 45970 b6d0cff57d96
child 53015 a1119cf551e8
permissions -rw-r--r--
tuned line length;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     1
theory Context_Free_Grammar_Example
41956
c15ef1b85035 modernized imports (untested!?);
wenzelm
parents: 40924
diff changeset
     2
imports "~~/src/HOL/Library/Code_Prolog"
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     3
begin
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
     4
(*
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     5
declare mem_def[code_pred_inline]
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
     6
*)
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     7
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     8
subsection {* Alternative rules for length *}
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
     9
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    10
definition size_list :: "'a list => nat"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    11
where "size_list = size"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    12
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    13
lemma size_list_simps:
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    14
  "size_list [] = 0"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    15
  "size_list (x # xs) = Suc (size_list xs)"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    16
by (auto simp add: size_list_def)
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    17
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    18
declare size_list_simps[code_pred_def]
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    19
declare size_list_def[symmetric, code_pred_inline]
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    20
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    21
52666
391913d17d15 tuned line length;
wenzelm
parents: 45970
diff changeset
    22
setup {*
391913d17d15 tuned line length;
wenzelm
parents: 45970
diff changeset
    23
  Context.theory_map
391913d17d15 tuned line length;
wenzelm
parents: 45970
diff changeset
    24
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
391913d17d15 tuned line length;
wenzelm
parents: 45970
diff changeset
    25
*}
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    26
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    27
datatype alphabet = a | b
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    28
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    29
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    30
  "[] \<in> S\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    31
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    32
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    33
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    34
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    35
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    36
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    37
lemma
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    38
  "S\<^isub>1p w \<Longrightarrow> w = []"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
    39
quickcheck[tester = prolog, iterations=1, expect = counterexample]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    40
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    41
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    42
definition "filter_a = filter (\<lambda>x. x = a)"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    43
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    44
lemma [code_pred_def]: "filter_a [] = []"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    45
unfolding filter_a_def by simp
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    46
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    47
lemma [code_pred_def]: "filter_a (x#xs) = (if x = a then x # filter_a xs else filter_a xs)"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    48
unfolding filter_a_def by simp
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    49
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    50
declare filter_a_def[symmetric, code_pred_inline]
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    51
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    52
definition "filter_b = filter (\<lambda>x. x = b)"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    53
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    54
lemma [code_pred_def]: "filter_b [] = []"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    55
unfolding filter_b_def by simp
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    56
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    57
lemma [code_pred_def]: "filter_b (x#xs) = (if x = b then x # filter_b xs else filter_b xs)"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    58
unfolding filter_b_def by simp
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    59
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    60
declare filter_b_def[symmetric, code_pred_inline]
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    61
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    62
setup {* Code_Prolog.map_code_options (K
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    63
  {ensure_groundness = true,
39800
17e29ddd538e adapting manual configuration in examples
bulwahn
parents: 39463
diff changeset
    64
  limit_globally = NONE,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    65
  limited_types = [],
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    66
  limited_predicates = [(["s1p", "a1p", "b1p"], 2)],
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    67
  replacing = [(("s1p", "limited_s1p"), "quickcheck")],
39463
7ce0ed8dc4d6 adapting examples
bulwahn
parents: 39189
diff changeset
    68
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    69
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    70
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    71
theorem S\<^isub>1_sound:
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    72
"S\<^isub>1p w \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
    73
quickcheck[tester = prolog, iterations=1, expect = counterexample]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    74
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    75
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    76
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    77
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    78
  "[] \<in> S\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    79
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    80
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    81
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    82
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    83
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    84
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    85
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    86
setup {* Code_Prolog.map_code_options (K
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    87
  {ensure_groundness = true,
39800
17e29ddd538e adapting manual configuration in examples
bulwahn
parents: 39463
diff changeset
    88
  limit_globally = NONE,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    89
  limited_types = [],
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    90
  limited_predicates = [(["s2p", "a2p", "b2p"], 3)],
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    91
  replacing = [(("s2p", "limited_s2p"), "quickcheck")],
39463
7ce0ed8dc4d6 adapting examples
bulwahn
parents: 39189
diff changeset
    92
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    93
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    94
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    95
theorem S\<^isub>2_sound:
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
    96
  "S\<^isub>2p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
    97
quickcheck[tester = prolog, iterations=1, expect = counterexample]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    98
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
    99
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   100
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   101
  "[] \<in> S\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   102
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   103
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   104
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   105
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   106
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   107
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   108
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   109
setup {* Code_Prolog.map_code_options (K
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   110
  {ensure_groundness = true,
39800
17e29ddd538e adapting manual configuration in examples
bulwahn
parents: 39463
diff changeset
   111
  limit_globally = NONE,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   112
  limited_types = [],
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   113
  limited_predicates = [(["s3p", "a3p", "b3p"], 6)],
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   114
  replacing = [(("s3p", "limited_s3p"), "quickcheck")],
39463
7ce0ed8dc4d6 adapting examples
bulwahn
parents: 39189
diff changeset
   115
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   116
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   117
lemma S\<^isub>3_sound:
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   118
  "S\<^isub>3p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
   119
quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   120
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   121
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   122
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   123
(*
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   124
setup {* Code_Prolog.map_code_options (K
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   125
  {ensure_groundness = true,
39800
17e29ddd538e adapting manual configuration in examples
bulwahn
parents: 39463
diff changeset
   126
  limit_globally = NONE,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   127
  limited_types = [],
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   128
  limited_predicates = [],
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   129
  replacing = [],
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   130
  manual_reorder = [],
40301
bf39a257b3d3 simplified some time constants;
wenzelm
parents: 39800
diff changeset
   131
  timeout = seconds 10.0,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   132
  prolog_system = Code_Prolog.SWI_PROLOG}) *}
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   133
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   134
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   135
theorem S\<^isub>3_complete:
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   136
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
   137
quickcheck[tester = prolog, size=1, iterations=1]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   138
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   139
*)
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   140
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   141
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   142
  "[] \<in> S\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   143
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   144
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   145
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   146
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   147
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   148
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   149
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   150
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   151
setup {* Code_Prolog.map_code_options (K
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   152
  {ensure_groundness = true,
39800
17e29ddd538e adapting manual configuration in examples
bulwahn
parents: 39463
diff changeset
   153
  limit_globally = NONE,
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   154
  limited_types = [],
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   155
  limited_predicates = [(["s4p", "a4p", "b4p"], 6)],
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   156
  replacing = [(("s4p", "limited_s4p"), "quickcheck")],
39463
7ce0ed8dc4d6 adapting examples
bulwahn
parents: 39189
diff changeset
   157
  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   158
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   159
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   160
theorem S\<^isub>4_sound:
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 43913
diff changeset
   161
  "S\<^isub>4p w \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
40924
a9be7f26b4e6 adapting predicate_compile_quickcheck
bulwahn
parents: 40301
diff changeset
   162
quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
38962
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   163
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   164
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   165
(*
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   166
theorem S\<^isub>4_complete:
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   167
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   168
oops
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   169
*)
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   170
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   171
hide_const a b
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   172
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   173
3917c2acaec4 adding further example for quickcheck with prolog code generation
bulwahn
parents:
diff changeset
   174
end