src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
author bulwahn
Mon Mar 29 17:30:56 2010 +0200 (2010-03-29)
changeset 36040 fcd7bea01a93
parent 35954 d87d85a5d9ab
child 36055 537876d0fa62
permissions -rw-r--r--
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
bulwahn@35950
     1
theory Predicate_Compile_Examples
bulwahn@35954
     2
imports Predicate_Compile_Alternative_Defs
bulwahn@35950
     3
begin
bulwahn@35950
     4
bulwahn@35950
     5
subsection {* Basic predicates *}
bulwahn@35950
     6
bulwahn@35950
     7
inductive False' :: "bool"
bulwahn@35950
     8
bulwahn@35950
     9
code_pred (expected_modes: bool) False' .
bulwahn@35950
    10
code_pred [dseq] False' .
bulwahn@35950
    11
code_pred [random_dseq] False' .
bulwahn@35950
    12
bulwahn@35950
    13
values [expected "{}" pred] "{x. False'}"
bulwahn@35950
    14
values [expected "{}" dseq 1] "{x. False'}"
bulwahn@35950
    15
values [expected "{}" random_dseq 1, 1, 1] "{x. False'}"
bulwahn@35950
    16
bulwahn@35950
    17
value "False'"
bulwahn@35950
    18
bulwahn@35950
    19
bulwahn@35950
    20
inductive True' :: "bool"
bulwahn@35950
    21
where
bulwahn@35950
    22
  "True ==> True'"
bulwahn@35950
    23
bulwahn@35950
    24
code_pred True' .
bulwahn@35950
    25
code_pred [dseq] True' .
bulwahn@35950
    26
code_pred [random_dseq] True' .
bulwahn@35950
    27
bulwahn@35950
    28
thm True'.equation
bulwahn@35950
    29
thm True'.dseq_equation
bulwahn@35950
    30
thm True'.random_dseq_equation
bulwahn@35950
    31
values [expected "{()}" ]"{x. True'}"
bulwahn@35950
    32
values [expected "{}" dseq 0] "{x. True'}"
bulwahn@35950
    33
values [expected "{()}" dseq 1] "{x. True'}"
bulwahn@35950
    34
values [expected "{()}" dseq 2] "{x. True'}"
bulwahn@35950
    35
values [expected "{}" random_dseq 1, 1, 0] "{x. True'}"
bulwahn@35950
    36
values [expected "{}" random_dseq 1, 1, 1] "{x. True'}"
bulwahn@35950
    37
values [expected "{()}" random_dseq 1, 1, 2] "{x. True'}"
bulwahn@35950
    38
values [expected "{()}" random_dseq 1, 1, 3] "{x. True'}"
bulwahn@35950
    39
bulwahn@35950
    40
inductive EmptySet :: "'a \<Rightarrow> bool"
bulwahn@35950
    41
bulwahn@35950
    42
code_pred (expected_modes: o => bool, i => bool) EmptySet .
bulwahn@35950
    43
bulwahn@35950
    44
definition EmptySet' :: "'a \<Rightarrow> bool"
bulwahn@35950
    45
where "EmptySet' = {}"
bulwahn@35950
    46
bulwahn@35950
    47
code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' .
bulwahn@35950
    48
bulwahn@35950
    49
inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
bulwahn@35950
    50
bulwahn@35950
    51
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel .
bulwahn@35950
    52
bulwahn@35950
    53
inductive EmptyClosure :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@35950
    54
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@35950
    55
bulwahn@35950
    56
code_pred
bulwahn@35950
    57
  (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool,
bulwahn@35950
    58
         (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool,
bulwahn@35950
    59
         (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool,
bulwahn@35950
    60
         (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool,
bulwahn@35950
    61
         (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool,
bulwahn@35950
    62
         (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool,
bulwahn@35950
    63
         (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool,
bulwahn@35950
    64
         (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool)
bulwahn@35950
    65
  EmptyClosure .
bulwahn@35950
    66
bulwahn@35950
    67
thm EmptyClosure.equation
bulwahn@35950
    68
bulwahn@35950
    69
(* TODO: inductive package is broken!
bulwahn@35950
    70
inductive False'' :: "bool"
bulwahn@35950
    71
where
bulwahn@35950
    72
  "False \<Longrightarrow> False''"
bulwahn@35950
    73
bulwahn@35950
    74
code_pred (expected_modes: []) False'' .
bulwahn@35950
    75
bulwahn@35950
    76
inductive EmptySet'' :: "'a \<Rightarrow> bool"
bulwahn@35950
    77
where
bulwahn@35950
    78
  "False \<Longrightarrow> EmptySet'' x"
bulwahn@35950
    79
bulwahn@35950
    80
code_pred (expected_modes: [1]) EmptySet'' .
bulwahn@35950
    81
code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
bulwahn@35950
    82
*)
bulwahn@35950
    83
bulwahn@35950
    84
consts a' :: 'a
bulwahn@35950
    85
bulwahn@35950
    86
inductive Fact :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@35950
    87
where
bulwahn@35950
    88
"Fact a' a'"
bulwahn@35950
    89
bulwahn@35950
    90
code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact .
bulwahn@35950
    91
bulwahn@35950
    92
inductive zerozero :: "nat * nat => bool"
bulwahn@35950
    93
where
bulwahn@35950
    94
  "zerozero (0, 0)"
bulwahn@35950
    95
bulwahn@35950
    96
code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero .
bulwahn@35950
    97
code_pred [dseq] zerozero .
bulwahn@35950
    98
code_pred [random_dseq] zerozero .
bulwahn@35950
    99
bulwahn@35950
   100
thm zerozero.equation
bulwahn@35950
   101
thm zerozero.dseq_equation
bulwahn@35950
   102
thm zerozero.random_dseq_equation
bulwahn@35950
   103
bulwahn@35950
   104
text {* We expect the user to expand the tuples in the values command.
bulwahn@35950
   105
The following values command is not supported. *}
bulwahn@35950
   106
(*values "{x. zerozero x}" *)
bulwahn@35950
   107
text {* Instead, the user must type *}
bulwahn@35950
   108
values "{(x, y). zerozero (x, y)}"
bulwahn@35950
   109
bulwahn@35950
   110
values [expected "{}" dseq 0] "{(x, y). zerozero (x, y)}"
bulwahn@35950
   111
values [expected "{(0::nat, 0::nat)}" dseq 1] "{(x, y). zerozero (x, y)}"
bulwahn@35950
   112
values [expected "{(0::nat, 0::nat)}" dseq 2] "{(x, y). zerozero (x, y)}"
bulwahn@35950
   113
values [expected "{}" random_dseq 1, 1, 2] "{(x, y). zerozero (x, y)}"
bulwahn@35950
   114
values [expected "{(0::nat, 0:: nat)}" random_dseq 1, 1, 3] "{(x, y). zerozero (x, y)}"
bulwahn@35950
   115
bulwahn@35950
   116
inductive nested_tuples :: "((int * int) * int * int) => bool"
bulwahn@35950
   117
where
bulwahn@35950
   118
  "nested_tuples ((0, 1), 2, 3)"
bulwahn@35950
   119
bulwahn@35950
   120
code_pred nested_tuples .
bulwahn@35950
   121
bulwahn@35950
   122
inductive JamesBond :: "nat => int => code_numeral => bool"
bulwahn@35950
   123
where
bulwahn@35950
   124
  "JamesBond 0 0 7"
bulwahn@35950
   125
bulwahn@35950
   126
code_pred JamesBond .
bulwahn@35950
   127
bulwahn@35950
   128
values [expected "{(0::nat, 0::int , 7::code_numeral)}"] "{(a, b, c). JamesBond a b c}"
bulwahn@35950
   129
values [expected "{(0::nat, 7::code_numeral, 0:: int)}"] "{(a, c, b). JamesBond a b c}"
bulwahn@35950
   130
values [expected "{(0::int, 0::nat, 7::code_numeral)}"] "{(b, a, c). JamesBond a b c}"
bulwahn@35950
   131
values [expected "{(0::int, 7::code_numeral, 0::nat)}"] "{(b, c, a). JamesBond a b c}"
bulwahn@35950
   132
values [expected "{(7::code_numeral, 0::nat, 0::int)}"] "{(c, a, b). JamesBond a b c}"
bulwahn@35950
   133
values [expected "{(7::code_numeral, 0::int, 0::nat)}"] "{(c, b, a). JamesBond a b c}"
bulwahn@35950
   134
bulwahn@35950
   135
values [expected "{(7::code_numeral, 0::int)}"] "{(a, b). JamesBond 0 b a}"
bulwahn@35950
   136
values [expected "{(7::code_numeral, 0::nat)}"] "{(c, a). JamesBond a 0 c}"
bulwahn@35950
   137
values [expected "{(0::nat, 7::code_numeral)}"] "{(a, c). JamesBond a 0 c}"
bulwahn@35950
   138
bulwahn@35950
   139
bulwahn@35950
   140
subsection {* Alternative Rules *}
bulwahn@35950
   141
bulwahn@35950
   142
datatype char = C | D | E | F | G | H
bulwahn@35950
   143
bulwahn@35950
   144
inductive is_C_or_D
bulwahn@35950
   145
where
bulwahn@35950
   146
  "(x = C) \<or> (x = D) ==> is_C_or_D x"
bulwahn@35950
   147
bulwahn@35950
   148
code_pred (expected_modes: i => bool) is_C_or_D .
bulwahn@35950
   149
thm is_C_or_D.equation
bulwahn@35950
   150
bulwahn@35950
   151
inductive is_D_or_E
bulwahn@35950
   152
where
bulwahn@35950
   153
  "(x = D) \<or> (x = E) ==> is_D_or_E x"
bulwahn@35950
   154
bulwahn@35950
   155
lemma [code_pred_intro]:
bulwahn@35950
   156
  "is_D_or_E D"
bulwahn@35950
   157
by (auto intro: is_D_or_E.intros)
bulwahn@35950
   158
bulwahn@35950
   159
lemma [code_pred_intro]:
bulwahn@35950
   160
  "is_D_or_E E"
bulwahn@35950
   161
by (auto intro: is_D_or_E.intros)
bulwahn@35950
   162
bulwahn@35950
   163
code_pred (expected_modes: o => bool, i => bool) is_D_or_E
bulwahn@35950
   164
proof -
bulwahn@35950
   165
  case is_D_or_E
bulwahn@35950
   166
  from this(1) show thesis
bulwahn@35950
   167
  proof
bulwahn@35950
   168
    fix xa
bulwahn@35950
   169
    assume x: "x = xa"
bulwahn@35950
   170
    assume "xa = D \<or> xa = E"
bulwahn@35950
   171
    from this show thesis
bulwahn@35950
   172
    proof
bulwahn@35950
   173
      assume "xa = D" from this x is_D_or_E(2) show thesis by simp
bulwahn@35950
   174
    next
bulwahn@35950
   175
      assume "xa = E" from this x is_D_or_E(3) show thesis by simp
bulwahn@35950
   176
    qed
bulwahn@35950
   177
  qed
bulwahn@35950
   178
qed
bulwahn@35950
   179
bulwahn@35950
   180
thm is_D_or_E.equation
bulwahn@35950
   181
bulwahn@35950
   182
inductive is_F_or_G
bulwahn@35950
   183
where
bulwahn@35950
   184
  "x = F \<or> x = G ==> is_F_or_G x"
bulwahn@35950
   185
bulwahn@35950
   186
lemma [code_pred_intro]:
bulwahn@35950
   187
  "is_F_or_G F"
bulwahn@35950
   188
by (auto intro: is_F_or_G.intros)
bulwahn@35950
   189
bulwahn@35950
   190
lemma [code_pred_intro]:
bulwahn@35950
   191
  "is_F_or_G G"
bulwahn@35950
   192
by (auto intro: is_F_or_G.intros)
bulwahn@35950
   193
bulwahn@35950
   194
inductive is_FGH
bulwahn@35950
   195
where
bulwahn@35950
   196
  "is_F_or_G x ==> is_FGH x"
bulwahn@35950
   197
| "is_FGH H"
bulwahn@35950
   198
bulwahn@35950
   199
text {* Compilation of is_FGH requires elimination rule for is_F_or_G *}
bulwahn@35950
   200
bulwahn@35950
   201
code_pred (expected_modes: o => bool, i => bool) is_FGH
bulwahn@35950
   202
proof -
bulwahn@35950
   203
  case is_F_or_G
bulwahn@35950
   204
  from this(1) show thesis
bulwahn@35950
   205
  proof
bulwahn@35950
   206
    fix xa
bulwahn@35950
   207
    assume x: "x = xa"
bulwahn@35950
   208
    assume "xa = F \<or> xa = G"
bulwahn@35950
   209
    from this show thesis
bulwahn@35950
   210
    proof
bulwahn@35950
   211
      assume "xa = F"
bulwahn@35950
   212
      from this x is_F_or_G(2) show thesis by simp
bulwahn@35950
   213
    next
bulwahn@35950
   214
      assume "xa = G"
bulwahn@35950
   215
      from this x is_F_or_G(3) show thesis by simp
bulwahn@35950
   216
    qed
bulwahn@35950
   217
  qed
bulwahn@35950
   218
qed
bulwahn@35950
   219
bulwahn@35950
   220
subsection {* Preprocessor Inlining  *}
bulwahn@35950
   221
bulwahn@35950
   222
definition "equals == (op =)"
bulwahn@35950
   223
 
bulwahn@35950
   224
inductive zerozero' :: "nat * nat => bool" where
bulwahn@35950
   225
  "equals (x, y) (0, 0) ==> zerozero' (x, y)"
bulwahn@35950
   226
bulwahn@35950
   227
code_pred (expected_modes: i => bool) zerozero' .
bulwahn@35950
   228
bulwahn@35950
   229
lemma zerozero'_eq: "zerozero' x == zerozero x"
bulwahn@35950
   230
proof -
bulwahn@35950
   231
  have "zerozero' = zerozero"
bulwahn@35950
   232
    apply (auto simp add: mem_def)
bulwahn@35950
   233
    apply (cases rule: zerozero'.cases)
bulwahn@35950
   234
    apply (auto simp add: equals_def intro: zerozero.intros)
bulwahn@35950
   235
    apply (cases rule: zerozero.cases)
bulwahn@35950
   236
    apply (auto simp add: equals_def intro: zerozero'.intros)
bulwahn@35950
   237
    done
bulwahn@35950
   238
  from this show "zerozero' x == zerozero x" by auto
bulwahn@35950
   239
qed
bulwahn@35950
   240
bulwahn@35950
   241
declare zerozero'_eq [code_pred_inline]
bulwahn@35950
   242
bulwahn@35950
   243
definition "zerozero'' x == zerozero' x"
bulwahn@35950
   244
bulwahn@35950
   245
text {* if preprocessing fails, zerozero'' will not have all modes. *}
bulwahn@35950
   246
bulwahn@35950
   247
code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' .
bulwahn@35950
   248
bulwahn@35950
   249
subsection {* Sets and Numerals *}
bulwahn@35950
   250
bulwahn@35950
   251
definition
bulwahn@35950
   252
  "one_or_two = {Suc 0, (Suc (Suc 0))}"
bulwahn@35950
   253
bulwahn@35950
   254
code_pred [inductify] one_or_two .
bulwahn@35950
   255
bulwahn@35950
   256
code_pred [dseq] one_or_two .
bulwahn@35950
   257
code_pred [random_dseq] one_or_two .
bulwahn@35950
   258
thm one_or_two.dseq_equation
bulwahn@35950
   259
values [expected "{Suc 0::nat, 2::nat}"] "{x. one_or_two x}"
bulwahn@35950
   260
values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
bulwahn@35950
   261
bulwahn@35950
   262
inductive one_or_two' :: "nat => bool"
bulwahn@35950
   263
where
bulwahn@35950
   264
  "one_or_two' 1"
bulwahn@35950
   265
| "one_or_two' 2"
bulwahn@35950
   266
bulwahn@35950
   267
code_pred one_or_two' .
bulwahn@35950
   268
thm one_or_two'.equation
bulwahn@35950
   269
bulwahn@35950
   270
values "{x. one_or_two' x}"
bulwahn@35950
   271
bulwahn@35950
   272
definition one_or_two'':
bulwahn@35950
   273
  "one_or_two'' == {1, (2::nat)}"
bulwahn@35950
   274
bulwahn@35950
   275
code_pred [inductify] one_or_two'' .
bulwahn@35950
   276
thm one_or_two''.equation
bulwahn@35950
   277
bulwahn@35950
   278
values "{x. one_or_two'' x}"
bulwahn@35950
   279
bulwahn@35950
   280
subsection {* even predicate *}
bulwahn@35950
   281
bulwahn@35950
   282
inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
bulwahn@35950
   283
    "even 0"
bulwahn@35950
   284
  | "even n \<Longrightarrow> odd (Suc n)"
bulwahn@35950
   285
  | "odd n \<Longrightarrow> even (Suc n)"
bulwahn@35950
   286
bulwahn@35950
   287
code_pred (expected_modes: i => bool, o => bool) even .
bulwahn@35950
   288
code_pred [dseq] even .
bulwahn@35950
   289
code_pred [random_dseq] even .
bulwahn@35950
   290
bulwahn@35950
   291
thm odd.equation
bulwahn@35950
   292
thm even.equation
bulwahn@35950
   293
thm odd.dseq_equation
bulwahn@35950
   294
thm even.dseq_equation
bulwahn@35950
   295
thm odd.random_dseq_equation
bulwahn@35950
   296
thm even.random_dseq_equation
bulwahn@35950
   297
bulwahn@35950
   298
values "{x. even 2}"
bulwahn@35950
   299
values "{x. odd 2}"
bulwahn@35950
   300
values 10 "{n. even n}"
bulwahn@35950
   301
values 10 "{n. odd n}"
bulwahn@35950
   302
values [expected "{}" dseq 2] "{x. even 6}"
bulwahn@35950
   303
values [expected "{}" dseq 6] "{x. even 6}"
bulwahn@35950
   304
values [expected "{()}" dseq 7] "{x. even 6}"
bulwahn@35950
   305
values [dseq 2] "{x. odd 7}"
bulwahn@35950
   306
values [dseq 6] "{x. odd 7}"
bulwahn@35950
   307
values [dseq 7] "{x. odd 7}"
bulwahn@35950
   308
values [expected "{()}" dseq 8] "{x. odd 7}"
bulwahn@35950
   309
bulwahn@35950
   310
values [expected "{}" dseq 0] 8 "{x. even x}"
bulwahn@35950
   311
values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
bulwahn@35950
   312
values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
bulwahn@35950
   313
values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
bulwahn@35950
   314
values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
bulwahn@35950
   315
bulwahn@35950
   316
values [random_dseq 1, 1, 0] 8 "{x. even x}"
bulwahn@35950
   317
values [random_dseq 1, 1, 1] 8 "{x. even x}"
bulwahn@35950
   318
values [random_dseq 1, 1, 2] 8 "{x. even x}"
bulwahn@35950
   319
values [random_dseq 1, 1, 3] 8 "{x. even x}"
bulwahn@35950
   320
values [random_dseq 1, 1, 6] 8 "{x. even x}"
bulwahn@35950
   321
bulwahn@35950
   322
values [expected "{}" random_dseq 1, 1, 7] "{x. odd 7}"
bulwahn@35950
   323
values [random_dseq 1, 1, 8] "{x. odd 7}"
bulwahn@35950
   324
values [random_dseq 1, 1, 9] "{x. odd 7}"
bulwahn@35950
   325
bulwahn@35950
   326
definition odd' where "odd' x == \<not> even x"
bulwahn@35950
   327
bulwahn@35950
   328
code_pred (expected_modes: i => bool) [inductify] odd' .
bulwahn@35950
   329
code_pred [dseq inductify] odd' .
bulwahn@35950
   330
code_pred [random_dseq inductify] odd' .
bulwahn@35950
   331
bulwahn@35950
   332
values [expected "{}" dseq 2] "{x. odd' 7}"
bulwahn@35950
   333
values [expected "{()}" dseq 9] "{x. odd' 7}"
bulwahn@35950
   334
values [expected "{}" dseq 2] "{x. odd' 8}"
bulwahn@35950
   335
values [expected "{}" dseq 10] "{x. odd' 8}"
bulwahn@35950
   336
bulwahn@35950
   337
bulwahn@35950
   338
inductive is_even :: "nat \<Rightarrow> bool"
bulwahn@35950
   339
where
bulwahn@35950
   340
  "n mod 2 = 0 \<Longrightarrow> is_even n"
bulwahn@35950
   341
bulwahn@35950
   342
code_pred (expected_modes: i => bool) is_even .
bulwahn@35950
   343
bulwahn@35950
   344
subsection {* append predicate *}
bulwahn@35950
   345
bulwahn@35950
   346
inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
bulwahn@35950
   347
    "append [] xs xs"
bulwahn@35950
   348
  | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
bulwahn@35950
   349
bulwahn@35950
   350
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
bulwahn@35950
   351
  i => o => i => bool as suffix, i => i => i => bool) append .
bulwahn@35950
   352
code_pred [dseq] append .
bulwahn@35950
   353
code_pred [random_dseq] append .
bulwahn@35950
   354
bulwahn@35950
   355
thm append.equation
bulwahn@35950
   356
thm append.dseq_equation
bulwahn@35950
   357
thm append.random_dseq_equation
bulwahn@35950
   358
bulwahn@35950
   359
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
bulwahn@35950
   360
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
bulwahn@35950
   361
values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
bulwahn@35950
   362
bulwahn@35950
   363
values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@35950
   364
values [expected "{(([]::nat list), [Suc 0, 2, 3, 4, (5::nat)])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@35950
   365
values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@35950
   366
values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@35950
   367
values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
bulwahn@35950
   368
values [random_dseq 1, 1, 1] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@35950
   369
values [random_dseq 1, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@35950
   370
values [random_dseq 3, 1, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@35950
   371
values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@35950
   372
values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
bulwahn@35950
   373
bulwahn@35950
   374
value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
bulwahn@35950
   375
value [code] "Predicate.the (slice ([]::int list))"
bulwahn@35950
   376
bulwahn@35950
   377
bulwahn@35950
   378
text {* tricky case with alternative rules *}
bulwahn@35950
   379
bulwahn@35950
   380
inductive append2
bulwahn@35950
   381
where
bulwahn@35950
   382
  "append2 [] xs xs"
bulwahn@35950
   383
| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
bulwahn@35950
   384
bulwahn@35950
   385
lemma append2_Nil: "append2 [] (xs::'b list) xs"
bulwahn@35950
   386
  by (simp add: append2.intros(1))
bulwahn@35950
   387
bulwahn@35950
   388
lemmas [code_pred_intro] = append2_Nil append2.intros(2)
bulwahn@35950
   389
bulwahn@35950
   390
code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
bulwahn@35950
   391
  i => o => i => bool, i => i => i => bool) append2
bulwahn@35950
   392
proof -
bulwahn@35950
   393
  case append2
bulwahn@35950
   394
  from append2(1) show thesis
bulwahn@35950
   395
  proof
bulwahn@35950
   396
    fix xs
bulwahn@35950
   397
    assume "xa = []" "xb = xs" "xc = xs"
bulwahn@35950
   398
    from this append2(2) show thesis by simp
bulwahn@35950
   399
  next
bulwahn@35950
   400
    fix xs ys zs x
bulwahn@35950
   401
    assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
bulwahn@35950
   402
    from this append2(3) show thesis by fastsimp
bulwahn@35950
   403
  qed
bulwahn@35950
   404
qed
bulwahn@35950
   405
bulwahn@35950
   406
inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@35950
   407
where
bulwahn@35950
   408
  "tupled_append ([], xs, xs)"
bulwahn@35950
   409
| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
bulwahn@35950
   410
bulwahn@35950
   411
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@35950
   412
  i * o * i => bool, i * i * i => bool) tupled_append .
bulwahn@35950
   413
code_pred [random_dseq] tupled_append .
bulwahn@35950
   414
thm tupled_append.equation
bulwahn@35950
   415
bulwahn@35950
   416
values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"
bulwahn@35950
   417
bulwahn@35950
   418
inductive tupled_append'
bulwahn@35950
   419
where
bulwahn@35950
   420
"tupled_append' ([], xs, xs)"
bulwahn@35950
   421
| "[| ys = fst (xa, y); x # zs = snd (xa, y);
bulwahn@35950
   422
 tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
bulwahn@35950
   423
bulwahn@35950
   424
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@35950
   425
  i * o * i => bool, i * i * i => bool) tupled_append' .
bulwahn@35950
   426
thm tupled_append'.equation
bulwahn@35950
   427
bulwahn@35950
   428
inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@35950
   429
where
bulwahn@35950
   430
  "tupled_append'' ([], xs, xs)"
bulwahn@35950
   431
| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
bulwahn@35950
   432
bulwahn@35950
   433
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@35950
   434
  i * o * i => bool, i * i * i => bool) tupled_append'' .
bulwahn@35950
   435
thm tupled_append''.equation
bulwahn@35950
   436
bulwahn@35950
   437
inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
bulwahn@35950
   438
where
bulwahn@35950
   439
  "tupled_append''' ([], xs, xs)"
bulwahn@35950
   440
| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
bulwahn@35950
   441
bulwahn@35950
   442
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
bulwahn@35950
   443
  i * o * i => bool, i * i * i => bool) tupled_append''' .
bulwahn@35950
   444
thm tupled_append'''.equation
bulwahn@35950
   445
bulwahn@35950
   446
subsection {* map_ofP predicate *}
bulwahn@35950
   447
bulwahn@35950
   448
inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
bulwahn@35950
   449
where
bulwahn@35950
   450
  "map_ofP ((a, b)#xs) a b"
bulwahn@35950
   451
| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
bulwahn@35950
   452
bulwahn@35950
   453
code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP .
bulwahn@35950
   454
thm map_ofP.equation
bulwahn@35950
   455
bulwahn@35950
   456
subsection {* filter predicate *}
bulwahn@35950
   457
bulwahn@35950
   458
inductive filter1
bulwahn@35950
   459
for P
bulwahn@35950
   460
where
bulwahn@35950
   461
  "filter1 P [] []"
bulwahn@35950
   462
| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
bulwahn@35950
   463
| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
bulwahn@35950
   464
bulwahn@35950
   465
code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 .
bulwahn@35950
   466
code_pred [dseq] filter1 .
bulwahn@35950
   467
code_pred [random_dseq] filter1 .
bulwahn@35950
   468
bulwahn@35950
   469
thm filter1.equation
bulwahn@35950
   470
bulwahn@35950
   471
values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
bulwahn@35950
   472
values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
bulwahn@35950
   473
values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
bulwahn@35950
   474
bulwahn@35950
   475
inductive filter2
bulwahn@35950
   476
where
bulwahn@35950
   477
  "filter2 P [] []"
bulwahn@35950
   478
| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
bulwahn@35950
   479
| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
bulwahn@35950
   480
bulwahn@35950
   481
code_pred (expected_modes: (i => bool) => i => i => bool, (i => bool) => i => o => bool) filter2 .
bulwahn@35950
   482
code_pred [dseq] filter2 .
bulwahn@35950
   483
code_pred [random_dseq] filter2 .
bulwahn@35950
   484
bulwahn@35950
   485
thm filter2.equation
bulwahn@35950
   486
thm filter2.random_dseq_equation
bulwahn@35950
   487
bulwahn@35950
   488
(*
bulwahn@35950
   489
inductive filter3
bulwahn@35950
   490
for P
bulwahn@35950
   491
where
bulwahn@35950
   492
  "List.filter P xs = ys ==> filter3 P xs ys"
bulwahn@35950
   493
bulwahn@35950
   494
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@35950
   495
bulwahn@35950
   496
code_pred [dseq] filter3 .
bulwahn@35950
   497
thm filter3.dseq_equation
bulwahn@35950
   498
*)
bulwahn@35950
   499
(*
bulwahn@35950
   500
inductive filter4
bulwahn@35950
   501
where
bulwahn@35950
   502
  "List.filter P xs = ys ==> filter4 P xs ys"
bulwahn@35950
   503
bulwahn@35950
   504
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 .
bulwahn@35950
   505
(*code_pred [depth_limited] filter4 .*)
bulwahn@35950
   506
(*code_pred [random] filter4 .*)
bulwahn@35950
   507
*)
bulwahn@35950
   508
subsection {* reverse predicate *}
bulwahn@35950
   509
bulwahn@35950
   510
inductive rev where
bulwahn@35950
   511
    "rev [] []"
bulwahn@35950
   512
  | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
bulwahn@35950
   513
bulwahn@35950
   514
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev .
bulwahn@35950
   515
bulwahn@35950
   516
thm rev.equation
bulwahn@35950
   517
bulwahn@35950
   518
values "{xs. rev [0, 1, 2, 3::nat] xs}"
bulwahn@35950
   519
bulwahn@35950
   520
inductive tupled_rev where
bulwahn@35950
   521
  "tupled_rev ([], [])"
bulwahn@35950
   522
| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
bulwahn@35950
   523
bulwahn@35950
   524
code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev .
bulwahn@35950
   525
thm tupled_rev.equation
bulwahn@35950
   526
bulwahn@35950
   527
subsection {* partition predicate *}
bulwahn@35950
   528
bulwahn@35950
   529
inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
bulwahn@35950
   530
  for f where
bulwahn@35950
   531
    "partition f [] [] []"
bulwahn@35950
   532
  | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
bulwahn@35950
   533
  | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
bulwahn@35950
   534
bulwahn@35950
   535
code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool,
bulwahn@35950
   536
  (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool)
bulwahn@35950
   537
  partition .
bulwahn@35950
   538
code_pred [dseq] partition .
bulwahn@35950
   539
code_pred [random_dseq] partition .
bulwahn@35950
   540
bulwahn@35950
   541
values 10 "{(ys, zs). partition is_even
bulwahn@35950
   542
  [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
bulwahn@35950
   543
values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
bulwahn@35950
   544
values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
bulwahn@35950
   545
bulwahn@35950
   546
inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
bulwahn@35950
   547
  for f where
bulwahn@35950
   548
   "tupled_partition f ([], [], [])"
bulwahn@35950
   549
  | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
bulwahn@35950
   550
  | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
bulwahn@35950
   551
bulwahn@35950
   552
code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool,
bulwahn@35950
   553
  (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition .
bulwahn@35950
   554
bulwahn@35950
   555
thm tupled_partition.equation
bulwahn@35950
   556
bulwahn@35950
   557
lemma [code_pred_intro]:
bulwahn@35950
   558
  "r a b \<Longrightarrow> tranclp r a b"
bulwahn@35950
   559
  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
bulwahn@35950
   560
  by auto
bulwahn@35950
   561
bulwahn@35950
   562
subsection {* transitive predicate *}
bulwahn@35950
   563
bulwahn@35950
   564
text {* Also look at the tabled transitive closure in the Library *}
bulwahn@35950
   565
bulwahn@35950
   566
code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
bulwahn@35950
   567
  (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@35950
   568
  (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
bulwahn@35950
   569
proof -
bulwahn@35950
   570
  case tranclp
bulwahn@35950
   571
  from this converse_tranclpE[OF this(1)] show thesis by metis
bulwahn@35950
   572
qed
bulwahn@35950
   573
bulwahn@35950
   574
bulwahn@35950
   575
code_pred [dseq] tranclp .
bulwahn@35950
   576
code_pred [random_dseq] tranclp .
bulwahn@35950
   577
thm tranclp.equation
bulwahn@35950
   578
thm tranclp.random_dseq_equation
bulwahn@35950
   579
bulwahn@35950
   580
inductive rtrancl' :: "'a => 'a => ('a => 'a => bool) => bool" 
bulwahn@35950
   581
where
bulwahn@35950
   582
  "rtrancl' x x r"
bulwahn@35950
   583
| "r x y ==> rtrancl' y z r ==> rtrancl' x z r"
bulwahn@35950
   584
bulwahn@35950
   585
code_pred [random_dseq] rtrancl' .
bulwahn@35950
   586
bulwahn@35950
   587
thm rtrancl'.random_dseq_equation
bulwahn@35950
   588
bulwahn@35950
   589
inductive rtrancl'' :: "('a * 'a * ('a \<Rightarrow> 'a \<Rightarrow> bool)) \<Rightarrow> bool"  
bulwahn@35950
   590
where
bulwahn@35950
   591
  "rtrancl'' (x, x, r)"
bulwahn@35950
   592
| "r x y \<Longrightarrow> rtrancl'' (y, z, r) \<Longrightarrow> rtrancl'' (x, z, r)"
bulwahn@35950
   593
bulwahn@35950
   594
code_pred rtrancl'' .
bulwahn@35950
   595
bulwahn@35950
   596
inductive rtrancl''' :: "('a * ('a * 'a) * ('a * 'a => bool)) => bool" 
bulwahn@35950
   597
where
bulwahn@35950
   598
  "rtrancl''' (x, (x, x), r)"
bulwahn@35950
   599
| "r (x, y) ==> rtrancl''' (y, (z, z), r) ==> rtrancl''' (x, (z, z), r)"
bulwahn@35950
   600
bulwahn@35950
   601
code_pred rtrancl''' .
bulwahn@35950
   602
bulwahn@35950
   603
bulwahn@35950
   604
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
bulwahn@35950
   605
    "succ 0 1"
bulwahn@35950
   606
  | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
bulwahn@35950
   607
bulwahn@35950
   608
code_pred (modes: i => i => bool, i => o => bool, o => i => bool, o => o => bool) succ .
bulwahn@35950
   609
code_pred [random_dseq] succ .
bulwahn@35950
   610
thm succ.equation
bulwahn@35950
   611
thm succ.random_dseq_equation
bulwahn@35950
   612
bulwahn@35950
   613
values 10 "{(m, n). succ n m}"
bulwahn@35950
   614
values "{m. succ 0 m}"
bulwahn@35950
   615
values "{m. succ m 0}"
bulwahn@35950
   616
bulwahn@35950
   617
text {* values command needs mode annotation of the parameter succ
bulwahn@35950
   618
to disambiguate which mode is to be chosen. *} 
bulwahn@35950
   619
bulwahn@35950
   620
values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
bulwahn@35950
   621
values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
bulwahn@35950
   622
values 20 "{(n, m). tranclp succ n m}"
bulwahn@35950
   623
bulwahn@35950
   624
inductive example_graph :: "int => int => bool"
bulwahn@35950
   625
where
bulwahn@35950
   626
  "example_graph 0 1"
bulwahn@35950
   627
| "example_graph 1 2"
bulwahn@35950
   628
| "example_graph 1 3"
bulwahn@35950
   629
| "example_graph 4 7"
bulwahn@35950
   630
| "example_graph 4 5"
bulwahn@35950
   631
| "example_graph 5 6"
bulwahn@35950
   632
| "example_graph 7 6"
bulwahn@35950
   633
| "example_graph 7 8"
bulwahn@35950
   634
 
bulwahn@35950
   635
inductive not_reachable_in_example_graph :: "int => int => bool"
bulwahn@35950
   636
where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
bulwahn@35950
   637
bulwahn@35950
   638
code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
bulwahn@35950
   639
bulwahn@35950
   640
thm not_reachable_in_example_graph.equation
bulwahn@35950
   641
thm tranclp.equation
bulwahn@35950
   642
value "not_reachable_in_example_graph 0 3"
bulwahn@35950
   643
value "not_reachable_in_example_graph 4 8"
bulwahn@35950
   644
value "not_reachable_in_example_graph 5 6"
bulwahn@35950
   645
text {* rtrancl compilation is strange! *}
bulwahn@35950
   646
(*
bulwahn@35950
   647
value "not_reachable_in_example_graph 0 4"
bulwahn@35950
   648
value "not_reachable_in_example_graph 1 6"
bulwahn@35950
   649
value "not_reachable_in_example_graph 8 4"*)
bulwahn@35950
   650
bulwahn@35950
   651
code_pred [dseq] not_reachable_in_example_graph .
bulwahn@35950
   652
bulwahn@35950
   653
values [dseq 6] "{x. tranclp example_graph 0 3}"
bulwahn@35950
   654
bulwahn@35950
   655
values [dseq 0] "{x. not_reachable_in_example_graph 0 3}"
bulwahn@35950
   656
values [dseq 0] "{x. not_reachable_in_example_graph 0 4}"
bulwahn@35950
   657
values [dseq 20] "{x. not_reachable_in_example_graph 0 4}"
bulwahn@35950
   658
values [dseq 6] "{x. not_reachable_in_example_graph 0 3}"
bulwahn@35950
   659
values [dseq 3] "{x. not_reachable_in_example_graph 4 2}"
bulwahn@35950
   660
values [dseq 6] "{x. not_reachable_in_example_graph 4 2}"
bulwahn@35950
   661
bulwahn@35950
   662
bulwahn@35950
   663
inductive not_reachable_in_example_graph' :: "int => int => bool"
bulwahn@35950
   664
where "\<not> (rtranclp example_graph x y) ==> not_reachable_in_example_graph' x y"
bulwahn@35950
   665
bulwahn@35950
   666
code_pred not_reachable_in_example_graph' .
bulwahn@35950
   667
bulwahn@35950
   668
value "not_reachable_in_example_graph' 0 3"
bulwahn@35950
   669
(* value "not_reachable_in_example_graph' 0 5" would not terminate *)
bulwahn@35950
   670
bulwahn@35950
   671
bulwahn@35950
   672
(*values [depth_limited 0] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@35950
   673
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
bulwahn@35950
   674
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@35950
   675
(*values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
bulwahn@35950
   676
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@35950
   677
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@35950
   678
bulwahn@35950
   679
code_pred [dseq] not_reachable_in_example_graph' .
bulwahn@35950
   680
bulwahn@35950
   681
(*thm not_reachable_in_example_graph'.dseq_equation*)
bulwahn@35950
   682
bulwahn@35950
   683
(*values [dseq 0] "{x. not_reachable_in_example_graph' 0 3}"*)
bulwahn@35950
   684
(*values [depth_limited 3] "{x. not_reachable_in_example_graph' 0 3}"*) (* fails with undefined *)
bulwahn@35950
   685
(*values [depth_limited 5] "{x. not_reachable_in_example_graph' 0 3}"
bulwahn@35950
   686
values [depth_limited 1] "{x. not_reachable_in_example_graph' 0 4}"*)
bulwahn@35950
   687
(*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@35950
   688
(*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
bulwahn@35950
   689
bulwahn@35950
   690
bulwahn@35950
   691
subsection {* IMP *}
bulwahn@35950
   692
bulwahn@35950
   693
types
bulwahn@35950
   694
  var = nat
bulwahn@35950
   695
  state = "int list"
bulwahn@35950
   696
bulwahn@35950
   697
datatype com =
bulwahn@35950
   698
  Skip |
bulwahn@35950
   699
  Ass var "state => int" |
bulwahn@35950
   700
  Seq com com |
bulwahn@35950
   701
  IF "state => bool" com com |
bulwahn@35950
   702
  While "state => bool" com
bulwahn@35950
   703
bulwahn@35950
   704
inductive exec :: "com => state => state => bool" where
bulwahn@35950
   705
"exec Skip s s" |
bulwahn@35950
   706
"exec (Ass x e) s (s[x := e(s)])" |
bulwahn@35950
   707
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
bulwahn@35950
   708
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
bulwahn@35950
   709
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
bulwahn@35950
   710
"~b s ==> exec (While b c) s s" |
bulwahn@35950
   711
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
bulwahn@35950
   712
bulwahn@35950
   713
code_pred exec .
bulwahn@35950
   714
bulwahn@35950
   715
values "{t. exec
bulwahn@35950
   716
 (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
bulwahn@35950
   717
 [3,5] t}"
bulwahn@35950
   718
bulwahn@35950
   719
bulwahn@35950
   720
inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
bulwahn@35950
   721
"tupled_exec (Skip, s, s)" |
bulwahn@35950
   722
"tupled_exec (Ass x e, s, s[x := e(s)])" |
bulwahn@35950
   723
"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
bulwahn@35950
   724
"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
bulwahn@35950
   725
"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
bulwahn@35950
   726
"~b s ==> tupled_exec (While b c, s, s)" |
bulwahn@35950
   727
"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
bulwahn@35950
   728
bulwahn@35950
   729
code_pred tupled_exec .
bulwahn@35950
   730
bulwahn@35950
   731
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@35950
   732
bulwahn@35950
   733
subsection {* CCS *}
bulwahn@35950
   734
bulwahn@35950
   735
text{* This example formalizes finite CCS processes without communication or
bulwahn@35950
   736
recursion. For simplicity, labels are natural numbers. *}
bulwahn@35950
   737
bulwahn@35950
   738
datatype proc = nil | pre nat proc | or proc proc | par proc proc
bulwahn@35950
   739
bulwahn@35950
   740
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
bulwahn@35950
   741
"step (pre n p) n p" |
bulwahn@35950
   742
"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
bulwahn@35950
   743
"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
bulwahn@35950
   744
"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
bulwahn@35950
   745
"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
bulwahn@35950
   746
bulwahn@35950
   747
code_pred step .
bulwahn@35950
   748
bulwahn@35950
   749
inductive steps where
bulwahn@35950
   750
"steps p [] p" |
bulwahn@35950
   751
"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
bulwahn@35950
   752
bulwahn@35950
   753
code_pred steps .
bulwahn@35950
   754
bulwahn@35950
   755
values 3 
bulwahn@35950
   756
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
bulwahn@35950
   757
bulwahn@35950
   758
values 5
bulwahn@35950
   759
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
bulwahn@35950
   760
bulwahn@35950
   761
values 3 "{(a,q). step (par nil nil) a q}"
bulwahn@35950
   762
bulwahn@35950
   763
bulwahn@35950
   764
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
bulwahn@35950
   765
where
bulwahn@35950
   766
"tupled_step (pre n p, n, p)" |
bulwahn@35950
   767
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
bulwahn@35950
   768
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
bulwahn@35950
   769
"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
bulwahn@35950
   770
"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
bulwahn@35950
   771
bulwahn@35950
   772
code_pred tupled_step .
bulwahn@35950
   773
thm tupled_step.equation
bulwahn@35950
   774
bulwahn@35950
   775
subsection {* divmod *}
bulwahn@35950
   776
bulwahn@35950
   777
inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
bulwahn@35950
   778
    "k < l \<Longrightarrow> divmod_rel k l 0 k"
bulwahn@35950
   779
  | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
bulwahn@35950
   780
bulwahn@35950
   781
code_pred divmod_rel ..
bulwahn@35950
   782
thm divmod_rel.equation
bulwahn@35950
   783
value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
bulwahn@35950
   784
bulwahn@35950
   785
subsection {* Transforming predicate logic into logic programs *}
bulwahn@35950
   786
bulwahn@35950
   787
subsection {* Transforming functions into logic programs *}
bulwahn@35950
   788
definition
bulwahn@35950
   789
  "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
bulwahn@35950
   790
bulwahn@36040
   791
code_pred [inductify, skip_proof] case_f .
bulwahn@35950
   792
thm case_fP.equation
bulwahn@35950
   793
thm case_fP.intros
bulwahn@35950
   794
bulwahn@35950
   795
fun fold_map_idx where
bulwahn@35950
   796
  "fold_map_idx f i y [] = (y, [])"
bulwahn@35950
   797
| "fold_map_idx f i y (x # xs) =
bulwahn@35950
   798
 (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
bulwahn@35950
   799
 in (y'', x' # xs'))"
bulwahn@35950
   800
bulwahn@35950
   801
text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
bulwahn@35950
   802
(*code_pred [inductify, show_steps] fold_map_idx .*)
bulwahn@35950
   803
bulwahn@35950
   804
subsection {* Minimum *}
bulwahn@35950
   805
bulwahn@35950
   806
definition Min
bulwahn@35950
   807
where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
bulwahn@35950
   808
bulwahn@35950
   809
code_pred [inductify] Min .
bulwahn@35950
   810
thm Min.equation
bulwahn@35950
   811
bulwahn@35950
   812
subsection {* Lexicographic order *}
bulwahn@35950
   813
bulwahn@35950
   814
declare lexord_def[code_pred_def]
bulwahn@35950
   815
code_pred [inductify] lexord .
bulwahn@35950
   816
code_pred [random_dseq inductify] lexord .
bulwahn@35950
   817
bulwahn@35950
   818
thm lexord.equation
bulwahn@35950
   819
thm lexord.random_dseq_equation
bulwahn@35950
   820
bulwahn@35950
   821
inductive less_than_nat :: "nat * nat => bool"
bulwahn@35950
   822
where
bulwahn@35950
   823
  "less_than_nat (0, x)"
bulwahn@35950
   824
| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
bulwahn@35950
   825
 
bulwahn@35950
   826
code_pred less_than_nat .
bulwahn@35950
   827
bulwahn@35950
   828
code_pred [dseq] less_than_nat .
bulwahn@35950
   829
code_pred [random_dseq] less_than_nat .
bulwahn@35950
   830
bulwahn@35950
   831
inductive test_lexord :: "nat list * nat list => bool"
bulwahn@35950
   832
where
bulwahn@35950
   833
  "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
bulwahn@35950
   834
bulwahn@35950
   835
code_pred test_lexord .
bulwahn@35950
   836
code_pred [dseq] test_lexord .
bulwahn@35950
   837
code_pred [random_dseq] test_lexord .
bulwahn@35950
   838
thm test_lexord.dseq_equation
bulwahn@35950
   839
thm test_lexord.random_dseq_equation
bulwahn@35950
   840
bulwahn@35950
   841
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
bulwahn@35950
   842
(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
bulwahn@35950
   843
bulwahn@35950
   844
declare list.size(3,4)[code_pred_def]
bulwahn@35950
   845
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
bulwahn@35950
   846
(*
bulwahn@35950
   847
code_pred [inductify] lexn .
bulwahn@35950
   848
thm lexn.equation
bulwahn@35950
   849
*)
bulwahn@35950
   850
(*
bulwahn@35950
   851
code_pred [random_dseq inductify] lexn .
bulwahn@35950
   852
thm lexn.random_dseq_equation
bulwahn@35950
   853
bulwahn@35950
   854
values [random_dseq 4, 4, 6] 100 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
bulwahn@35950
   855
*)
bulwahn@35950
   856
inductive has_length
bulwahn@35950
   857
where
bulwahn@35950
   858
  "has_length [] 0"
bulwahn@35950
   859
| "has_length xs i ==> has_length (x # xs) (Suc i)" 
bulwahn@35950
   860
bulwahn@35950
   861
lemma has_length:
bulwahn@35950
   862
  "has_length xs n = (length xs = n)"
bulwahn@35950
   863
proof (rule iffI)
bulwahn@35950
   864
  assume "has_length xs n"
bulwahn@35950
   865
  from this show "length xs = n"
bulwahn@35950
   866
    by (rule has_length.induct) auto
bulwahn@35950
   867
next
bulwahn@35950
   868
  assume "length xs = n"
bulwahn@35950
   869
  from this show "has_length xs n"
bulwahn@35950
   870
    by (induct xs arbitrary: n) (auto intro: has_length.intros)
bulwahn@35950
   871
qed
bulwahn@35950
   872
bulwahn@35950
   873
lemma lexn_intros [code_pred_intro]:
bulwahn@35950
   874
  "has_length xs i ==> has_length ys i ==> r (x, y) ==> lexn r (Suc i) (x # xs, y # ys)"
bulwahn@35950
   875
  "lexn r i (xs, ys) ==> lexn r (Suc i) (x # xs, x # ys)"
bulwahn@35950
   876
proof -
bulwahn@35950
   877
  assume "has_length xs i" "has_length ys i" "r (x, y)"
bulwahn@35950
   878
  from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
bulwahn@35950
   879
    unfolding lexn_conv Collect_def mem_def
bulwahn@35950
   880
    by fastsimp
bulwahn@35950
   881
next
bulwahn@35950
   882
  assume "lexn r i (xs, ys)"
bulwahn@35950
   883
  thm lexn_conv
bulwahn@35950
   884
  from this show "lexn r (Suc i) (x#xs, x#ys)"
bulwahn@35950
   885
    unfolding Collect_def mem_def lexn_conv
bulwahn@35950
   886
    apply auto
bulwahn@35950
   887
    apply (rule_tac x="x # xys" in exI)
bulwahn@35950
   888
    by auto
bulwahn@35950
   889
qed
bulwahn@35950
   890
bulwahn@35950
   891
code_pred [random_dseq inductify] lexn
bulwahn@35950
   892
proof -
bulwahn@35950
   893
  fix r n xs ys
bulwahn@35950
   894
  assume 1: "lexn r n (xs, ys)"
bulwahn@35950
   895
  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@35950
   896
  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@35950
   897
  from 1 2 3 show thesis
bulwahn@35950
   898
    unfolding lexn_conv Collect_def mem_def
bulwahn@35950
   899
    apply (auto simp add: has_length)
bulwahn@35950
   900
    apply (case_tac xys)
bulwahn@35950
   901
    apply auto
bulwahn@35950
   902
    apply fastsimp
bulwahn@35950
   903
    apply fastsimp done
bulwahn@35950
   904
qed
bulwahn@35950
   905
bulwahn@35950
   906
bulwahn@35950
   907
values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
bulwahn@35950
   908
thm lenlex_conv
bulwahn@35950
   909
thm lex_conv
bulwahn@35950
   910
declare list.size(3,4)[code_pred_def]
bulwahn@35950
   911
(*code_pred [inductify, show_steps, show_intermediate_results] length .*)
bulwahn@35950
   912
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
bulwahn@36040
   913
code_pred [inductify, skip_proof] lex .
bulwahn@35950
   914
thm lex.equation
bulwahn@35950
   915
thm lex_def
bulwahn@35950
   916
declare lenlex_conv[code_pred_def]
bulwahn@36040
   917
code_pred [inductify, skip_proof] lenlex .
bulwahn@35950
   918
thm lenlex.equation
bulwahn@35950
   919
bulwahn@35950
   920
code_pred [random_dseq inductify] lenlex .
bulwahn@35950
   921
thm lenlex.random_dseq_equation
bulwahn@35950
   922
bulwahn@35950
   923
values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
bulwahn@35950
   924
thm lists.intros
bulwahn@35950
   925
bulwahn@35950
   926
code_pred [inductify] lists .
bulwahn@35950
   927
thm lists.equation
bulwahn@35950
   928
bulwahn@35950
   929
subsection {* AVL Tree *}
bulwahn@35950
   930
bulwahn@35950
   931
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
bulwahn@35950
   932
fun height :: "'a tree => nat" where
bulwahn@35950
   933
"height ET = 0"
bulwahn@35950
   934
| "height (MKT x l r h) = max (height l) (height r) + 1"
bulwahn@35950
   935
bulwahn@35950
   936
consts avl :: "'a tree => bool"
bulwahn@35950
   937
primrec
bulwahn@35950
   938
  "avl ET = True"
bulwahn@35950
   939
  "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
bulwahn@35950
   940
  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
bulwahn@35950
   941
(*
bulwahn@35950
   942
code_pred [inductify] avl .
bulwahn@35950
   943
thm avl.equation*)
bulwahn@35950
   944
bulwahn@35950
   945
code_pred [random_dseq inductify] avl .
bulwahn@35950
   946
thm avl.random_dseq_equation
bulwahn@35950
   947
bulwahn@35950
   948
values [random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
bulwahn@35950
   949
bulwahn@35950
   950
fun set_of
bulwahn@35950
   951
where
bulwahn@35950
   952
"set_of ET = {}"
bulwahn@35950
   953
| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
bulwahn@35950
   954
bulwahn@35950
   955
fun is_ord :: "nat tree => bool"
bulwahn@35950
   956
where
bulwahn@35950
   957
"is_ord ET = True"
bulwahn@35950
   958
| "is_ord (MKT n l r h) =
bulwahn@35950
   959
 ((\<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@35950
   960
bulwahn@35950
   961
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of .
bulwahn@35950
   962
thm set_of.equation
bulwahn@35950
   963
bulwahn@35950
   964
code_pred (expected_modes: i => bool) [inductify] is_ord .
bulwahn@35950
   965
thm is_ord_aux.equation
bulwahn@35950
   966
thm is_ord.equation
bulwahn@35950
   967
bulwahn@35950
   968
bulwahn@35950
   969
subsection {* Definitions about Relations *}
bulwahn@35950
   970
term "converse"
bulwahn@35950
   971
code_pred (modes:
bulwahn@35950
   972
  (i * i => bool) => i * i => bool,
bulwahn@35950
   973
  (i * o => bool) => o * i => bool,
bulwahn@35950
   974
  (i * o => bool) => i * i => bool,
bulwahn@35950
   975
  (o * i => bool) => i * o => bool,
bulwahn@35950
   976
  (o * i => bool) => i * i => bool,
bulwahn@35950
   977
  (o * o => bool) => o * o => bool,
bulwahn@35950
   978
  (o * o => bool) => i * o => bool,
bulwahn@35950
   979
  (o * o => bool) => o * i => bool,
bulwahn@35950
   980
  (o * o => bool) => i * i => bool) [inductify] converse .
bulwahn@35950
   981
bulwahn@35950
   982
thm converse.equation
bulwahn@35950
   983
code_pred [inductify] rel_comp .
bulwahn@35950
   984
thm rel_comp.equation
bulwahn@35950
   985
code_pred [inductify] Image .
bulwahn@35950
   986
thm Image.equation
bulwahn@35950
   987
declare singleton_iff[code_pred_inline]
bulwahn@35950
   988
declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
bulwahn@35950
   989
bulwahn@35950
   990
code_pred (expected_modes:
bulwahn@35950
   991
  (o => bool) => o => bool,
bulwahn@35950
   992
  (o => bool) => i * o => bool,
bulwahn@35950
   993
  (o => bool) => o * i => bool,
bulwahn@35950
   994
  (o => bool) => i => bool,
bulwahn@35950
   995
  (i => bool) => i * o => bool,
bulwahn@35950
   996
  (i => bool) => o * i => bool,
bulwahn@35950
   997
  (i => bool) => i => bool) [inductify] Id_on .
bulwahn@35950
   998
thm Id_on.equation
bulwahn@35950
   999
thm Domain_def
bulwahn@35950
  1000
code_pred (modes:
bulwahn@35950
  1001
  (o * o => bool) => o => bool,
bulwahn@35950
  1002
  (o * o => bool) => i => bool,
bulwahn@35950
  1003
  (i * o => bool) => i => bool) [inductify] Domain .
bulwahn@35950
  1004
thm Domain.equation
bulwahn@35950
  1005
bulwahn@35950
  1006
thm Range_def
bulwahn@35950
  1007
code_pred (modes:
bulwahn@35950
  1008
  (o * o => bool) => o => bool,
bulwahn@35950
  1009
  (o * o => bool) => i => bool,
bulwahn@35950
  1010
  (o * i => bool) => i => bool) [inductify] Range .
bulwahn@35950
  1011
thm Range.equation
bulwahn@35950
  1012
bulwahn@35950
  1013
code_pred [inductify] Field .
bulwahn@35950
  1014
thm Field.equation
bulwahn@35950
  1015
bulwahn@35950
  1016
thm refl_on_def
bulwahn@35950
  1017
code_pred [inductify] refl_on .
bulwahn@35950
  1018
thm refl_on.equation
bulwahn@35950
  1019
code_pred [inductify] total_on .
bulwahn@35950
  1020
thm total_on.equation
bulwahn@35950
  1021
code_pred [inductify] antisym .
bulwahn@35950
  1022
thm antisym.equation
bulwahn@35950
  1023
code_pred [inductify] trans .
bulwahn@35950
  1024
thm trans.equation
bulwahn@35950
  1025
code_pred [inductify] single_valued .
bulwahn@35950
  1026
thm single_valued.equation
bulwahn@35950
  1027
thm inv_image_def
bulwahn@35950
  1028
code_pred [inductify] inv_image .
bulwahn@35950
  1029
thm inv_image.equation
bulwahn@35950
  1030
bulwahn@35950
  1031
subsection {* Inverting list functions *}
bulwahn@35950
  1032
bulwahn@35950
  1033
(*code_pred [inductify] length .
bulwahn@35950
  1034
code_pred [random inductify] length .
bulwahn@35950
  1035
thm size_listP.equation
bulwahn@35950
  1036
thm size_listP.random_equation
bulwahn@35950
  1037
*)
bulwahn@35950
  1038
(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
bulwahn@35950
  1039
bulwahn@36040
  1040
code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
bulwahn@35950
  1041
thm concatP.equation
bulwahn@35950
  1042
bulwahn@35950
  1043
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
bulwahn@35950
  1044
values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}"
bulwahn@35950
  1045
bulwahn@35950
  1046
code_pred [dseq inductify] List.concat .
bulwahn@35950
  1047
thm concatP.dseq_equation
bulwahn@35950
  1048
bulwahn@35950
  1049
values [dseq 3] 3
bulwahn@35950
  1050
  "{xs. concatP xs ([0] :: nat list)}"
bulwahn@35950
  1051
bulwahn@35950
  1052
values [dseq 5] 3
bulwahn@35950
  1053
  "{xs. concatP xs ([1] :: int list)}"
bulwahn@35950
  1054
bulwahn@35950
  1055
values [dseq 5] 3
bulwahn@35950
  1056
  "{xs. concatP xs ([1] :: nat list)}"
bulwahn@35950
  1057
bulwahn@35950
  1058
values [dseq 5] 3
bulwahn@35950
  1059
  "{xs. concatP xs [(1::int), 2]}"
bulwahn@35950
  1060
bulwahn@35950
  1061
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd .
bulwahn@35950
  1062
thm hdP.equation
bulwahn@35950
  1063
values "{x. hdP [1, 2, (3::int)] x}"
bulwahn@35950
  1064
values "{(xs, x). hdP [1, 2, (3::int)] 1}"
bulwahn@35950
  1065
 
bulwahn@35950
  1066
code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl .
bulwahn@35950
  1067
thm tlP.equation
bulwahn@35950
  1068
values "{x. tlP [1, 2, (3::nat)] x}"
bulwahn@35950
  1069
values "{x. tlP [1, 2, (3::int)] [3]}"
bulwahn@35950
  1070
bulwahn@36040
  1071
code_pred [inductify, skip_proof] last .
bulwahn@35950
  1072
thm lastP.equation
bulwahn@35950
  1073
bulwahn@36040
  1074
code_pred [inductify, skip_proof] butlast .
bulwahn@35950
  1075
thm butlastP.equation
bulwahn@35950
  1076
bulwahn@36040
  1077
code_pred [inductify, skip_proof] take .
bulwahn@35950
  1078
thm takeP.equation
bulwahn@35950
  1079
bulwahn@36040
  1080
code_pred [inductify, skip_proof] drop .
bulwahn@35950
  1081
thm dropP.equation
bulwahn@36040
  1082
code_pred [inductify, skip_proof] zip .
bulwahn@35950
  1083
thm zipP.equation
bulwahn@35950
  1084
bulwahn@36040
  1085
code_pred [inductify, skip_proof] upt .
bulwahn@36040
  1086
code_pred [inductify, skip_proof] remdups .
bulwahn@35950
  1087
thm remdupsP.equation
bulwahn@35950
  1088
code_pred [dseq inductify] remdups .
bulwahn@35950
  1089
values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
bulwahn@35950
  1090
bulwahn@36040
  1091
code_pred [inductify, skip_proof] remove1 .
bulwahn@35950
  1092
thm remove1P.equation
bulwahn@35950
  1093
values "{xs. remove1P 1 xs [2, (3::int)]}"
bulwahn@35950
  1094
bulwahn@36040
  1095
code_pred [inductify, skip_proof] removeAll .
bulwahn@35950
  1096
thm removeAllP.equation
bulwahn@35950
  1097
code_pred [dseq inductify] removeAll .
bulwahn@35950
  1098
bulwahn@35950
  1099
values [dseq 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}"
bulwahn@35950
  1100
bulwahn@35950
  1101
code_pred [inductify] distinct .
bulwahn@35950
  1102
thm distinct.equation
bulwahn@36040
  1103
code_pred [inductify, skip_proof] replicate .
bulwahn@35950
  1104
thm replicateP.equation
bulwahn@35950
  1105
values 5 "{(n, xs). replicateP n (0::int) xs}"
bulwahn@35950
  1106
bulwahn@36040
  1107
code_pred [inductify, skip_proof] splice .
bulwahn@35950
  1108
thm splice.simps
bulwahn@35950
  1109
thm spliceP.equation
bulwahn@35950
  1110
bulwahn@35950
  1111
values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
bulwahn@35950
  1112
bulwahn@36040
  1113
code_pred [inductify, skip_proof] List.rev .
bulwahn@35950
  1114
code_pred [inductify] map .
bulwahn@35950
  1115
code_pred [inductify] foldr .
bulwahn@35950
  1116
code_pred [inductify] foldl .
bulwahn@35950
  1117
code_pred [inductify] filter .
bulwahn@35950
  1118
code_pred [random_dseq inductify] filter .
bulwahn@35950
  1119
bulwahn@35950
  1120
subsection {* Context Free Grammar *}
bulwahn@35950
  1121
bulwahn@35950
  1122
datatype alphabet = a | b
bulwahn@35950
  1123
bulwahn@35950
  1124
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
bulwahn@35950
  1125
  "[] \<in> S\<^isub>1"
bulwahn@35950
  1126
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
bulwahn@35950
  1127
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
bulwahn@35950
  1128
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
bulwahn@35950
  1129
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
bulwahn@35950
  1130
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
bulwahn@35950
  1131
bulwahn@35950
  1132
code_pred [inductify] S\<^isub>1p .
bulwahn@35950
  1133
code_pred [random_dseq inductify] S\<^isub>1p .
bulwahn@35950
  1134
thm S\<^isub>1p.equation
bulwahn@35950
  1135
thm S\<^isub>1p.random_dseq_equation
bulwahn@35950
  1136
bulwahn@35950
  1137
values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
bulwahn@35950
  1138
bulwahn@35950
  1139
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
bulwahn@35950
  1140
  "[] \<in> S\<^isub>2"
bulwahn@35950
  1141
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
bulwahn@35950
  1142
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
bulwahn@35950
  1143
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
bulwahn@35950
  1144
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
bulwahn@35950
  1145
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
bulwahn@35950
  1146
bulwahn@35950
  1147
code_pred [random_dseq inductify] S\<^isub>2p .
bulwahn@35950
  1148
thm S\<^isub>2p.random_dseq_equation
bulwahn@35950
  1149
thm A\<^isub>2p.random_dseq_equation
bulwahn@35950
  1150
thm B\<^isub>2p.random_dseq_equation
bulwahn@35950
  1151
bulwahn@35950
  1152
values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
bulwahn@35950
  1153
bulwahn@35950
  1154
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
bulwahn@35950
  1155
  "[] \<in> S\<^isub>3"
bulwahn@35950
  1156
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
bulwahn@35950
  1157
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
bulwahn@35950
  1158
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
bulwahn@35950
  1159
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
bulwahn@35950
  1160
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
bulwahn@35950
  1161
bulwahn@36040
  1162
code_pred [inductify, skip_proof] S\<^isub>3p .
bulwahn@35950
  1163
thm S\<^isub>3p.equation
bulwahn@35950
  1164
bulwahn@35950
  1165
values 10 "{x. S\<^isub>3p x}"
bulwahn@35950
  1166
bulwahn@35950
  1167
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
bulwahn@35950
  1168
  "[] \<in> S\<^isub>4"
bulwahn@35950
  1169
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
bulwahn@35950
  1170
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
bulwahn@35950
  1171
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
bulwahn@35950
  1172
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
bulwahn@35950
  1173
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
bulwahn@35950
  1174
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
bulwahn@35950
  1175
bulwahn@35950
  1176
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
bulwahn@35950
  1177
bulwahn@35950
  1178
subsection {* Lambda *}
bulwahn@35950
  1179
bulwahn@35950
  1180
datatype type =
bulwahn@35950
  1181
    Atom nat
bulwahn@35950
  1182
  | Fun type type    (infixr "\<Rightarrow>" 200)
bulwahn@35950
  1183
bulwahn@35950
  1184
datatype dB =
bulwahn@35950
  1185
    Var nat
bulwahn@35950
  1186
  | App dB dB (infixl "\<degree>" 200)
bulwahn@35950
  1187
  | Abs type dB
bulwahn@35950
  1188
bulwahn@35950
  1189
primrec
bulwahn@35950
  1190
  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
bulwahn@35950
  1191
where
bulwahn@35950
  1192
  "[]\<langle>i\<rangle> = None"
bulwahn@35950
  1193
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
bulwahn@35950
  1194
bulwahn@35950
  1195
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@35950
  1196
where
bulwahn@35950
  1197
  "nth_el' (x # xs) 0 x"
bulwahn@35950
  1198
| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
bulwahn@35950
  1199
bulwahn@35950
  1200
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
bulwahn@35950
  1201
  where
bulwahn@35950
  1202
    Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
bulwahn@35950
  1203
  | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
bulwahn@35950
  1204
  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
bulwahn@35950
  1205
bulwahn@35950
  1206
primrec
bulwahn@35950
  1207
  lift :: "[dB, nat] => dB"
bulwahn@35950
  1208
where
bulwahn@35950
  1209
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
bulwahn@35950
  1210
  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
bulwahn@35950
  1211
  | "lift (Abs T s) k = Abs T (lift s (k + 1))"
bulwahn@35950
  1212
bulwahn@35950
  1213
primrec
bulwahn@35950
  1214
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
bulwahn@35950
  1215
where
bulwahn@35950
  1216
    subst_Var: "(Var i)[s/k] =
bulwahn@35950
  1217
      (if k < i then Var (i - 1) else if i = k then s else Var i)"
bulwahn@35950
  1218
  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
bulwahn@35950
  1219
  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
bulwahn@35950
  1220
bulwahn@35950
  1221
inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
bulwahn@35950
  1222
  where
bulwahn@35950
  1223
    beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
bulwahn@35950
  1224
  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
bulwahn@35950
  1225
  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
bulwahn@35950
  1226
  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
bulwahn@35950
  1227
bulwahn@35950
  1228
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
bulwahn@35950
  1229
thm typing.equation
bulwahn@35950
  1230
bulwahn@35950
  1231
code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
bulwahn@35950
  1232
thm beta.equation
bulwahn@35950
  1233
bulwahn@35950
  1234
values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
bulwahn@35950
  1235
bulwahn@35950
  1236
definition "reduce t = Predicate.the (reduce' t)"
bulwahn@35950
  1237
bulwahn@35950
  1238
value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
bulwahn@35950
  1239
bulwahn@35950
  1240
code_pred [dseq] typing .
bulwahn@35950
  1241
code_pred [random_dseq] typing .
bulwahn@35950
  1242
bulwahn@35950
  1243
values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
bulwahn@35950
  1244
bulwahn@35950
  1245
subsection {* A minimal example of yet another semantics *}
bulwahn@35950
  1246
bulwahn@35950
  1247
text {* thanks to Elke Salecker *}
bulwahn@35950
  1248
bulwahn@35950
  1249
types
bulwahn@35950
  1250
  vname = nat
bulwahn@35950
  1251
  vvalue = int
bulwahn@35950
  1252
  var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
bulwahn@35950
  1253
bulwahn@35950
  1254
datatype ir_expr = 
bulwahn@35950
  1255
  IrConst vvalue
bulwahn@35950
  1256
| ObjAddr vname
bulwahn@35950
  1257
| Add ir_expr ir_expr
bulwahn@35950
  1258
bulwahn@35950
  1259
datatype val =
bulwahn@35950
  1260
  IntVal  vvalue
bulwahn@35950
  1261
bulwahn@35950
  1262
record  configuration =
bulwahn@35950
  1263
  Env :: var_assign
bulwahn@35950
  1264
bulwahn@35950
  1265
inductive eval_var ::
bulwahn@35950
  1266
  "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
bulwahn@35950
  1267
where
bulwahn@35950
  1268
  irconst: "eval_var (IrConst i) conf (IntVal i)"
bulwahn@35950
  1269
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
bulwahn@35950
  1270
| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
bulwahn@35950
  1271
bulwahn@35950
  1272
bulwahn@35950
  1273
code_pred eval_var .
bulwahn@35950
  1274
thm eval_var.equation
bulwahn@35950
  1275
bulwahn@35950
  1276
values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
bulwahn@35950
  1277
bulwahn@35950
  1278
end