src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 67226 ec32cdaab97b
permissions -rw-r--r--
more robust sorted_entries;
bulwahn@39655
     1
theory Predicate_Compile_Tests
wenzelm@66453
     2
imports "HOL-Library.Predicate_Compile_Alternative_Defs"
bulwahn@39655
     3
begin
bulwahn@39655
     4
krauss@42208
     5
declare [[values_timeout = 480.0]]
krauss@42142
     6
wenzelm@63167
     7
subsection \<open>Basic predicates\<close>
bulwahn@39655
     8
bulwahn@39655
     9
inductive False' :: "bool"
bulwahn@39655
    10
bulwahn@39655
    11
code_pred (expected_modes: bool) False' .
bulwahn@39655
    12
code_pred [dseq] False' .
bulwahn@39655
    13
code_pred [random_dseq] False' .
bulwahn@39655
    14
bulwahn@39655
    15
values [expected "{}" pred] "{x. False'}"
bulwahn@39655
    16
values [expected "{}" dseq 1] "{x. False'}"
bulwahn@39655
    17
values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
bulwahn@39655
    18
bulwahn@39655
    19
value "False'"
bulwahn@39655
    20
bulwahn@39655
    21
inductive True' :: "bool"
bulwahn@39655
    22
where
bulwahn@39655
    23
  "True ==> True'"
bulwahn@39655
    24
bulwahn@39655
    25
code_pred True' .
bulwahn@39655
    26
code_pred [dseq] True' .
bulwahn@39655
    27
code_pred [random_dseq] True' .
bulwahn@39655
    28
bulwahn@39655
    29
thm True'.equation
bulwahn@39655
    30
thm True'.dseq_equation
bulwahn@39655
    31
thm True'.random_dseq_equation
haftmann@51143
    32
values [expected "{()}"] "{x. True'}"
bulwahn@39655
    33
values [expected "{}" dseq 0] "{x. True'}"
bulwahn@39655
    34
values [expected "{()}" dseq 1] "{x. True'}"
bulwahn@39655
    35
values [expected "{()}" dseq 2] "{x. True'}"
bulwahn@39655
    36
values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
bulwahn@39655
    37
values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
bulwahn@39655
    38
values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
bulwahn@39655
    39
values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
bulwahn@39655
    40
haftmann@45970
    41
inductive EmptyPred :: "'a \<Rightarrow> bool"
bulwahn@39655
    42
haftmann@45970
    43
code_pred (expected_modes: o => bool, i => bool) EmptyPred .
bulwahn@39655
    44
haftmann@45970
    45
definition EmptyPred' :: "'a \<Rightarrow> bool"
haftmann@45970
    46
where "EmptyPred' = (\<lambda> x. False)"
bulwahn@39655
    47
haftmann@45970
    48
code_pred (expected_modes: o => bool, i => bool) [inductify] EmptyPred' .
bulwahn@39655
    49
bulwahn@39655
    50
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
bulwahn@39655
    51
bulwahn@39655
    52
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
bulwahn@39655
    53
bulwahn@39655
    54
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@39655
    55
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@39655
    56
bulwahn@39655
    57
code_pred
bulwahn@39655
    58
  (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
bulwahn@39655
    59
         (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
bulwahn@39655
    60
         (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
bulwahn@39655
    61
         (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
bulwahn@39655
    62
         (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
bulwahn@39655
    63
         (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
bulwahn@39655
    64
         (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
bulwahn@39655
    65
         (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
bulwahn@39655
    66
  EmptyClosure .
bulwahn@39655
    67
bulwahn@39655
    68
thm EmptyClosure.equation
bulwahn@39655
    69
bulwahn@39655
    70
(* TODO: inductive package is broken!
bulwahn@39655
    71
inductive False'' :: "bool"
bulwahn@39655
    72
where
bulwahn@39655
    73
  "False \<Longrightarrow> False''"
bulwahn@39655
    74
bulwahn@40100
    75
code_pred (expected_modes: bool) False'' .
bulwahn@39655
    76
bulwahn@39655
    77
inductive EmptySet'' :: "'a \<Rightarrow> bool"
bulwahn@39655
    78
where
bulwahn@39655
    79
  "False \<Longrightarrow> EmptySet'' x"
bulwahn@39655
    80
bulwahn@40100
    81
code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
bulwahn@39655
    82
*)
bulwahn@39655
    83
bulwahn@39655
    84
consts a' :: 'a
bulwahn@39655
    85
bulwahn@39655
    86
inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@39655
    87
where
lukas@62121
    88
  "Fact a' a'"
bulwahn@39655
    89
bulwahn@39655
    90
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
bulwahn@39655
    91
wenzelm@63167
    92
text \<open>
lukas@62121
    93
  The following example was derived from an predicate in the CakeML formalisation provided by Lars Hupel.
wenzelm@63167
    94
\<close>
lukas@62121
    95
inductive predicate_where_argument_is_condition :: "bool \<Rightarrow> bool"
lukas@62121
    96
where
lukas@62121
    97
  "ck \<Longrightarrow> predicate_where_argument_is_condition ck"
lukas@62121
    98
lukas@62121
    99
code_pred predicate_where_argument_is_condition .
lukas@62121
   100
wenzelm@63167
   101
text \<open>Other similar examples of this kind:\<close>
lukas@62121
   102
lukas@62121
   103
inductive predicate_where_argument_is_in_equation :: "bool \<Rightarrow> bool"
lukas@62121
   104
where
lukas@62121
   105
  "ck = True \<Longrightarrow> predicate_where_argument_is_in_equation ck"
lukas@62121
   106
lukas@62121
   107
code_pred predicate_where_argument_is_in_equation .
lukas@62121
   108
lukas@62121
   109
inductive predicate_where_argument_is_condition_and_value :: "bool \<Rightarrow> bool"
lukas@62121
   110
where
lukas@62121
   111
  "predicate_where_argument_is_condition_and_value ck \<Longrightarrow> ck
lukas@62121
   112
     \<Longrightarrow> predicate_where_argument_is_condition_and_value ck"
lukas@62121
   113
lukas@62121
   114
code_pred predicate_where_argument_is_condition_and_value .
lukas@62121
   115
lukas@62121
   116
inductive predicate_where_argument_is_neg_condition :: "bool \<Rightarrow> bool"
lukas@62121
   117
where
lukas@62121
   118
  "\<not> ck \<Longrightarrow> predicate_where_argument_is_neg_condition ck"
lukas@62121
   119
lukas@62121
   120
code_pred predicate_where_argument_is_neg_condition .
lukas@62121
   121
lukas@62121
   122
inductive predicate_where_argument_is_neg_condition_and_in_equation :: "bool \<Rightarrow> bool"
lukas@62121
   123
where
lukas@62121
   124
  "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
lukas@62121
   125
lukas@62121
   126
code_pred predicate_where_argument_is_neg_condition_and_in_equation .
lukas@62121
   127
bulwahn@64542
   128
text {* Another related example that required slight adjustment of the proof procedure *}
bulwahn@64542
   129
bulwahn@64542
   130
inductive if_as_predicate :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@64542
   131
where
bulwahn@64542
   132
  "condition \<Longrightarrow> if_as_predicate condition then_value else_value then_value"
bulwahn@64542
   133
| "\<not> condition \<Longrightarrow> if_as_predicate condition then_value else_value else_value"
bulwahn@64542
   134
bulwahn@64542
   135
code_pred [show_proof_trace] if_as_predicate .
lukas@62121
   136
bulwahn@39655
   137
inductive zerozero :: "nat * nat => bool"
bulwahn@39655
   138
where
bulwahn@39655
   139
  "zerozero (0, 0)"
bulwahn@39655
   140
bulwahn@39655
   141
code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
bulwahn@39655
   142
code_pred [dseq] zerozero .
bulwahn@39655
   143
code_pred [random_dseq] zerozero .
bulwahn@39655
   144
bulwahn@39655
   145
thm zerozero.equation
bulwahn@39655
   146
thm zerozero.dseq_equation
bulwahn@39655
   147
thm zerozero.random_dseq_equation
bulwahn@39655
   148
wenzelm@63167
   149
text \<open>We expect the user to expand the tuples in the values command.
wenzelm@63167
   150
The following values command is not supported.\<close>
bulwahn@39655
   151
(*values "{x. zerozero x}" *)
wenzelm@63167
   152
text \<open>Instead, the user must type\<close>
bulwahn@39655
   153
values "{(x, y). zerozero (x, y)}"
bulwahn@39655
   154
bulwahn@39655
   155
values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
bulwahn@39655
   156
values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
bulwahn@39655
   157
values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
bulwahn@39655
   158
values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
bulwahn@39655
   159
values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
bulwahn@39655
   160
bulwahn@39655
   161
inductive nested_tuples :: "((int * int) * int * int) => bool"
bulwahn@39655
   162
where
bulwahn@39655
   163
  "nested_tuples ((0, 1), 2, 3)"
bulwahn@39655
   164
bulwahn@39655
   165
code_pred nested_tuples .
bulwahn@39655
   166
haftmann@51143
   167
inductive JamesBond :: "nat => int => natural => bool"
bulwahn@39655
   168
where
bulwahn@39655
   169
  "JamesBond 0 0 7"
bulwahn@39655
   170
bulwahn@39655
   171
code_pred JamesBond .
bulwahn@39655
   172
haftmann@51143
   173
values [expected "{(0::nat, 0::int , 7::natural)}"] "{(a, b, c). JamesBond a b c}"
haftmann@51143
   174
values [expected "{(0::nat, 7::natural, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
haftmann@51143
   175
values [expected "{(0::int, 0::nat, 7::natural)}"] "{(b, a, c). JamesBond a b c}"
haftmann@51143
   176
values [expected "{(0::int, 7::natural, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
haftmann@51143
   177
values [expected "{(7::natural, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
haftmann@51143
   178
values [expected "{(7::natural, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
bulwahn@39655
   179
haftmann@51143
   180
values [expected "{(7::natural, 0::int)}"] "{(a, b). JamesBond 0 b a}"
haftmann@51143
   181
values [expected "{(7::natural, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
haftmann@51143
   182
values [expected "{(0::nat, 7::natural)}"] "{(a, c). JamesBond a 0 c}"
bulwahn@39655
   183
bulwahn@39655
   184
wenzelm@63167
   185
subsection \<open>Alternative Rules\<close>
bulwahn@39655
   186
blanchet@58310
   187
datatype char = C | D | E | F | G | H
bulwahn@39655
   188
bulwahn@39655
   189
inductive is_C_or_D
bulwahn@39655
   190
where
bulwahn@39655
   191
  "(x = C) \<or> (x = D) ==> is_C_or_D x"
bulwahn@39655
   192
bulwahn@39655
   193
code_pred (expected_modes: i => bool) is_C_or_D .
bulwahn@39655
   194
thm is_C_or_D.equation
bulwahn@39655
   195
bulwahn@39655
   196
inductive is_D_or_E
bulwahn@39655
   197
where
bulwahn@39655
   198
  "(x = D) \<or> (x = E) ==> is_D_or_E x"
bulwahn@39655
   199
bulwahn@39655
   200
lemma [code_pred_intro]:
bulwahn@39655
   201
  "is_D_or_E D"
bulwahn@39655
   202
by (auto intro: is_D_or_E.intros)
bulwahn@39655
   203
bulwahn@39655
   204
lemma [code_pred_intro]:
bulwahn@39655
   205
  "is_D_or_E E"
bulwahn@39655
   206
by (auto intro: is_D_or_E.intros)
bulwahn@39655
   207
bulwahn@39655
   208
code_pred (expected_modes: o => bool, i => bool) is_D_or_E
bulwahn@39655
   209
proof -
bulwahn@39655
   210
  case is_D_or_E
bulwahn@39655
   211
  from is_D_or_E.prems show thesis
bulwahn@39655
   212
  proof 
bulwahn@39655
   213
    fix xa
bulwahn@39655
   214
    assume x: "x = xa"
bulwahn@39655
   215
    assume "xa = D \<or> xa = E"
bulwahn@39655
   216
    from this show thesis
bulwahn@39655
   217
    proof
bulwahn@39655
   218
      assume "xa = D" from this x is_D_or_E(1) show thesis by simp
bulwahn@39655
   219
    next
bulwahn@39655
   220
      assume "xa = E" from this x is_D_or_E(2) show thesis by simp
bulwahn@39655
   221
    qed
bulwahn@39655
   222
  qed
bulwahn@39655
   223
qed
bulwahn@39655
   224
bulwahn@39655
   225
thm is_D_or_E.equation
bulwahn@39655
   226
bulwahn@39655
   227
inductive is_F_or_G
bulwahn@39655
   228
where
bulwahn@39655
   229
  "x = F \<or> x = G ==> is_F_or_G x"
bulwahn@39655
   230
bulwahn@39655
   231
lemma [code_pred_intro]:
bulwahn@39655
   232
  "is_F_or_G F"
bulwahn@39655
   233
by (auto intro: is_F_or_G.intros)
bulwahn@39655
   234
bulwahn@39655
   235
lemma [code_pred_intro]:
bulwahn@39655
   236
  "is_F_or_G G"
bulwahn@39655
   237
by (auto intro: is_F_or_G.intros)
bulwahn@39655
   238
bulwahn@39655
   239
inductive is_FGH
bulwahn@39655
   240
where
bulwahn@39655
   241
  "is_F_or_G x ==> is_FGH x"
bulwahn@39655
   242
| "is_FGH H"
bulwahn@39655
   243
wenzelm@63167
   244
text \<open>Compilation of is_FGH requires elimination rule for is_F_or_G\<close>
bulwahn@39655
   245
bulwahn@39655
   246
code_pred (expected_modes: o => bool, i => bool) is_FGH
bulwahn@39655
   247
proof -
bulwahn@39655
   248
  case is_F_or_G
bulwahn@39655
   249
  from is_F_or_G.prems show thesis
bulwahn@39655
   250
  proof
bulwahn@39655
   251
    fix xa
bulwahn@39655
   252
    assume x: "x = xa"
bulwahn@39655
   253
    assume "xa = F \<or> xa = G"
bulwahn@39655
   254
    from this show thesis
bulwahn@39655
   255
    proof
bulwahn@39655
   256
      assume "xa = F"
bulwahn@39655
   257
      from this x is_F_or_G(1) show thesis by simp
bulwahn@39655
   258
    next
bulwahn@39655
   259
      assume "xa = G"
bulwahn@39655
   260
      from this x is_F_or_G(2) show thesis by simp
bulwahn@39655
   261
    qed
bulwahn@39655
   262
  qed
bulwahn@39655
   263
qed
bulwahn@39655
   264
wenzelm@63167
   265
subsection \<open>Named alternative rules\<close>
bulwahn@39655
   266
bulwahn@39655
   267
inductive appending
bulwahn@39655
   268
where
bulwahn@39655
   269
  nil: "appending [] ys ys"
bulwahn@39655
   270
| cons: "appending xs ys zs \<Longrightarrow> appending (x#xs) ys (x#zs)"
bulwahn@39655
   271
bulwahn@39655
   272
lemma appending_alt_nil: "ys = zs \<Longrightarrow> appending [] ys zs"
bulwahn@39655
   273
by (auto intro: appending.intros)
bulwahn@39655
   274
bulwahn@39655
   275
lemma appending_alt_cons: "xs' = x # xs \<Longrightarrow> appending xs ys zs \<Longrightarrow> zs' = x # zs \<Longrightarrow> appending xs' ys zs'"
bulwahn@39655
   276
by (auto intro: appending.intros)
bulwahn@39655
   277
wenzelm@63167
   278
text \<open>With code_pred_intro, we can give fact names to the alternative rules,
wenzelm@63167
   279
  which are used for the code_pred command.\<close>
bulwahn@39655
   280
bulwahn@39655
   281
declare appending_alt_nil[code_pred_intro alt_nil] appending_alt_cons[code_pred_intro alt_cons]
bulwahn@39655
   282
 
bulwahn@39655
   283
code_pred appending
bulwahn@39655
   284
proof -
bulwahn@39655
   285
  case appending
bulwahn@39655
   286
  from appending.prems show thesis
bulwahn@39655
   287
  proof(cases)
bulwahn@39655
   288
    case nil
wenzelm@60565
   289
    from appending.alt_nil nil show thesis by auto
bulwahn@39655
   290
  next
bulwahn@39655
   291
    case cons
wenzelm@60565
   292
    from appending.alt_cons cons show thesis by fastforce
bulwahn@39655
   293
  qed
bulwahn@39655
   294
qed
bulwahn@39655
   295
bulwahn@39655
   296
bulwahn@39655
   297
inductive ya_even and ya_odd :: "nat => bool"
bulwahn@39655
   298
where
bulwahn@39655
   299
  even_zero: "ya_even 0"
bulwahn@39655
   300
| odd_plus1: "ya_even x ==> ya_odd (x + 1)"
bulwahn@39655
   301
| even_plus1: "ya_odd x ==> ya_even (x + 1)"
bulwahn@39655
   302
bulwahn@39655
   303
bulwahn@39655
   304
declare even_zero[code_pred_intro even_0]
bulwahn@39655
   305
bulwahn@39655
   306
lemma [code_pred_intro odd_Suc]: "ya_even x ==> ya_odd (Suc x)"
bulwahn@39655
   307
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
bulwahn@39655
   308
bulwahn@39655
   309
lemma [code_pred_intro even_Suc]:"ya_odd x ==> ya_even (Suc x)"
bulwahn@39655
   310
by (auto simp only: Suc_eq_plus1 intro: ya_even_ya_odd.intros)
bulwahn@39655
   311
bulwahn@39655
   312
code_pred ya_even
bulwahn@39655
   313
proof -
bulwahn@39655
   314
  case ya_even
bulwahn@39655
   315
  from ya_even.prems show thesis
bulwahn@39655
   316
  proof (cases)
bulwahn@39655
   317
    case even_zero
wenzelm@60565
   318
    from even_zero ya_even.even_0 show thesis by simp
bulwahn@39655
   319
  next
bulwahn@39655
   320
    case even_plus1
wenzelm@60565
   321
    from even_plus1 ya_even.even_Suc show thesis by simp
bulwahn@39655
   322
  qed
bulwahn@39655
   323
next
bulwahn@39655
   324
  case ya_odd
bulwahn@39655
   325
  from ya_odd.prems show thesis
bulwahn@39655
   326
  proof (cases)
bulwahn@39655
   327
    case odd_plus1
wenzelm@60565
   328
    from odd_plus1 ya_odd.odd_Suc show thesis by simp
bulwahn@39655
   329
  qed
bulwahn@39655
   330
qed
bulwahn@39655
   331
wenzelm@63167
   332
subsection \<open>Preprocessor Inlining\<close>
bulwahn@39655
   333
bulwahn@39655
   334
definition "equals == (op =)"
bulwahn@39655
   335
 
bulwahn@39655
   336
inductive zerozero' :: "nat * nat => bool" where
bulwahn@39655
   337
  "equals (x, y) (0, 0) ==> zerozero' (x, y)"
bulwahn@39655
   338
bulwahn@39655
   339
code_pred (expected_modes: i => bool) zerozero' .
bulwahn@39655
   340
bulwahn@39655
   341
lemma zerozero'_eq: "zerozero' x == zerozero x"
bulwahn@39655
   342
proof -
bulwahn@39655
   343
  have "zerozero' = zerozero"
haftmann@45970
   344
    apply (auto simp add: fun_eq_iff)
bulwahn@39655
   345
    apply (cases rule: zerozero'.cases)
bulwahn@39655
   346
    apply (auto simp add: equals_def intro: zerozero.intros)
bulwahn@39655
   347
    apply (cases rule: zerozero.cases)
bulwahn@39655
   348
    apply (auto simp add: equals_def intro: zerozero'.intros)
bulwahn@39655
   349
    done
bulwahn@39655
   350
  from this show "zerozero' x == zerozero x" by auto
bulwahn@39655
   351
qed
bulwahn@39655
   352
bulwahn@39655
   353
declare zerozero'_eq [code_pred_inline]
bulwahn@39655
   354
bulwahn@39655
   355
definition "zerozero'' x == zerozero' x"
bulwahn@39655
   356
wenzelm@63167
   357
text \<open>if preprocessing fails, zerozero'' will not have all modes.\<close>
bulwahn@39655
   358
bulwahn@39655
   359
code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
bulwahn@39655
   360
wenzelm@63167
   361
subsection \<open>Sets\<close>
haftmann@45970
   362
(*
haftmann@45970
   363
inductive_set EmptySet :: "'a set"
haftmann@45970
   364
haftmann@45970
   365
code_pred (expected_modes: o => bool, i => bool) EmptySet .
haftmann@45970
   366
haftmann@45970
   367
definition EmptySet' :: "'a set"
haftmann@45970
   368
where "EmptySet' = {}"
haftmann@45970
   369
haftmann@45970
   370
code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
haftmann@45970
   371
*)
wenzelm@63167
   372
subsection \<open>Numerals\<close>
bulwahn@39655
   373
bulwahn@39655
   374
definition
haftmann@45970
   375
  "one_or_two = (%x. x = Suc 0 \<or> ( x = Suc (Suc 0)))"
bulwahn@39655
   376
bulwahn@39655
   377
code_pred [inductify] one_or_two .
bulwahn@39655
   378
bulwahn@39655
   379
code_pred [dseq] one_or_two .
bulwahn@39655
   380
code_pred [random_dseq] one_or_two .
bulwahn@39655
   381
thm one_or_two.dseq_equation
eberlm@66283
   382
values [expected "{1::nat, 2}"] "{x. one_or_two x}"
bulwahn@39655
   383
values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
bulwahn@39655
   384
bulwahn@39655
   385
inductive one_or_two' :: "nat => bool"
bulwahn@39655
   386
where
bulwahn@39655
   387
  "one_or_two' 1"
bulwahn@39655
   388
| "one_or_two' 2"
bulwahn@39655
   389
bulwahn@39655
   390
code_pred one_or_two' .
bulwahn@39655
   391
thm one_or_two'.equation
bulwahn@39655
   392
bulwahn@39655
   393
values "{x. one_or_two' x}"
bulwahn@39655
   394
bulwahn@39655
   395
definition one_or_two'':
haftmann@45970
   396
  "one_or_two'' == (%x. x = 1 \<or> x = (2::nat))"
bulwahn@39655
   397
bulwahn@39655
   398
code_pred [inductify] one_or_two'' .
bulwahn@39655
   399
thm one_or_two''.equation
bulwahn@39655
   400
bulwahn@39655
   401
values "{x. one_or_two'' x}"
bulwahn@39655
   402
wenzelm@63167
   403
subsection \<open>even predicate\<close>
bulwahn@39655
   404
bulwahn@39655
   405
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
bulwahn@39655
   406
    "even 0"
bulwahn@39655
   407
  | "even n \<Longrightarrow> odd (Suc n)"
bulwahn@39655
   408
  | "odd n \<Longrightarrow> even (Suc n)"
bulwahn@39655
   409
bulwahn@39655
   410
code_pred (expected_modes: i => bool, o => bool) even .
bulwahn@39655
   411
code_pred [dseq] even .
bulwahn@39655
   412
code_pred [random_dseq] even .
bulwahn@39655
   413
bulwahn@39655
   414
thm odd.equation
bulwahn@39655
   415
thm even.equation
bulwahn@39655
   416
thm odd.dseq_equation
bulwahn@39655
   417
thm even.dseq_equation
bulwahn@39655
   418
thm odd.random_dseq_equation
bulwahn@39655
   419
thm even.random_dseq_equation
bulwahn@39655
   420
bulwahn@39655
   421
values "{x. even 2}"
bulwahn@39655
   422
values "{x. odd 2}"
bulwahn@39655
   423
values 10 "{n. even n}"
bulwahn@39655
   424
values 10 "{n. odd n}"
bulwahn@39655
   425
values [expected "{}" dseq 2] "{x. even 6}"
bulwahn@39655
   426
values [expected "{}" dseq 6] "{x. even 6}"
bulwahn@39655
   427
values [expected "{()}" dseq 7] "{x. even 6}"
bulwahn@39655
   428
values [dseq 2] "{x. odd 7}"
bulwahn@39655
   429
values [dseq 6] "{x. odd 7}"
bulwahn@39655
   430
values [dseq 7] "{x. odd 7}"
bulwahn@39655
   431
values [expected "{()}" dseq 8] "{x. odd 7}"
bulwahn@39655
   432
bulwahn@39655
   433
values [expected "{}" dseq 0] 8 "{x. even x}"
bulwahn@39655
   434
values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
eberlm@66283
   435
values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
eberlm@66283
   436
values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
eberlm@66283
   437
values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
bulwahn@39655
   438
bulwahn@39655
   439
values [random_dseq 1, 1, 0] 8 "{x. even x}"
bulwahn@39655
   440
values [random_dseq 1, 1, 1] 8 "{x. even x}"
bulwahn@39655
   441
values [random_dseq 1, 1, 2] 8 "{x. even x}"
bulwahn@39655
   442
values [random_dseq 1, 1, 3] 8 "{x. even x}"
bulwahn@39655
   443
values [random_dseq 1, 1, 6] 8 "{x. even x}"
bulwahn@39655
   444
bulwahn@39655
   445
values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
bulwahn@39655
   446
values [random_dseq 1, 1, 8] "{x. odd 7}"
bulwahn@39655
   447
values [random_dseq 1, 1, 9] "{x. odd 7}"
bulwahn@39655
   448
bulwahn@39655
   449
definition odd' where "odd' x == \<not> even x"
bulwahn@39655
   450
bulwahn@39655
   451
code_pred (expected_modes: i => bool) [inductify] odd' .
bulwahn@39655
   452
code_pred [dseq inductify] odd' .
bulwahn@39655
   453
code_pred [random_dseq inductify] odd' .
bulwahn@39655
   454
bulwahn@39655
   455
values [expected "{}" dseq 2] "{x. odd' 7}"
bulwahn@39655
   456
values [expected "{()}" dseq 9] "{x. odd' 7}"
bulwahn@39655
   457
values [expected "{}" dseq 2] "{x. odd' 8}"
bulwahn@39655
   458
values [expected "{}" dseq 10] "{x. odd' 8}"
bulwahn@39655
   459
bulwahn@39655
   460
bulwahn@39655
   461
inductive is_even :: "nat \<Rightarrow> bool"
bulwahn@39655
   462
where
bulwahn@39655
   463
  "n mod 2 = 0 \<Longrightarrow> is_even n"
bulwahn@39655
   464
bulwahn@39655
   465
code_pred (expected_modes: i => bool) is_even .
bulwahn@39655
   466
wenzelm@63167
   467
subsection \<open>append predicate\<close>
bulwahn@39655
   468
bulwahn@39655
   469
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
bulwahn@39655
   470
    "append [] xs xs"
bulwahn@39655
   471
  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
bulwahn@39655
   472
bulwahn@39655
   473
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
bulwahn@39655
   474
  i => o => i => bool as suffix, i => i => i => bool) append .
bulwahn@39655
   475
code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
bulwahn@39655
   476
  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
bulwahn@39655
   477
bulwahn@39655
   478
code_pred [dseq] append .
bulwahn@39655
   479
code_pred [random_dseq] append .
bulwahn@39655
   480
bulwahn@39655
   481
thm append.equation
bulwahn@39655
   482
thm append.dseq_equation
bulwahn@39655
   483
thm append.random_dseq_equation
bulwahn@39655
   484
bulwahn@39655
   485
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
bulwahn@39655
   486
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
bulwahn@39655
   487
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
bulwahn@39655
   488
bulwahn@39655
   489
values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
eberlm@66283
   490
values [expected "{(([]::nat list), [1::nat, 2, 3, 4, 5])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@39655
   491
values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@39655
   492
values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@39655
   493
values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@39655
   494
values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@39655
   495
values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@39655
   496
values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@39655
   497
values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@39655
   498
values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@39655
   499
haftmann@56927
   500
value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
haftmann@56927
   501
value "Predicate.the (slice ([]::int list))"
bulwahn@39655
   502
bulwahn@39655
   503
wenzelm@63167
   504
text \<open>tricky case with alternative rules\<close>
bulwahn@39655
   505
bulwahn@39655
   506
inductive append2
bulwahn@39655
   507
where
bulwahn@39655
   508
  "append2 [] xs xs"
bulwahn@39655
   509
| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
bulwahn@39655
   510
bulwahn@39655
   511
lemma append2_Nil: "append2 [] (xs::'b list) xs"
bulwahn@39655
   512
  by (simp add: append2.intros(1))
bulwahn@39655
   513
bulwahn@39655
   514
lemmas [code_pred_intro] = append2_Nil append2.intros(2)
bulwahn@39655
   515
bulwahn@39655
   516
code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
bulwahn@39655
   517
  i => o => i => bool, i => i => i => bool) append2
bulwahn@39655
   518
proof -
bulwahn@39655
   519
  case append2
bulwahn@39655
   520
  from append2.prems show thesis
bulwahn@39655
   521
  proof
bulwahn@39655
   522
    fix xs
bulwahn@39655
   523
    assume "xa = []" "xb = xs" "xc = xs"
bulwahn@39655
   524
    from this append2(1) show thesis by simp
bulwahn@39655
   525
  next
bulwahn@39655
   526
    fix xs ys zs x
bulwahn@39655
   527
    assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
nipkow@44890
   528
    from this append2(2) show thesis by fastforce
bulwahn@39655
   529
  qed
bulwahn@39655
   530
qed
bulwahn@39655
   531
bulwahn@39655
   532
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@39655
   533
where
bulwahn@39655
   534
  "tupled_append ([], xs, xs)"
bulwahn@39655
   535
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
bulwahn@39655
   536
bulwahn@39655
   537
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@39655
   538
  i * o * i => bool, i * i * i => bool) tupled_append .
bulwahn@39655
   539
bulwahn@39655
   540
code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
bulwahn@39655
   541
  i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
bulwahn@39655
   542
bulwahn@39655
   543
code_pred [random_dseq] tupled_append .
bulwahn@39655
   544
thm tupled_append.equation
bulwahn@39655
   545
bulwahn@39655
   546
values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
bulwahn@39655
   547
bulwahn@39655
   548
inductive tupled_append'
bulwahn@39655
   549
where
bulwahn@39655
   550
"tupled_append' ([], xs, xs)"
bulwahn@39655
   551
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
bulwahn@39655
   552
 tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
bulwahn@39655
   553
bulwahn@39655
   554
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@39655
   555
  i * o * i => bool, i * i * i => bool) tupled_append' .
bulwahn@39655
   556
thm tupled_append'.equation
bulwahn@39655
   557
bulwahn@39655
   558
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@39655
   559
where
bulwahn@39655
   560
  "tupled_append'' ([], xs, xs)"
bulwahn@39655
   561
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
bulwahn@39655
   562
bulwahn@39655
   563
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@39655
   564
  i * o * i => bool, i * i * i => bool) tupled_append'' .
bulwahn@39655
   565
thm tupled_append''.equation
bulwahn@39655
   566
bulwahn@39655
   567
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@39655
   568
where
bulwahn@39655
   569
  "tupled_append''' ([], xs, xs)"
bulwahn@39655
   570
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
bulwahn@39655
   571
bulwahn@39655
   572
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@39655
   573
  i * o * i => bool, i * i * i => bool) tupled_append''' .
bulwahn@39655
   574
thm tupled_append'''.equation
bulwahn@39655
   575
wenzelm@63167
   576
subsection \<open>map_ofP predicate\<close>
bulwahn@39655
   577
bulwahn@39655
   578
inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
bulwahn@39655
   579
where
bulwahn@39655
   580
  "map_ofP ((a, b)#xs) a b"
bulwahn@39655
   581
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
bulwahn@39655
   582
bulwahn@39655
   583
code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
bulwahn@39655
   584
thm map_ofP.equation
bulwahn@39655
   585
wenzelm@63167
   586
subsection \<open>filter predicate\<close>
bulwahn@39655
   587
bulwahn@39655
   588
inductive filter1
bulwahn@39655
   589
for P
bulwahn@39655
   590
where
bulwahn@39655
   591
  "filter1 P [] []"
bulwahn@39655
   592
| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
bulwahn@39655
   593
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
bulwahn@39655
   594
bulwahn@39655
   595
code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
bulwahn@39655
   596
code_pred [dseq] filter1 .
bulwahn@39655
   597
code_pred [random_dseq] filter1 .
bulwahn@39655
   598
bulwahn@39655
   599
thm filter1.equation
bulwahn@39655
   600
eberlm@66283
   601
values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
bulwahn@39655
   602
values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
eberlm@66283
   603
values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
bulwahn@39655
   604
bulwahn@39655
   605
inductive filter2
bulwahn@39655
   606
where
bulwahn@39655
   607
  "filter2 P [] []"
bulwahn@39655
   608
| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
bulwahn@39655
   609
| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
bulwahn@39655
   610
bulwahn@39655
   611
code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
bulwahn@39655
   612
code_pred [dseq] filter2 .
bulwahn@39655
   613
code_pred [random_dseq] filter2 .
bulwahn@39655
   614
bulwahn@39655
   615
thm filter2.equation
bulwahn@39655
   616
thm filter2.random_dseq_equation
bulwahn@39655
   617
bulwahn@39655
   618
inductive filter3
bulwahn@39655
   619
for P
bulwahn@39655
   620
where
bulwahn@39655
   621
  "List.filter P xs = ys ==> filter3 P xs ys"
bulwahn@39655
   622
bulwahn@39655
   623
code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) [skip_proof] filter3 .
bulwahn@39655
   624
bulwahn@39655
   625
code_pred filter3 .
bulwahn@39655
   626
thm filter3.equation
bulwahn@39655
   627
bulwahn@39655
   628
(*
bulwahn@39655
   629
inductive filter4
bulwahn@39655
   630
where
bulwahn@39655
   631
  "List.filter P xs = ys ==> filter4 P xs ys"
bulwahn@39655
   632
bulwahn@39655
   633
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
bulwahn@39655
   634
(*code_pred [depth_limited] filter4 .*)
bulwahn@39655
   635
(*code_pred [random] filter4 .*)
bulwahn@39655
   636
*)
wenzelm@63167
   637
subsection \<open>reverse predicate\<close>
bulwahn@39655
   638
bulwahn@39655
   639
inductive rev where
bulwahn@39655
   640
    "rev [] []"
bulwahn@39655
   641
  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
bulwahn@39655
   642
bulwahn@39655
   643
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
bulwahn@39655
   644
bulwahn@39655
   645
thm rev.equation
bulwahn@39655
   646
bulwahn@39655
   647
values "{xs. rev [0, 1, 2, 3::nat] xs}"
bulwahn@39655
   648
bulwahn@39655
   649
inductive tupled_rev where
bulwahn@39655
   650
  "tupled_rev ([], [])"
bulwahn@39655
   651
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
bulwahn@39655
   652
bulwahn@39655
   653
code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
bulwahn@39655
   654
thm tupled_rev.equation
bulwahn@39655
   655
wenzelm@63167
   656
subsection \<open>partition predicate\<close>
bulwahn@39655
   657
bulwahn@39655
   658
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
bulwahn@39655
   659
  for f where
bulwahn@39655
   660
    "partition f [] [] []"
bulwahn@39655
   661
  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
bulwahn@39655
   662
  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
bulwahn@39655
   663
bulwahn@39655
   664
code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
bulwahn@39655
   665
  (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
bulwahn@39655
   666
  partition .
bulwahn@39655
   667
code_pred [dseq] partition .
bulwahn@39655
   668
code_pred [random_dseq] partition .
bulwahn@39655
   669
bulwahn@39655
   670
values 10 "{(ys, zs). partition is_even
bulwahn@39655
   671
  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
bulwahn@39655
   672
values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
bulwahn@39655
   673
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
bulwahn@39655
   674
bulwahn@39655
   675
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
bulwahn@39655
   676
  for f where
bulwahn@39655
   677
   "tupled_partition f ([], [], [])"
bulwahn@39655
   678
  | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
bulwahn@39655
   679
  | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
bulwahn@39655
   680
bulwahn@39655
   681
code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
bulwahn@39655
   682
  (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
bulwahn@39655
   683
bulwahn@39655
   684
thm tupled_partition.equation
bulwahn@39655
   685
bulwahn@39655
   686
lemma [code_pred_intro]:
bulwahn@39655
   687
  "r a b \<Longrightarrow> tranclp r a b"
bulwahn@39655
   688
  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
bulwahn@39655
   689
  by auto
bulwahn@39655
   690
wenzelm@63167
   691
subsection \<open>transitive predicate\<close>
bulwahn@39655
   692
wenzelm@63167
   693
text \<open>Also look at the tabled transitive closure in the Library\<close>
bulwahn@39655
   694
bulwahn@39655
   695
code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
bulwahn@39655
   696
  (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
bulwahn@39655
   697
  (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
bulwahn@39655
   698
proof -
bulwahn@39655
   699
  case tranclp
bulwahn@39655
   700
  from this converse_tranclpE[OF tranclp.prems] show thesis by metis
bulwahn@39655
   701
qed
bulwahn@39655
   702
bulwahn@39655
   703
bulwahn@39655
   704
code_pred [dseq] tranclp .
bulwahn@39655
   705
code_pred [random_dseq] tranclp .
bulwahn@39655
   706
thm tranclp.equation
bulwahn@39655
   707
thm tranclp.random_dseq_equation
bulwahn@39655
   708
bulwahn@39655
   709
inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
bulwahn@39655
   710
where
bulwahn@39655
   711
  "rtrancl' x x r"
bulwahn@39655
   712
| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
bulwahn@39655
   713
bulwahn@39655
   714
code_pred [random_dseq] rtrancl' .
bulwahn@39655
   715
bulwahn@39655
   716
thm rtrancl'.random_dseq_equation
bulwahn@39655
   717
bulwahn@39655
   718
inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
bulwahn@39655
   719
where
bulwahn@39655
   720
  "rtrancl'' (x, x, r)"
bulwahn@39655
   721
| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
bulwahn@39655
   722
bulwahn@39655
   723
code_pred rtrancl'' .
bulwahn@39655
   724
bulwahn@39655
   725
inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
bulwahn@39655
   726
where
bulwahn@39655
   727
  "rtrancl''' (x, (x, x), r)"
bulwahn@39655
   728
| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
bulwahn@39655
   729
bulwahn@39655
   730
code_pred rtrancl''' .
bulwahn@39655
   731
bulwahn@39655
   732
bulwahn@39655
   733
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
bulwahn@39655
   734
    "succ 0 1"
bulwahn@39655
   735
  | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
bulwahn@39655
   736
bulwahn@39655
   737
code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
bulwahn@39655
   738
code_pred [random_dseq] succ .
bulwahn@39655
   739
thm succ.equation
bulwahn@39655
   740
thm succ.random_dseq_equation
bulwahn@39655
   741
bulwahn@39655
   742
values 10 "{(m, n). succ n m}"
bulwahn@39655
   743
values "{m. succ 0 m}"
bulwahn@39655
   744
values "{m. succ m 0}"
bulwahn@39655
   745
wenzelm@63167
   746
text \<open>values command needs mode annotation of the parameter succ
wenzelm@63167
   747
to disambiguate which mode is to be chosen.\<close> 
bulwahn@39655
   748
bulwahn@39655
   749
values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
bulwahn@39655
   750
values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
bulwahn@39655
   751
values 20 "{(n, m). tranclp succ n m}"
bulwahn@39655
   752
bulwahn@39655
   753
inductive example_graph :: "int => int => bool"
bulwahn@39655
   754
where
bulwahn@39655
   755
  "example_graph 0 1"
bulwahn@39655
   756
| "example_graph 1 2"
bulwahn@39655
   757
| "example_graph 1 3"
bulwahn@39655
   758
| "example_graph 4 7"
bulwahn@39655
   759
| "example_graph 4 5"
bulwahn@39655
   760
| "example_graph 5 6"
bulwahn@39655
   761
| "example_graph 7 6"
bulwahn@39655
   762
| "example_graph 7 8"
bulwahn@39655
   763
 
bulwahn@39655
   764
inductive not_reachable_in_example_graph :: "int => int => bool"
bulwahn@39655
   765
where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
bulwahn@39655
   766
bulwahn@39655
   767
code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
bulwahn@39655
   768
bulwahn@39655
   769
thm not_reachable_in_example_graph.equation
bulwahn@39655
   770
thm tranclp.equation
bulwahn@39655
   771
value "not_reachable_in_example_graph 0 3"
bulwahn@39655
   772
value "not_reachable_in_example_graph 4 8"
bulwahn@39655
   773
value "not_reachable_in_example_graph 5 6"
wenzelm@63167
   774
text \<open>rtrancl compilation is strange!\<close>
bulwahn@39655
   775
(*
bulwahn@39655
   776
value "not_reachable_in_example_graph 0 4"
bulwahn@39655
   777
value "not_reachable_in_example_graph 1 6"
bulwahn@39655
   778
value "not_reachable_in_example_graph 8 4"*)
bulwahn@39655
   779
bulwahn@39655
   780
code_pred [dseq] not_reachable_in_example_graph .
bulwahn@39655
   781
bulwahn@39655
   782
values [dseq 6] "{x. tranclp example_graph 0 3}"
bulwahn@39655
   783
bulwahn@39655
   784
values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
bulwahn@39655
   785
values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
bulwahn@39655
   786
values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
bulwahn@39655
   787
values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
bulwahn@39655
   788
values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
bulwahn@39655
   789
values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
bulwahn@39655
   790
bulwahn@39655
   791
bulwahn@39655
   792
inductive not_reachable_in_example_graph' :: "int => int => bool"
bulwahn@39655
   793
where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
bulwahn@39655
   794
bulwahn@39655
   795
code_pred not_reachable_in_example_graph' .
bulwahn@39655
   796
bulwahn@39655
   797
value "not_reachable_in_example_graph' 0 3"
bulwahn@39655
   798
(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
bulwahn@39655
   799
bulwahn@39655
   800
bulwahn@39655
   801
(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@39655
   802
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
bulwahn@39655
   803
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@39655
   804
(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
bulwahn@39655
   805
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@39655
   806
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@39655
   807
bulwahn@39655
   808
code_pred [dseq] not_reachable_in_example_graph' .
bulwahn@39655
   809
bulwahn@39655
   810
(*thm not_reachable_in_example_graph'.dseq_equation*)
bulwahn@39655
   811
bulwahn@39655
   812
(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@39655
   813
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
bulwahn@39655
   814
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
bulwahn@39655
   815
values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
bulwahn@39655
   816
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@39655
   817
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@39655
   818
wenzelm@63167
   819
subsection \<open>Free function variable\<close>
bulwahn@39655
   820
bulwahn@39655
   821
inductive FF :: "nat => nat => bool"
bulwahn@39655
   822
where
bulwahn@39655
   823
  "f x = y ==> FF x y"
bulwahn@39655
   824
bulwahn@39655
   825
code_pred FF .
bulwahn@39655
   826
wenzelm@63167
   827
subsection \<open>IMP\<close>
bulwahn@39655
   828
wenzelm@42463
   829
type_synonym var = nat
wenzelm@42463
   830
type_synonym state = "int list"
bulwahn@39655
   831
blanchet@58310
   832
datatype com =
bulwahn@39655
   833
  Skip |
bulwahn@39655
   834
  Ass var "state => int" |
bulwahn@39655
   835
  Seq com com |
bulwahn@39655
   836
  IF "state => bool" com com |
bulwahn@39655
   837
  While "state => bool" com
bulwahn@39655
   838
bulwahn@39655
   839
inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
bulwahn@39655
   840
"tupled_exec (Skip, s, s)" |
bulwahn@39655
   841
"tupled_exec (Ass x e, s, s[x := e(s)])" |
bulwahn@39655
   842
"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
bulwahn@39655
   843
"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
bulwahn@39655
   844
"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
bulwahn@39655
   845
"~b s ==> tupled_exec (While b c, s, s)" |
bulwahn@39655
   846
"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
bulwahn@39655
   847
bulwahn@39655
   848
code_pred tupled_exec .
bulwahn@39655
   849
bulwahn@39655
   850
values "{s. tupled_exec (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))), [3, 5], s)}"
bulwahn@39655
   851
wenzelm@63167
   852
subsection \<open>CCS\<close>
bulwahn@39655
   853
wenzelm@63167
   854
text\<open>This example formalizes finite CCS processes without communication or
wenzelm@63167
   855
recursion. For simplicity, labels are natural numbers.\<close>
bulwahn@39655
   856
blanchet@58310
   857
datatype proc = nil | pre nat proc | or proc proc | par proc proc
bulwahn@39655
   858
bulwahn@39655
   859
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
bulwahn@39655
   860
where
bulwahn@39655
   861
"tupled_step (pre n p, n, p)" |
bulwahn@39655
   862
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
bulwahn@39655
   863
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
bulwahn@39655
   864
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
bulwahn@39655
   865
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
bulwahn@39655
   866
bulwahn@39655
   867
code_pred tupled_step .
bulwahn@39655
   868
thm tupled_step.equation
bulwahn@39655
   869
wenzelm@63167
   870
subsection \<open>divmod\<close>
bulwahn@39655
   871
bulwahn@39655
   872
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
bulwahn@39655
   873
    "k < l \<Longrightarrow> divmod_rel k l 0 k"
bulwahn@39655
   874
  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
bulwahn@39655
   875
bulwahn@39655
   876
code_pred divmod_rel .
bulwahn@39655
   877
thm divmod_rel.equation
haftmann@56927
   878
value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
bulwahn@39655
   879
wenzelm@63167
   880
subsection \<open>Transforming predicate logic into logic programs\<close>
bulwahn@39655
   881
wenzelm@63167
   882
subsection \<open>Transforming functions into logic programs\<close>
bulwahn@39655
   883
definition
bulwahn@39655
   884
  "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
bulwahn@39655
   885
bulwahn@39655
   886
code_pred [inductify, skip_proof] case_f .
bulwahn@39655
   887
thm case_fP.equation
bulwahn@39655
   888
bulwahn@39655
   889
fun fold_map_idx where
bulwahn@39655
   890
  "fold_map_idx f i y [] = (y, [])"
bulwahn@39655
   891
| "fold_map_idx f i y (x # xs) =
bulwahn@39655
   892
 (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
bulwahn@39655
   893
 in (y'', x' # xs'))"
bulwahn@39655
   894
bulwahn@39655
   895
code_pred [inductify] fold_map_idx .
bulwahn@39655
   896
wenzelm@63167
   897
subsection \<open>Minimum\<close>
bulwahn@39655
   898
bulwahn@39655
   899
definition Min
bulwahn@39655
   900
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
bulwahn@39655
   901
bulwahn@39655
   902
code_pred [inductify] Min .
bulwahn@39655
   903
thm Min.equation
bulwahn@39655
   904
wenzelm@63167
   905
subsection \<open>Lexicographic order\<close>
wenzelm@63167
   906
text \<open>This example requires to handle the differences of sets and predicates in the predicate compiler,
wenzelm@63167
   907
or to have a copy of all definitions on predicates due to the set-predicate distinction.\<close>
bulwahn@39655
   908
haftmann@45970
   909
(*
bulwahn@39655
   910
declare lexord_def[code_pred_def]
bulwahn@39655
   911
code_pred [inductify] lexord .
bulwahn@39655
   912
code_pred [random_dseq inductify] lexord .
bulwahn@39655
   913
bulwahn@39655
   914
thm lexord.equation
bulwahn@39655
   915
thm lexord.random_dseq_equation
bulwahn@39655
   916
bulwahn@39655
   917
inductive less_than_nat :: "nat * nat => bool"
bulwahn@39655
   918
where
bulwahn@39655
   919
  "less_than_nat (0, x)"
bulwahn@39655
   920
| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
bulwahn@39655
   921
 
bulwahn@39655
   922
code_pred less_than_nat .
bulwahn@39655
   923
bulwahn@39655
   924
code_pred [dseq] less_than_nat .
bulwahn@39655
   925
code_pred [random_dseq] less_than_nat .
bulwahn@39655
   926
bulwahn@39655
   927
inductive test_lexord :: "nat list * nat list => bool"
bulwahn@39655
   928
where
bulwahn@39655
   929
  "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
bulwahn@39655
   930
bulwahn@39655
   931
code_pred test_lexord .
bulwahn@39655
   932
code_pred [dseq] test_lexord .
bulwahn@39655
   933
code_pred [random_dseq] test_lexord .
bulwahn@39655
   934
thm test_lexord.dseq_equation
bulwahn@39655
   935
thm test_lexord.random_dseq_equation
bulwahn@39655
   936
bulwahn@39655
   937
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
bulwahn@39655
   938
(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
bulwahn@39655
   939
bulwahn@39655
   940
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
bulwahn@39655
   941
(*
bulwahn@39655
   942
code_pred [inductify] lexn .
bulwahn@39655
   943
thm lexn.equation
bulwahn@39655
   944
*)
bulwahn@39655
   945
(*
bulwahn@39655
   946
code_pred [random_dseq inductify] lexn .
bulwahn@39655
   947
thm lexn.random_dseq_equation
bulwahn@39655
   948
bulwahn@39655
   949
values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
bulwahn@39655
   950
*)
haftmann@45970
   951
bulwahn@39655
   952
inductive has_length
bulwahn@39655
   953
where
bulwahn@39655
   954
  "has_length [] 0"
bulwahn@39655
   955
| "has_length xs i ==> has_length (x # xs) (Suc i)" 
bulwahn@39655
   956
bulwahn@39655
   957
lemma has_length:
bulwahn@39655
   958
  "has_length xs n = (length xs = n)"
bulwahn@39655
   959
proof (rule iffI)
bulwahn@39655
   960
  assume "has_length xs n"
bulwahn@39655
   961
  from this show "length xs = n"
bulwahn@39655
   962
    by (rule has_length.induct) auto
bulwahn@39655
   963
next
bulwahn@39655
   964
  assume "length xs = n"
bulwahn@39655
   965
  from this show "has_length xs n"
bulwahn@39655
   966
    by (induct xs arbitrary: n) (auto intro: has_length.intros)
bulwahn@39655
   967
qed
bulwahn@39655
   968
bulwahn@39655
   969
lemma lexn_intros [code_pred_intro]:
bulwahn@39655
   970
  "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
bulwahn@39655
   971
  "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
bulwahn@39655
   972
proof -
bulwahn@39655
   973
  assume "has_length xs i" "has_length ys i" "r (x, y)"
bulwahn@39655
   974
  from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
bulwahn@39655
   975
    unfolding lexn_conv Collect_def mem_def
nipkow@44890
   976
    by fastforce
bulwahn@39655
   977
next
bulwahn@39655
   978
  assume "lexn r i (xs, ys)"
bulwahn@39655
   979
  thm lexn_conv
bulwahn@39655
   980
  from this show "lexn r (Suc i) (x#xs, x#ys)"
bulwahn@39655
   981
    unfolding Collect_def mem_def lexn_conv
bulwahn@39655
   982
    apply auto
bulwahn@39655
   983
    apply (rule_tac x="x # xys" in exI)
bulwahn@39655
   984
    by auto
bulwahn@39655
   985
qed
bulwahn@39655
   986
bulwahn@39655
   987
code_pred [random_dseq] lexn
bulwahn@39655
   988
proof -
bulwahn@39655
   989
  fix r n xs ys
bulwahn@39655
   990
  assume 1: "lexn r n (xs, ys)"
bulwahn@39655
   991
  assume 2: "\<And>r' i x xs' y ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', y # ys') ==> has_length xs' i ==> has_length ys' i ==> r' (x, y) ==> thesis"
bulwahn@39655
   992
  assume 3: "\<And>r' i x xs' ys'. r = r' ==> n = Suc i ==> (xs, ys) = (x # xs', x # ys') ==> lexn r' i (xs', ys') ==> thesis"
bulwahn@39655
   993
  from 1 2 3 show thesis
bulwahn@39655
   994
    unfolding lexn_conv Collect_def mem_def
bulwahn@39655
   995
    apply (auto simp add: has_length)
bulwahn@39655
   996
    apply (case_tac xys)
bulwahn@39655
   997
    apply auto
nipkow@44890
   998
    apply fastforce
nipkow@44890
   999
    apply fastforce done
bulwahn@39655
  1000
qed
bulwahn@39655
  1001
bulwahn@39655
  1002
values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
bulwahn@39655
  1003
bulwahn@39655
  1004
code_pred [inductify, skip_proof] lex .
bulwahn@39655
  1005
thm lex.equation
bulwahn@39655
  1006
thm lex_def
bulwahn@39655
  1007
declare lenlex_conv[code_pred_def]
bulwahn@39655
  1008
code_pred [inductify, skip_proof] lenlex .
bulwahn@39655
  1009
thm lenlex.equation
bulwahn@39655
  1010
bulwahn@39655
  1011
code_pred [random_dseq inductify] lenlex .
bulwahn@39655
  1012
thm lenlex.random_dseq_equation
bulwahn@39655
  1013
bulwahn@39655
  1014
values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
bulwahn@39655
  1015
bulwahn@39655
  1016
thm lists.intros
bulwahn@39655
  1017
code_pred [inductify] lists .
bulwahn@39655
  1018
thm lists.equation
haftmann@45970
  1019
*)
wenzelm@63167
  1020
subsection \<open>AVL Tree\<close>
bulwahn@39655
  1021
blanchet@58310
  1022
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
bulwahn@39655
  1023
fun height :: "'a tree => nat" where
bulwahn@39655
  1024
"height ET = 0"
bulwahn@39655
  1025
| "height (MKT x l r h) = max (height l) (height r) + 1"
bulwahn@39655
  1026
bulwahn@39655
  1027
primrec avl :: "'a tree => bool"
bulwahn@39655
  1028
where
bulwahn@39655
  1029
  "avl ET = True"
bulwahn@39655
  1030
| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
bulwahn@39655
  1031
  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
bulwahn@39655
  1032
(*
bulwahn@39655
  1033
code_pred [inductify] avl .
bulwahn@39655
  1034
thm avl.equation*)
bulwahn@39655
  1035
bulwahn@39655
  1036
code_pred [new_random_dseq inductify] avl .
bulwahn@39655
  1037
thm avl.new_random_dseq_equation
bulwahn@40137
  1038
(* TODO: has highly non-deterministic execution time!
bulwahn@39655
  1039
bulwahn@39655
  1040
values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
bulwahn@40137
  1041
*)
bulwahn@39655
  1042
fun set_of
bulwahn@39655
  1043
where
bulwahn@39655
  1044
"set_of ET = {}"
bulwahn@39655
  1045
| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
bulwahn@39655
  1046
bulwahn@39655
  1047
fun is_ord :: "nat tree => bool"
bulwahn@39655
  1048
where
bulwahn@39655
  1049
"is_ord ET = True"
bulwahn@39655
  1050
| "is_ord (MKT n l r h) =
bulwahn@39655
  1051
 ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
bulwahn@39655
  1052
haftmann@45970
  1053
(* 
bulwahn@39655
  1054
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
bulwahn@39655
  1055
thm set_of.equation
bulwahn@39655
  1056
bulwahn@39655
  1057
code_pred (expected_modes: i => bool) [inductify] is_ord .
bulwahn@39655
  1058
thm is_ord_aux.equation
bulwahn@39655
  1059
thm is_ord.equation
haftmann@45970
  1060
*)
wenzelm@63167
  1061
subsection \<open>Definitions about Relations\<close>
haftmann@45970
  1062
(*
bulwahn@39655
  1063
code_pred (modes:
bulwahn@39655
  1064
  (i * i => bool) => i * i => bool,
bulwahn@39655
  1065
  (i * o => bool) => o * i => bool,
bulwahn@39655
  1066
  (i * o => bool) => i * i => bool,
bulwahn@39655
  1067
  (o * i => bool) => i * o => bool,
bulwahn@39655
  1068
  (o * i => bool) => i * i => bool,
bulwahn@39655
  1069
  (o * o => bool) => o * o => bool,
bulwahn@39655
  1070
  (o * o => bool) => i * o => bool,
bulwahn@39655
  1071
  (o * o => bool) => o * i => bool,
bulwahn@39655
  1072
  (o * o => bool) => i * i => bool) [inductify] converse .
bulwahn@39655
  1073
bulwahn@39655
  1074
thm converse.equation
griff@47433
  1075
code_pred [inductify] relcomp .
griff@47433
  1076
thm relcomp.equation
bulwahn@39655
  1077
code_pred [inductify] Image .
bulwahn@39655
  1078
thm Image.equation
bulwahn@39655
  1079
declare singleton_iff[code_pred_inline]
hoelzl@44928
  1080
declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
bulwahn@39655
  1081
bulwahn@39655
  1082
code_pred (expected_modes:
bulwahn@39655
  1083
  (o => bool) => o => bool,
bulwahn@39655
  1084
  (o => bool) => i * o => bool,
bulwahn@39655
  1085
  (o => bool) => o * i => bool,
bulwahn@39655
  1086
  (o => bool) => i => bool,
bulwahn@39655
  1087
  (i => bool) => i * o => bool,
bulwahn@39655
  1088
  (i => bool) => o * i => bool,
bulwahn@39655
  1089
  (i => bool) => i => bool) [inductify] Id_on .
bulwahn@39655
  1090
thm Id_on.equation
haftmann@46752
  1091
thm Domain_unfold
bulwahn@39655
  1092
code_pred (modes:
bulwahn@39655
  1093
  (o * o => bool) => o => bool,
bulwahn@39655
  1094
  (o * o => bool) => i => bool,
bulwahn@39655
  1095
  (i * o => bool) => i => bool) [inductify] Domain .
bulwahn@39655
  1096
thm Domain.equation
bulwahn@39655
  1097
haftmann@46752
  1098
thm Domain_converse [symmetric]
bulwahn@39655
  1099
code_pred (modes:
bulwahn@39655
  1100
  (o * o => bool) => o => bool,
bulwahn@39655
  1101
  (o * o => bool) => i => bool,
bulwahn@39655
  1102
  (o * i => bool) => i => bool) [inductify] Range .
bulwahn@39655
  1103
thm Range.equation
bulwahn@39655
  1104
bulwahn@39655
  1105
code_pred [inductify] Field .
bulwahn@39655
  1106
thm Field.equation
bulwahn@39655
  1107
bulwahn@39655
  1108
thm refl_on_def
bulwahn@39655
  1109
code_pred [inductify] refl_on .
bulwahn@39655
  1110
thm refl_on.equation
bulwahn@39655
  1111
code_pred [inductify] total_on .
bulwahn@39655
  1112
thm total_on.equation
bulwahn@39655
  1113
code_pred [inductify] antisym .
bulwahn@39655
  1114
thm antisym.equation
bulwahn@39655
  1115
code_pred [inductify] trans .
bulwahn@39655
  1116
thm trans.equation
bulwahn@39655
  1117
code_pred [inductify] single_valued .
bulwahn@39655
  1118
thm single_valued.equation
bulwahn@39655
  1119
thm inv_image_def
bulwahn@39655
  1120
code_pred [inductify] inv_image .
bulwahn@39655
  1121
thm inv_image.equation
haftmann@45970
  1122
*)
wenzelm@63167
  1123
subsection \<open>Inverting list functions\<close>
bulwahn@39655
  1124
blanchet@56679
  1125
code_pred [inductify, skip_proof] size_list' .
blanchet@56679
  1126
code_pred [new_random_dseq inductify] size_list' .
blanchet@56679
  1127
thm size_list'P.equation
blanchet@56679
  1128
thm size_list'P.new_random_dseq_equation
bulwahn@39655
  1129
blanchet@56679
  1130
values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
bulwahn@39655
  1131
bulwahn@39655
  1132
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
bulwahn@39655
  1133
thm concatP.equation
bulwahn@39655
  1134
bulwahn@39655
  1135
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
bulwahn@39655
  1136
values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
bulwahn@39655
  1137
bulwahn@39655
  1138
code_pred [dseq inductify] List.concat .
bulwahn@39655
  1139
thm concatP.dseq_equation
bulwahn@39655
  1140
bulwahn@39655
  1141
values [dseq 3] 3
bulwahn@39655
  1142
  "{xs. concatP xs ([0] :: nat list)}"
bulwahn@39655
  1143
bulwahn@39655
  1144
values [dseq 5] 3
bulwahn@39655
  1145
  "{xs. concatP xs ([1] :: int list)}"
bulwahn@39655
  1146
bulwahn@39655
  1147
values [dseq 5] 3
bulwahn@39655
  1148
  "{xs. concatP xs ([1] :: nat list)}"
bulwahn@39655
  1149
bulwahn@39655
  1150
values [dseq 5] 3
bulwahn@39655
  1151
  "{xs. concatP xs [(1::int), 2]}"
bulwahn@39655
  1152
bulwahn@39655
  1153
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
bulwahn@39655
  1154
thm hdP.equation
bulwahn@39655
  1155
values "{x. hdP [1, 2, (3::int)] x}"
bulwahn@39655
  1156
values "{(xs, x). hdP [1, 2, (3::int)] 1}"
bulwahn@39655
  1157
 
bulwahn@39655
  1158
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
bulwahn@39655
  1159
thm tlP.equation
bulwahn@39655
  1160
values "{x. tlP [1, 2, (3::nat)] x}"
bulwahn@39655
  1161
values "{x. tlP [1, 2, (3::int)] [3]}"
bulwahn@39655
  1162
bulwahn@39655
  1163
code_pred [inductify, skip_proof] last .
bulwahn@39655
  1164
thm lastP.equation
bulwahn@39655
  1165
bulwahn@39655
  1166
code_pred [inductify, skip_proof] butlast .
bulwahn@39655
  1167
thm butlastP.equation
bulwahn@39655
  1168
bulwahn@39655
  1169
code_pred [inductify, skip_proof] take .
bulwahn@39655
  1170
thm takeP.equation
bulwahn@39655
  1171
bulwahn@39655
  1172
code_pred [inductify, skip_proof] drop .
bulwahn@39655
  1173
thm dropP.equation
bulwahn@39655
  1174
code_pred [inductify, skip_proof] zip .
bulwahn@39655
  1175
thm zipP.equation
bulwahn@39655
  1176
bulwahn@39655
  1177
code_pred [inductify, skip_proof] upt .
haftmann@45970
  1178
(*
bulwahn@39655
  1179
code_pred [inductify, skip_proof] remdups .
bulwahn@39655
  1180
thm remdupsP.equation
bulwahn@39655
  1181
code_pred [dseq inductify] remdups .
bulwahn@39655
  1182
values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
haftmann@45970
  1183
*)
bulwahn@39655
  1184
code_pred [inductify, skip_proof] remove1 .
bulwahn@39655
  1185
thm remove1P.equation
bulwahn@39655
  1186
values "{xs. remove1P 1 xs [2, (3::int)]}"
bulwahn@39655
  1187
bulwahn@39655
  1188
code_pred [inductify, skip_proof] removeAll .
bulwahn@39655
  1189
thm removeAllP.equation
bulwahn@39655
  1190
code_pred [dseq inductify] removeAll .
bulwahn@39655
  1191
bulwahn@39655
  1192
values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
haftmann@45970
  1193
(*
bulwahn@39655
  1194
code_pred [inductify] distinct .
bulwahn@39655
  1195
thm distinct.equation
haftmann@45970
  1196
*)
bulwahn@39655
  1197
code_pred [inductify, skip_proof] replicate .
bulwahn@39655
  1198
thm replicateP.equation
bulwahn@39655
  1199
values 5 "{(n, xs). replicateP n (0::int) xs}"
bulwahn@39655
  1200
bulwahn@39655
  1201
code_pred [inductify, skip_proof] splice .
bulwahn@39655
  1202
thm splice.simps
bulwahn@39655
  1203
thm spliceP.equation
bulwahn@39655
  1204
bulwahn@39655
  1205
values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
bulwahn@39655
  1206
bulwahn@39655
  1207
code_pred [inductify, skip_proof] List.rev .
bulwahn@39655
  1208
code_pred [inductify] map .
bulwahn@39655
  1209
code_pred [inductify] foldr .
bulwahn@39655
  1210
code_pred [inductify] foldl .
bulwahn@39655
  1211
code_pred [inductify] filter .
bulwahn@39655
  1212
code_pred [random_dseq inductify] filter .
bulwahn@39655
  1213
wenzelm@63167
  1214
section \<open>Function predicate replacement\<close>
bulwahn@39655
  1215
wenzelm@63167
  1216
text \<open>
bulwahn@39655
  1217
If the mode analysis uses the functional mode, we
bulwahn@39655
  1218
replace predicates that resulted from functions again by their functions.
wenzelm@63167
  1219
\<close>
bulwahn@39655
  1220
bulwahn@39655
  1221
inductive test_append
bulwahn@39655
  1222
where
bulwahn@39655
  1223
  "List.append xs ys = zs ==> test_append xs ys zs"
bulwahn@39655
  1224
bulwahn@39655
  1225
code_pred [inductify, skip_proof] test_append .
bulwahn@39655
  1226
thm test_append.equation
bulwahn@39655
  1227
wenzelm@63167
  1228
text \<open>If append is not turned into a predicate, then the mode
wenzelm@63167
  1229
  o => o => i => bool could not be inferred.\<close>
bulwahn@39655
  1230
bulwahn@39655
  1231
values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
bulwahn@39655
  1232
wenzelm@63167
  1233
text \<open>If appendP is not reverted back to a function, then mode i => i => o => bool
wenzelm@63167
  1234
  fails after deleting the predicate equation.\<close>
bulwahn@39655
  1235
bulwahn@39655
  1236
declare appendP.equation[code del]
bulwahn@39655
  1237
bulwahn@39655
  1238
values "{xs::int list. test_append [1,2] [3,4] xs}"
bulwahn@39655
  1239
values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
bulwahn@39655
  1240
values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
bulwahn@39655
  1241
wenzelm@63167
  1242
text \<open>Redeclaring append.equation as code equation\<close>
bulwahn@39655
  1243
bulwahn@39655
  1244
declare appendP.equation[code]
bulwahn@39655
  1245
wenzelm@63167
  1246
subsection \<open>Function with tuples\<close>
bulwahn@39655
  1247
bulwahn@39655
  1248
fun append'
bulwahn@39655
  1249
where
bulwahn@39655
  1250
  "append' ([], ys) = ys"
bulwahn@39655
  1251
| "append' (x # xs, ys) = x # append' (xs, ys)"
bulwahn@39655
  1252
bulwahn@39655
  1253
inductive test_append'
bulwahn@39655
  1254
where
bulwahn@39655
  1255
  "append' (xs, ys) = zs ==> test_append' xs ys zs"
bulwahn@39655
  1256
bulwahn@39655
  1257
code_pred [inductify, skip_proof] test_append' .
bulwahn@39655
  1258
bulwahn@39655
  1259
thm test_append'.equation
bulwahn@39655
  1260
bulwahn@39655
  1261
values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
bulwahn@39655
  1262
bulwahn@39655
  1263
declare append'P.equation[code del]
bulwahn@39655
  1264
bulwahn@39655
  1265
values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
bulwahn@39655
  1266
wenzelm@63167
  1267
section \<open>Arithmetic examples\<close>
bulwahn@39655
  1268
wenzelm@63167
  1269
subsection \<open>Examples on nat\<close>
bulwahn@39655
  1270
bulwahn@39655
  1271
inductive plus_nat_test :: "nat => nat => nat => bool"
bulwahn@39655
  1272
where
bulwahn@39655
  1273
  "x + y = z ==> plus_nat_test x y z"
bulwahn@39655
  1274
bulwahn@39655
  1275
code_pred [inductify, skip_proof] plus_nat_test .
bulwahn@39655
  1276
code_pred [new_random_dseq inductify] plus_nat_test .
bulwahn@39655
  1277
bulwahn@39655
  1278
thm plus_nat_test.equation
bulwahn@39655
  1279
thm plus_nat_test.new_random_dseq_equation
bulwahn@39655
  1280
eberlm@66283
  1281
values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
eberlm@66283
  1282
values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
eberlm@66283
  1283
values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
bulwahn@39655
  1284
values [expected "{}"] "{y. plus_nat_test 9 y 8}"
eberlm@66283
  1285
values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
eberlm@66283
  1286
values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
bulwahn@39655
  1287
values [expected "{}"] "{x. plus_nat_test x 9 7}"
haftmann@51144
  1288
values [expected "{(0::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 0}"
eberlm@66283
  1289
values [expected "{(0, 1), (1::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 1}"
eberlm@66283
  1290
values [expected "{(0::nat, 5::nat), (1, 4), (2, 3), (3, 2), (4, 1), (5, 0)}"]
bulwahn@39655
  1291
  "{(x, y). plus_nat_test x y 5}"
bulwahn@39655
  1292
bulwahn@39655
  1293
inductive minus_nat_test :: "nat => nat => nat => bool"
bulwahn@39655
  1294
where
bulwahn@39655
  1295
  "x - y = z ==> minus_nat_test x y z"
bulwahn@39655
  1296
bulwahn@39655
  1297
code_pred [inductify, skip_proof] minus_nat_test .
bulwahn@39655
  1298
code_pred [new_random_dseq inductify] minus_nat_test .
bulwahn@39655
  1299
bulwahn@39655
  1300
thm minus_nat_test.equation
bulwahn@39655
  1301
thm minus_nat_test.new_random_dseq_equation
bulwahn@39655
  1302
bulwahn@39655
  1303
values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
eberlm@66283
  1304
values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
eberlm@66283
  1305
values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
eberlm@66283
  1306
values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
eberlm@66283
  1307
values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
bulwahn@39655
  1308
values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
bulwahn@39655
  1309
wenzelm@63167
  1310
subsection \<open>Examples on int\<close>
bulwahn@39655
  1311
bulwahn@39655
  1312
inductive plus_int_test :: "int => int => int => bool"
bulwahn@39655
  1313
where
bulwahn@39655
  1314
  "a + b = c ==> plus_int_test a b c"
bulwahn@39655
  1315
bulwahn@39655
  1316
code_pred [inductify, skip_proof] plus_int_test .
bulwahn@39655
  1317
code_pred [new_random_dseq inductify] plus_int_test .
bulwahn@39655
  1318
bulwahn@39655
  1319
thm plus_int_test.equation
bulwahn@39655
  1320
thm plus_int_test.new_random_dseq_equation
bulwahn@39655
  1321
bulwahn@39655
  1322
values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
bulwahn@39655
  1323
values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
bulwahn@39655
  1324
values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
bulwahn@39655
  1325
bulwahn@39655
  1326
inductive minus_int_test :: "int => int => int => bool"
bulwahn@39655
  1327
where
bulwahn@39655
  1328
  "a - b = c ==> minus_int_test a b c"
bulwahn@39655
  1329
bulwahn@39655
  1330
code_pred [inductify, skip_proof] minus_int_test .
bulwahn@39655
  1331
code_pred [new_random_dseq inductify] minus_int_test .
bulwahn@39655
  1332
bulwahn@39655
  1333
thm minus_int_test.equation
bulwahn@39655
  1334
thm minus_int_test.new_random_dseq_equation
bulwahn@39655
  1335
bulwahn@39655
  1336
values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
bulwahn@39655
  1337
values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
haftmann@40885
  1338
values [expected "{-1::int}"] "{b. minus_int_test 4 b 5}"
bulwahn@39655
  1339
wenzelm@63167
  1340
subsection \<open>minus on bool\<close>
bulwahn@39655
  1341
bulwahn@39655
  1342
inductive All :: "nat => bool"
bulwahn@39655
  1343
where
bulwahn@39655
  1344
  "All x"
bulwahn@39655
  1345
bulwahn@39655
  1346
inductive None :: "nat => bool"
bulwahn@39655
  1347
bulwahn@39655
  1348
definition "test_minus_bool x = (None x - All x)"
bulwahn@39655
  1349
bulwahn@39655
  1350
code_pred [inductify] test_minus_bool .
bulwahn@39655
  1351
thm test_minus_bool.equation
bulwahn@39655
  1352
bulwahn@39655
  1353
values "{x. test_minus_bool x}"
bulwahn@39655
  1354
wenzelm@63167
  1355
subsection \<open>Functions\<close>
bulwahn@39655
  1356
bulwahn@39655
  1357
fun partial_hd :: "'a list => 'a option"
bulwahn@39655
  1358
where
bulwahn@39655
  1359
  "partial_hd [] = Option.None"
bulwahn@39655
  1360
| "partial_hd (x # xs) = Some x"
bulwahn@39655
  1361
bulwahn@39655
  1362
inductive hd_predicate
bulwahn@39655
  1363
where
bulwahn@39655
  1364
  "partial_hd xs = Some x ==> hd_predicate xs x"
bulwahn@39655
  1365
bulwahn@39655
  1366
code_pred (expected_modes: i => i => bool, i => o => bool) hd_predicate .
bulwahn@39655
  1367
bulwahn@39655
  1368
thm hd_predicate.equation
bulwahn@39655
  1369
wenzelm@63167
  1370
subsection \<open>Locales\<close>
bulwahn@39655
  1371
bulwahn@39655
  1372
inductive hd_predicate2 :: "('a list => 'a option) => 'a list => 'a => bool"
bulwahn@39655
  1373
where
bulwahn@39655
  1374
  "partial_hd' xs = Some x ==> hd_predicate2 partial_hd' xs x"
bulwahn@39655
  1375
bulwahn@39655
  1376
bulwahn@39655
  1377
thm hd_predicate2.intros
bulwahn@39655
  1378
bulwahn@39655
  1379
code_pred (expected_modes: i => i => i => bool, i => i => o => bool) hd_predicate2 .
bulwahn@39655
  1380
thm hd_predicate2.equation
bulwahn@39655
  1381
bulwahn@39655
  1382
locale A = fixes partial_hd :: "'a list => 'a option" begin
bulwahn@39655
  1383
bulwahn@39655
  1384
inductive hd_predicate_in_locale :: "'a list => 'a => bool"
bulwahn@39655
  1385
where
bulwahn@39655
  1386
  "partial_hd xs = Some x ==> hd_predicate_in_locale xs x"
bulwahn@39655
  1387
bulwahn@39655
  1388
end
bulwahn@39655
  1389
wenzelm@63167
  1390
text \<open>The global introduction rules must be redeclared as introduction rules and then 
wenzelm@63167
  1391
  one could invoke code_pred.\<close>
bulwahn@39655
  1392
bulwahn@39657
  1393
declare A.hd_predicate_in_locale.intros [code_pred_intro]
bulwahn@39655
  1394
bulwahn@39655
  1395
code_pred (expected_modes: i => i => i => bool, i => i => o => bool) A.hd_predicate_in_locale
bulwahn@39657
  1396
by (auto elim: A.hd_predicate_in_locale.cases)
bulwahn@39655
  1397
    
bulwahn@39655
  1398
interpretation A partial_hd .
bulwahn@39655
  1399
thm hd_predicate_in_locale.intros
wenzelm@63167
  1400
text \<open>A locally compliant solution with a trivial interpretation fails, because
wenzelm@63167
  1401
the predicate compiler has very strict assumptions about the terms and their structure.\<close>
bulwahn@39655
  1402
 
bulwahn@39655
  1403
(*code_pred hd_predicate_in_locale .*)
bulwahn@39655
  1404
wenzelm@63167
  1405
section \<open>Integer example\<close>
bulwahn@39655
  1406
bulwahn@39655
  1407
definition three :: int
bulwahn@39655
  1408
where "three = 3"
bulwahn@39655
  1409
bulwahn@39655
  1410
inductive is_three
bulwahn@39655
  1411
where
bulwahn@39655
  1412
  "is_three three"
bulwahn@39655
  1413
bulwahn@39655
  1414
code_pred is_three .
bulwahn@39655
  1415
bulwahn@39655
  1416
thm is_three.equation
bulwahn@39655
  1417
wenzelm@63167
  1418
section \<open>String.literal example\<close>
bulwahn@39655
  1419
bulwahn@39655
  1420
definition Error_1
bulwahn@39655
  1421
where
bulwahn@39655
  1422
  "Error_1 = STR ''Error 1''"
bulwahn@39655
  1423
bulwahn@39655
  1424
definition Error_2
bulwahn@39655
  1425
where
bulwahn@39655
  1426
  "Error_2 = STR ''Error 2''"
bulwahn@39655
  1427
bulwahn@39655
  1428
inductive "is_error" :: "String.literal \<Rightarrow> bool"
bulwahn@39655
  1429
where
bulwahn@39655
  1430
  "is_error Error_1"
bulwahn@39655
  1431
| "is_error Error_2"
bulwahn@39655
  1432
bulwahn@39655
  1433
code_pred is_error .
bulwahn@39655
  1434
bulwahn@39655
  1435
thm is_error.equation
bulwahn@39655
  1436
bulwahn@39655
  1437
inductive is_error' :: "String.literal \<Rightarrow> bool"
bulwahn@39655
  1438
where
bulwahn@39655
  1439
  "is_error' (STR ''Error1'')"
bulwahn@39655
  1440
| "is_error' (STR ''Error2'')"
bulwahn@39655
  1441
bulwahn@39655
  1442
code_pred is_error' .
bulwahn@39655
  1443
bulwahn@39655
  1444
thm is_error'.equation
bulwahn@39655
  1445
blanchet@58310
  1446
datatype ErrorObject = Error String.literal int
bulwahn@39655
  1447
bulwahn@39655
  1448
inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
bulwahn@39655
  1449
where
bulwahn@39655
  1450
  "is_error'' (Error Error_1 3)"
bulwahn@39655
  1451
| "is_error'' (Error Error_2 4)"
bulwahn@39655
  1452
bulwahn@39655
  1453
code_pred is_error'' .
bulwahn@39655
  1454
bulwahn@39655
  1455
thm is_error''.equation
bulwahn@39655
  1456
wenzelm@63167
  1457
section \<open>Another function example\<close>
bulwahn@39655
  1458
bulwahn@39655
  1459
consts f :: "'a \<Rightarrow> 'a"
bulwahn@39655
  1460
bulwahn@39655
  1461
inductive fun_upd :: "(('a * 'b) * ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
bulwahn@39655
  1462
where
bulwahn@39655
  1463
  "fun_upd ((x, a), s) (s(x := f a))"
bulwahn@39655
  1464
bulwahn@39655
  1465
code_pred fun_upd .
bulwahn@39655
  1466
bulwahn@39655
  1467
thm fun_upd.equation
bulwahn@39655
  1468
wenzelm@63167
  1469
section \<open>Examples for detecting switches\<close>
bulwahn@39655
  1470
bulwahn@39655
  1471
inductive detect_switches1 where
bulwahn@39655
  1472
  "detect_switches1 [] []"
bulwahn@39655
  1473
| "detect_switches1 (x # xs) (y # ys)"
bulwahn@39655
  1474
bulwahn@39655
  1475
code_pred [detect_switches, skip_proof] detect_switches1 .
bulwahn@39655
  1476
bulwahn@39655
  1477
thm detect_switches1.equation
bulwahn@39655
  1478
bulwahn@39655
  1479
inductive detect_switches2 :: "('a => bool) => bool"
bulwahn@39655
  1480
where
bulwahn@39655
  1481
  "detect_switches2 P"
bulwahn@39655
  1482
bulwahn@39655
  1483
code_pred [detect_switches, skip_proof] detect_switches2 .
bulwahn@39655
  1484
thm detect_switches2.equation
bulwahn@39655
  1485
bulwahn@39655
  1486
inductive detect_switches3 :: "('a => bool) => 'a list => bool"
bulwahn@39655
  1487
where
bulwahn@39655
  1488
  "detect_switches3 P []"
bulwahn@39655
  1489
| "detect_switches3 P (x # xs)" 
bulwahn@39655
  1490
bulwahn@39655
  1491
code_pred [detect_switches, skip_proof] detect_switches3 .
bulwahn@39655
  1492
bulwahn@39655
  1493
thm detect_switches3.equation
bulwahn@39655
  1494
bulwahn@39655
  1495
inductive detect_switches4 :: "('a => bool) => 'a list => 'a list => bool"
bulwahn@39655
  1496
where
bulwahn@39655
  1497
  "detect_switches4 P [] []"
bulwahn@39655
  1498
| "detect_switches4 P (x # xs) (y # ys)"
bulwahn@39655
  1499
bulwahn@39655
  1500
code_pred [detect_switches, skip_proof] detect_switches4 .
bulwahn@39655
  1501
thm detect_switches4.equation
bulwahn@39655
  1502
bulwahn@39655
  1503
inductive detect_switches5 :: "('a => 'a => bool) => 'a list => 'a list => bool"
bulwahn@39655
  1504
where
bulwahn@39655
  1505
  "detect_switches5 P [] []"
bulwahn@39655
  1506
| "detect_switches5 P xs ys ==> P x y ==> detect_switches5 P (x # xs) (y # ys)"
bulwahn@39655
  1507
bulwahn@39655
  1508
code_pred [detect_switches, skip_proof] detect_switches5 .
bulwahn@39655
  1509
bulwahn@39655
  1510
thm detect_switches5.equation
bulwahn@39655
  1511
bulwahn@39655
  1512
inductive detect_switches6 :: "(('a => 'b => bool) * 'a list * 'b list) => bool"
bulwahn@39655
  1513
where
bulwahn@39655
  1514
  "detect_switches6 (P, [], [])"
bulwahn@39655
  1515
| "detect_switches6 (P, xs, ys) ==> P x y ==> detect_switches6 (P, x # xs, y # ys)"
bulwahn@39655
  1516
bulwahn@39655
  1517
code_pred [detect_switches, skip_proof] detect_switches6 .
bulwahn@39655
  1518
bulwahn@39655
  1519
inductive detect_switches7 :: "('a => bool) => ('b => bool) => ('a * 'b list) => bool"
bulwahn@39655
  1520
where
bulwahn@39655
  1521
  "detect_switches7 P Q (a, [])"
bulwahn@39655
  1522
| "P a ==> Q x ==> detect_switches7 P Q (a, x#xs)"
bulwahn@39655
  1523
bulwahn@39655
  1524
code_pred [skip_proof] detect_switches7 .
bulwahn@39655
  1525
bulwahn@39655
  1526
thm detect_switches7.equation
bulwahn@39655
  1527
bulwahn@39655
  1528
inductive detect_switches8 :: "nat => bool"
bulwahn@39655
  1529
where
bulwahn@39655
  1530
  "detect_switches8 0"
bulwahn@39655
  1531
| "x mod 2 = 0 ==> detect_switches8 (Suc x)"
bulwahn@39655
  1532
bulwahn@39655
  1533
code_pred [detect_switches, skip_proof] detect_switches8 .
bulwahn@39655
  1534
bulwahn@39655
  1535
thm detect_switches8.equation
bulwahn@39655
  1536
bulwahn@39655
  1537
inductive detect_switches9 :: "nat => nat => bool"
bulwahn@39655
  1538
where
bulwahn@39655
  1539
  "detect_switches9 0 0"
bulwahn@39655
  1540
| "detect_switches9 0 (Suc x)"
bulwahn@39655
  1541
| "detect_switches9 (Suc x) 0"
bulwahn@39655
  1542
| "x = y ==> detect_switches9 (Suc x) (Suc y)"
bulwahn@39655
  1543
| "c1 = c2 ==> detect_switches9 c1 c2"
bulwahn@39655
  1544
bulwahn@39655
  1545
code_pred [detect_switches, skip_proof] detect_switches9 .
bulwahn@39655
  1546
bulwahn@39655
  1547
thm detect_switches9.equation
bulwahn@39655
  1548
wenzelm@63167
  1549
text \<open>The higher-order predicate r is in an output term\<close>
bulwahn@39762
  1550
blanchet@58310
  1551
datatype result = Result bool
bulwahn@39762
  1552
bulwahn@39762
  1553
inductive fixed_relation :: "'a => bool"
bulwahn@39762
  1554
bulwahn@39762
  1555
inductive test_relation_in_output_terms :: "('a => bool) => 'a => result => bool"
bulwahn@39762
  1556
where
bulwahn@39762
  1557
  "test_relation_in_output_terms r x (Result (r x))"
bulwahn@39762
  1558
| "test_relation_in_output_terms r x (Result (fixed_relation x))"
bulwahn@39762
  1559
bulwahn@39762
  1560
code_pred test_relation_in_output_terms .
bulwahn@39762
  1561
bulwahn@39762
  1562
thm test_relation_in_output_terms.equation
bulwahn@39655
  1563
bulwahn@39655
  1564
wenzelm@63167
  1565
text \<open>
bulwahn@39765
  1566
  We want that the argument r is not treated as a higher-order relation, but simply as input.
wenzelm@63167
  1567
\<close>
bulwahn@39765
  1568
bulwahn@39765
  1569
inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
bulwahn@39765
  1570
where
bulwahn@39765
  1571
  "list_all r xs ==> test_uninterpreted_relation r xs"
bulwahn@39765
  1572
bulwahn@39765
  1573
code_pred (modes: i => i => bool) test_uninterpreted_relation .
bulwahn@39765
  1574
bulwahn@39765
  1575
thm test_uninterpreted_relation.equation
bulwahn@39765
  1576
bulwahn@39786
  1577
inductive list_ex'
bulwahn@39786
  1578
where
bulwahn@39786
  1579
  "P x ==> list_ex' P (x#xs)"
bulwahn@39786
  1580
| "list_ex' P xs ==> list_ex' P (x#xs)"
bulwahn@39786
  1581
bulwahn@39786
  1582
code_pred list_ex' .
bulwahn@39786
  1583
bulwahn@39786
  1584
inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
bulwahn@39786
  1585
where
bulwahn@39786
  1586
  "list_ex r xs ==> test_uninterpreted_relation2 r xs"
bulwahn@39786
  1587
| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
bulwahn@39786
  1588
wenzelm@63167
  1589
text \<open>Proof procedure cannot handle this situation yet.\<close>
bulwahn@39786
  1590
bulwahn@39786
  1591
code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
bulwahn@39786
  1592
bulwahn@39786
  1593
thm test_uninterpreted_relation2.equation
bulwahn@39786
  1594
bulwahn@39786
  1595
wenzelm@63167
  1596
text \<open>Trivial predicate\<close>
bulwahn@39784
  1597
bulwahn@39784
  1598
inductive implies_itself :: "'a => bool"
bulwahn@39784
  1599
where
bulwahn@39784
  1600
  "implies_itself x ==> implies_itself x"
bulwahn@39784
  1601
bulwahn@39784
  1602
code_pred implies_itself .
bulwahn@39765
  1603
wenzelm@63167
  1604
text \<open>Case expressions\<close>
bulwahn@39803
  1605
bulwahn@39803
  1606
definition
blanchet@55932
  1607
  "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
bulwahn@39803
  1608
blanchet@55932
  1609
code_pred [inductify] map_prods .
bulwahn@39765
  1610
bulwahn@39655
  1611
end