src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
author bulwahn
Wed Aug 25 16:59:50 2010 +0200 (2010-08-25)
changeset 38731 2c8a595af43e
parent 38728 182b180e9804
child 38735 cb9031a9dccf
permissions -rw-r--r--
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn@38074
     1
theory Code_Prolog_Examples
bulwahn@38117
     2
imports Code_Prolog
bulwahn@38074
     3
begin
bulwahn@38074
     4
bulwahn@38074
     5
section {* Example append *}
bulwahn@38074
     6
bulwahn@38074
     7
inductive append
bulwahn@38074
     8
where
bulwahn@38074
     9
  "append [] ys ys"
bulwahn@38074
    10
| "append xs ys zs ==> append (x # xs) ys (x # zs)"
bulwahn@38074
    11
bulwahn@38116
    12
values 3 "{(x, y, z). append x y z}"
bulwahn@38116
    13
bulwahn@38116
    14
bulwahn@38116
    15
section {* Example queens *}
bulwahn@38116
    16
bulwahn@38116
    17
inductive nodiag :: "int => int => int list => bool"
bulwahn@38116
    18
where
bulwahn@38116
    19
  "nodiag B D []"
bulwahn@38116
    20
| "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
bulwahn@38116
    21
bulwahn@38116
    22
text {*
bulwahn@38116
    23
qdelete(A, [A|L], L).
bulwahn@38116
    24
qdelete(X, [A|Z], [A|R]) :-
bulwahn@38116
    25
	qdelete(X, Z, R).
bulwahn@38116
    26
*}
bulwahn@38116
    27
bulwahn@38116
    28
inductive qdelete :: "int => int list => int list => bool"
bulwahn@38116
    29
where
bulwahn@38116
    30
  "qdelete A (A # L) L"
bulwahn@38116
    31
| "qdelete X Z R ==> qdelete X (A # Z) (A # R)"
bulwahn@38116
    32
bulwahn@38116
    33
text {*
bulwahn@38116
    34
qperm([], []).
bulwahn@38116
    35
qperm([X|Y], K) :-
bulwahn@38116
    36
	qdelete(U, [X|Y], Z),
bulwahn@38116
    37
	K = [U|V],
bulwahn@38116
    38
	qperm(Z, V).
bulwahn@38116
    39
*}
bulwahn@38116
    40
bulwahn@38116
    41
inductive qperm :: "int list => int list => bool"
bulwahn@38116
    42
where
bulwahn@38116
    43
  "qperm [] []"
bulwahn@38116
    44
| "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
bulwahn@38116
    45
bulwahn@38116
    46
text {*
bulwahn@38116
    47
safe([]).
bulwahn@38116
    48
safe([N|L]) :-
bulwahn@38116
    49
	nodiag(N, 1, L),
bulwahn@38116
    50
	safe(L).
bulwahn@38116
    51
*}
bulwahn@38116
    52
bulwahn@38116
    53
inductive safe :: "int list => bool"
bulwahn@38116
    54
where
bulwahn@38116
    55
  "safe []"
bulwahn@38116
    56
| "nodiag N 1 L ==> safe L ==> safe (N # L)"
bulwahn@38116
    57
bulwahn@38116
    58
text {*
bulwahn@38116
    59
queen(Data, Out) :-
bulwahn@38116
    60
	qperm(Data, Out),
bulwahn@38116
    61
	safe(Out)
bulwahn@38116
    62
*}
bulwahn@38116
    63
bulwahn@38116
    64
inductive queen :: "int list => int list => bool"
bulwahn@38116
    65
where
bulwahn@38116
    66
  "qperm Data Out ==> safe Out ==> queen Data Out"
bulwahn@38116
    67
bulwahn@38116
    68
inductive queen_9
bulwahn@38116
    69
where
bulwahn@38116
    70
  "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
bulwahn@38116
    71
bulwahn@38731
    72
values 10 "{ys. queen_9 ys}"
bulwahn@38116
    73
bulwahn@38116
    74
bulwahn@38116
    75
section {* Example symbolic derivation *}
bulwahn@38116
    76
bulwahn@38116
    77
hide_const Plus Pow
bulwahn@38116
    78
bulwahn@38116
    79
datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
bulwahn@38116
    80
  | Minus expr expr | Uminus expr | Pow expr int | Exp expr
bulwahn@38116
    81
bulwahn@38116
    82
text {*
bulwahn@38116
    83
bulwahn@38116
    84
d(U + V, X, DU + DV) :-
bulwahn@38116
    85
	cut,
bulwahn@38116
    86
	d(U, X, DU),
bulwahn@38116
    87
	d(V, X, DV).
bulwahn@38116
    88
d(U - V, X, DU - DV) :-
bulwahn@38116
    89
	cut,
bulwahn@38116
    90
	d(U, X, DU),
bulwahn@38116
    91
	d(V, X, DV).
bulwahn@38116
    92
d(U * V, X, DU * V + U * DV) :-
bulwahn@38116
    93
	cut,
bulwahn@38116
    94
	d(U, X, DU),
bulwahn@38116
    95
	d(V, X, DV).
bulwahn@38116
    96
d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
bulwahn@38116
    97
	cut,
bulwahn@38116
    98
	d(U, X, DU),
bulwahn@38116
    99
	d(V, X, DV).
bulwahn@38116
   100
d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
bulwahn@38116
   101
	cut,
bulwahn@38116
   102
	N1 is N - 1,
bulwahn@38116
   103
	d(U, X, DU).
bulwahn@38116
   104
d(-U, X, -DU) :-
bulwahn@38116
   105
	cut,
bulwahn@38116
   106
	d(U, X, DU).
bulwahn@38116
   107
d(exp(U), X, exp(U) * DU) :-
bulwahn@38116
   108
	cut,
bulwahn@38116
   109
	d(U, X, DU).
bulwahn@38116
   110
d(log(U), X, DU / U) :-
bulwahn@38116
   111
	cut,
bulwahn@38116
   112
	d(U, X, DU).
bulwahn@38116
   113
d(x, X, num(1)) :-
bulwahn@38116
   114
	cut.
bulwahn@38116
   115
d(num(_), _, num(0)).
bulwahn@38116
   116
bulwahn@38116
   117
*}
bulwahn@38116
   118
bulwahn@38116
   119
inductive d :: "expr => expr => expr => bool"
bulwahn@38116
   120
where
bulwahn@38116
   121
  "d U X DU ==> d V X DV ==> d (Plus U V) X (Plus DU DV)"
bulwahn@38116
   122
| "d U X DU ==> d V X DV ==> d (Minus U V) X (Minus DU DV)"
bulwahn@38116
   123
| "d U X DU ==> d V X DV ==> d (Mult U V) X (Plus (Mult DU V) (Mult U DV))"
bulwahn@38116
   124
| "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
   125
| "d U X DU ==> N1 = N - 1 ==> d (Pow U N) X (Mult DU (Mult (Num N) (Pow U N1)))"
bulwahn@38116
   126
| "d U X DU ==> d (Uminus U) X (Uminus DU)"
bulwahn@38116
   127
| "d U X DU ==> d (Exp U) X (Mult (Exp U) DU)"
bulwahn@38116
   128
| "d U X DU ==> d (Log U) X (Div DU U)"
bulwahn@38116
   129
| "d x X (Num 1)"
bulwahn@38116
   130
| "d (Num n) X (Num 0)"
bulwahn@38116
   131
bulwahn@38116
   132
text {*
bulwahn@38116
   133
ops8(E) :-
bulwahn@38116
   134
	d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
bulwahn@38116
   135
bulwahn@38116
   136
divide10(E) :-
bulwahn@38116
   137
	d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).
bulwahn@38116
   138
bulwahn@38116
   139
log10(E) :-
bulwahn@38116
   140
	d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
bulwahn@38116
   141
bulwahn@38116
   142
times10(E) :-
bulwahn@38116
   143
	d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
bulwahn@38116
   144
*}
bulwahn@38116
   145
bulwahn@38116
   146
inductive ops8 :: "expr => bool"
bulwahn@38116
   147
where
bulwahn@38116
   148
  "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
   149
bulwahn@38116
   150
inductive divide10
bulwahn@38116
   151
where
bulwahn@38116
   152
  "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
   153
bulwahn@38116
   154
inductive log10
bulwahn@38116
   155
where
bulwahn@38116
   156
 "d (Log (Log (Log (Log (Log (Log (Log (Log (Log (Log x)))))))))) x e ==> log10 e"
bulwahn@38116
   157
bulwahn@38116
   158
inductive times10
bulwahn@38116
   159
where
bulwahn@38116
   160
  "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
   161
bulwahn@38116
   162
values "{e. ops8 e}"
bulwahn@38116
   163
values "{e. divide10 e}"
bulwahn@38116
   164
values "{e. log10 e}"
bulwahn@38116
   165
values "{e. times10 e}"
bulwahn@38075
   166
bulwahn@38727
   167
section {* Example negation *}
bulwahn@38727
   168
bulwahn@38727
   169
datatype abc = A | B | C
bulwahn@38727
   170
bulwahn@38727
   171
inductive notB :: "abc => bool"
bulwahn@38727
   172
where
bulwahn@38727
   173
  "y \<noteq> B \<Longrightarrow> notB y"
bulwahn@38727
   174
bulwahn@38727
   175
ML {* Code_Prolog.options := {ensure_groundness = true} *}
bulwahn@38727
   176
bulwahn@38727
   177
values 2 "{y. notB y}"
bulwahn@38727
   178
bulwahn@38728
   179
inductive notAB :: "abc * abc \<Rightarrow> bool"
bulwahn@38728
   180
where
bulwahn@38728
   181
  "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
bulwahn@38728
   182
bulwahn@38728
   183
values 5 "{y. notAB y}"
bulwahn@38728
   184
bulwahn@38074
   185
end