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