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