src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 41956 c15ef1b85035
child 55447 aa41ecbdc205
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
bulwahn@38074
     1
theory Code_Prolog_Examples
wenzelm@41956
     2
imports "~~/src/HOL/Library/Code_Prolog"
bulwahn@38074
     3
begin
bulwahn@38074
     4
bulwahn@38074
     5
section {* Example append *}
bulwahn@38074
     6
bulwahn@38792
     7
bulwahn@38074
     8
inductive append
bulwahn@38074
     9
where
bulwahn@38074
    10
  "append [] ys ys"
bulwahn@38074
    11
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
bulwahn@38074
    12
bulwahn@38963
    13
setup {* Code_Prolog.map_code_options (K
bulwahn@38963
    14
  {ensure_groundness = false,
bulwahn@39800
    15
   limit_globally = NONE,
bulwahn@38963
    16
   limited_types = [],
bulwahn@38963
    17
   limited_predicates = [],
bulwahn@38963
    18
   replacing = [],
bulwahn@39463
    19
   manual_reorder = []}) *}
bulwahn@38792
    20
bulwahn@38792
    21
values "{(x, y, z). append x y z}"
bulwahn@38792
    22
bulwahn@39466
    23
values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
bulwahn@39466
    24
bulwahn@38116
    25
values 3 "{(x, y, z). append x y z}"
bulwahn@38116
    26
bulwahn@38950
    27
setup {* Code_Prolog.map_code_options (K
bulwahn@38949
    28
  {ensure_groundness = false,
bulwahn@39800
    29
   limit_globally = NONE,
bulwahn@38963
    30
   limited_types = [],
bulwahn@38963
    31
   limited_predicates = [],
bulwahn@38963
    32
   replacing = [],
bulwahn@39463
    33
   manual_reorder = []}) *}
bulwahn@38792
    34
bulwahn@38792
    35
values "{(x, y, z). append x y z}"
bulwahn@38792
    36
bulwahn@38950
    37
setup {* Code_Prolog.map_code_options (K
bulwahn@38949
    38
  {ensure_groundness = false,
bulwahn@39800
    39
   limit_globally = NONE,
bulwahn@38963
    40
   limited_types = [],
bulwahn@38963
    41
   limited_predicates = [],
bulwahn@38963
    42
   replacing = [],
bulwahn@39463
    43
   manual_reorder = []}) *}
bulwahn@38792
    44
bulwahn@38116
    45
bulwahn@38116
    46
section {* Example queens *}
bulwahn@38116
    47
bulwahn@38116
    48
inductive nodiag :: "int => int => int list => bool"
bulwahn@38116
    49
where
bulwahn@38116
    50
  "nodiag B D []"
bulwahn@38116
    51
| "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
bulwahn@38116
    52
bulwahn@38116
    53
text {*
bulwahn@38116
    54
qdelete(A, [A|L], L).
bulwahn@38116
    55
qdelete(X, [A|Z], [A|R]) :-
wenzelm@41457
    56
  qdelete(X, Z, R).
bulwahn@38116
    57
*}
bulwahn@38116
    58
bulwahn@38116
    59
inductive qdelete :: "int => int list => int list => bool"
bulwahn@38116
    60
where
bulwahn@38116
    61
  "qdelete A (A # L) L"
bulwahn@38116
    62
| "qdelete X Z R ==> qdelete X (A # Z) (A # R)"
bulwahn@38116
    63
bulwahn@38116
    64
text {*
bulwahn@38116
    65
qperm([], []).
bulwahn@38116
    66
qperm([X|Y], K) :-
wenzelm@41457
    67
  qdelete(U, [X|Y], Z),
wenzelm@41457
    68
  K = [U|V],
wenzelm@41457
    69
  qperm(Z, V).
bulwahn@38116
    70
*}
bulwahn@38116
    71
bulwahn@38116
    72
inductive qperm :: "int list => int list => bool"
bulwahn@38116
    73
where
bulwahn@38116
    74
  "qperm [] []"
bulwahn@38116
    75
| "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
bulwahn@38116
    76
bulwahn@38116
    77
text {*
bulwahn@38116
    78
safe([]).
bulwahn@38116
    79
safe([N|L]) :-
wenzelm@41457
    80
  nodiag(N, 1, L),
wenzelm@41457
    81
  safe(L).
bulwahn@38116
    82
*}
bulwahn@38116
    83
bulwahn@38116
    84
inductive safe :: "int list => bool"
bulwahn@38116
    85
where
bulwahn@38116
    86
  "safe []"
bulwahn@38116
    87
| "nodiag N 1 L ==> safe L ==> safe (N # L)"
bulwahn@38116
    88
bulwahn@38116
    89
text {*
bulwahn@38116
    90
queen(Data, Out) :-
wenzelm@41457
    91
  qperm(Data, Out),
wenzelm@41457
    92
  safe(Out)
bulwahn@38116
    93
*}
bulwahn@38116
    94
bulwahn@38116
    95
inductive queen :: "int list => int list => bool"
bulwahn@38116
    96
where
bulwahn@38116
    97
  "qperm Data Out ==> safe Out ==> queen Data Out"
bulwahn@38116
    98
bulwahn@38116
    99
inductive queen_9
bulwahn@38116
   100
where
bulwahn@38116
   101
  "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
bulwahn@38116
   102
bulwahn@38731
   103
values 10 "{ys. queen_9 ys}"
bulwahn@38116
   104
bulwahn@38116
   105
bulwahn@38116
   106
section {* Example symbolic derivation *}
bulwahn@38116
   107
nipkow@40271
   108
hide_const Pow
bulwahn@38116
   109
bulwahn@38116
   110
datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
bulwahn@38116
   111
  | Minus expr expr | Uminus expr | Pow expr int | Exp expr
bulwahn@38116
   112
bulwahn@38116
   113
text {*
bulwahn@38116
   114
bulwahn@38116
   115
d(U + V, X, DU + DV) :-
wenzelm@41457
   116
  cut,
wenzelm@41457
   117
  d(U, X, DU),
wenzelm@41457
   118
  d(V, X, DV).
bulwahn@38116
   119
d(U - V, X, DU - DV) :-
wenzelm@41457
   120
  cut,
wenzelm@41457
   121
  d(U, X, DU),
wenzelm@41457
   122
  d(V, X, DV).
bulwahn@38116
   123
d(U * V, X, DU * V + U * DV) :-
wenzelm@41457
   124
  cut,
wenzelm@41457
   125
  d(U, X, DU),
wenzelm@41457
   126
  d(V, X, DV).
bulwahn@38116
   127
d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
wenzelm@41457
   128
  cut,
wenzelm@41457
   129
  d(U, X, DU),
wenzelm@41457
   130
  d(V, X, DV).
bulwahn@38116
   131
d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
wenzelm@41457
   132
  cut,
wenzelm@41457
   133
  N1 is N - 1,
wenzelm@41457
   134
  d(U, X, DU).
bulwahn@38116
   135
d(-U, X, -DU) :-
wenzelm@41457
   136
  cut,
wenzelm@41457
   137
  d(U, X, DU).
bulwahn@38116
   138
d(exp(U), X, exp(U) * DU) :-
wenzelm@41457
   139
  cut,
wenzelm@41457
   140
  d(U, X, DU).
bulwahn@38116
   141
d(log(U), X, DU / U) :-
wenzelm@41457
   142
  cut,
wenzelm@41457
   143
  d(U, X, DU).
bulwahn@38116
   144
d(x, X, num(1)) :-
wenzelm@41457
   145
  cut.
bulwahn@38116
   146
d(num(_), _, num(0)).
bulwahn@38116
   147
bulwahn@38116
   148
*}
bulwahn@38116
   149
bulwahn@38116
   150
inductive d :: "expr => expr => expr => bool"
bulwahn@38116
   151
where
bulwahn@38116
   152
  "d U X DU ==> d V X DV ==> d (Plus U V) X (Plus DU DV)"
bulwahn@38116
   153
| "d U X DU ==> d V X DV ==> d (Minus U V) X (Minus DU DV)"
bulwahn@38116
   154
| "d U X DU ==> d V X DV ==> d (Mult U V) X (Plus (Mult DU V) (Mult U DV))"
bulwahn@38116
   155
| "d U X DU ==> d V X DV ==> d (Div U V) X (Div (Minus (Mult DU V) (Mult U DV)) (Pow V 2))"
bulwahn@38116
   156
| "d U X DU ==> N1 = N - 1 ==> d (Pow U N) X (Mult DU (Mult (Num N) (Pow U N1)))"
bulwahn@38116
   157
| "d U X DU ==> d (Uminus U) X (Uminus DU)"
bulwahn@38116
   158
| "d U X DU ==> d (Exp U) X (Mult (Exp U) DU)"
bulwahn@38116
   159
| "d U X DU ==> d (Log U) X (Div DU U)"
bulwahn@38116
   160
| "d x X (Num 1)"
bulwahn@38116
   161
| "d (Num n) X (Num 0)"
bulwahn@38116
   162
bulwahn@38116
   163
text {*
bulwahn@38116
   164
ops8(E) :-
wenzelm@41457
   165
  d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
bulwahn@38116
   166
bulwahn@38116
   167
divide10(E) :-
wenzelm@41457
   168
  d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
bulwahn@38116
   169
bulwahn@38116
   170
log10(E) :-
wenzelm@41457
   171
  d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
bulwahn@38116
   172
bulwahn@38116
   173
times10(E) :-
wenzelm@41457
   174
  d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
bulwahn@38116
   175
*}
bulwahn@38116
   176
bulwahn@38116
   177
inductive ops8 :: "expr => bool"
bulwahn@38116
   178
where
bulwahn@38116
   179
  "d (Mult (Plus x (Num 1)) (Mult (Plus (Pow x 2) (Num 2)) (Plus (Pow x 3) (Num 3)))) x e ==> ops8 e"
bulwahn@38116
   180
bulwahn@38116
   181
inductive divide10
bulwahn@38116
   182
where
bulwahn@38116
   183
  "d (Div (Div (Div (Div (Div (Div (Div (Div (Div x x) x) x) x) x) x) x) x) x) x e ==> divide10 e"
bulwahn@38116
   184
bulwahn@38116
   185
inductive log10
bulwahn@38116
   186
where
bulwahn@38116
   187
 "d (Log (Log (Log (Log (Log (Log (Log (Log (Log (Log x)))))))))) x e ==> log10 e"
bulwahn@38116
   188
bulwahn@38116
   189
inductive times10
bulwahn@38116
   190
where
bulwahn@38116
   191
  "d (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult (Mult x x) x) x) x) x) x) x) x) x) x e ==> times10 e"
bulwahn@38116
   192
bulwahn@38116
   193
values "{e. ops8 e}"
bulwahn@38116
   194
values "{e. divide10 e}"
bulwahn@38116
   195
values "{e. log10 e}"
bulwahn@38116
   196
values "{e. times10 e}"
bulwahn@38075
   197
bulwahn@38727
   198
section {* Example negation *}
bulwahn@38727
   199
bulwahn@38727
   200
datatype abc = A | B | C
bulwahn@38727
   201
bulwahn@38727
   202
inductive notB :: "abc => bool"
bulwahn@38727
   203
where
bulwahn@38727
   204
  "y \<noteq> B \<Longrightarrow> notB y"
bulwahn@38727
   205
bulwahn@38963
   206
setup {* Code_Prolog.map_code_options (K
bulwahn@38963
   207
  {ensure_groundness = true,
bulwahn@39800
   208
   limit_globally = NONE,
bulwahn@38963
   209
   limited_types = [],
bulwahn@38963
   210
   limited_predicates = [],
bulwahn@38963
   211
   replacing = [],
bulwahn@39463
   212
   manual_reorder = []}) *}
bulwahn@38727
   213
bulwahn@38727
   214
values 2 "{y. notB y}"
bulwahn@38727
   215
bulwahn@38728
   216
inductive notAB :: "abc * abc \<Rightarrow> bool"
bulwahn@38728
   217
where
bulwahn@38728
   218
  "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
bulwahn@38728
   219
bulwahn@38728
   220
values 5 "{y. notAB y}"
bulwahn@38728
   221
bulwahn@38735
   222
section {* Example prolog conform variable names *}
bulwahn@38735
   223
bulwahn@38735
   224
inductive equals :: "abc => abc => bool"
bulwahn@38735
   225
where
bulwahn@38735
   226
  "equals y' y'"
bulwahn@38791
   227
bulwahn@38735
   228
values 1 "{(y, z). equals y z}"
bulwahn@38735
   229
bulwahn@38074
   230
end