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