src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

 theory Code_Prolog_Examples
 imports "~~/src/HOL/Library/Code_Prolog"
 begin
 
-section {* Example append *}
+section \<open>Example append\<close>
 
 
 inductive append
 where
   "append [] ys ys"
 | "append xs ys zs ==> append (x # xs) ys (x # zs)"
 
-setup {* Code_Prolog.map_code_options (K
+setup \<open>Code_Prolog.map_code_options (K
   {ensure_groundness = false,
    limit_globally = NONE,
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = []}) *}
+   manual_reorder = []})\<close>
 
 values_prolog "{(x, y, z). append x y z}"
 
 values_prolog 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
 
 values_prolog 3 "{(x, y, z). append x y z}"
 
-setup {* Code_Prolog.map_code_options (K
+setup \<open>Code_Prolog.map_code_options (K
   {ensure_groundness = false,
    limit_globally = NONE,
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = []}) *}
+   manual_reorder = []})\<close>
 
 values_prolog "{(x, y, z). append x y z}"
 
-setup {* Code_Prolog.map_code_options (K
+setup \<open>Code_Prolog.map_code_options (K
   {ensure_groundness = false,
    limit_globally = NONE,
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = []}) *}
-
-
-section {* Example queens *}
+   manual_reorder = []})\<close>
+
+
+section \<open>Example queens\<close>
 
 inductive nodiag :: "int => int => int list => bool"
 where
   "nodiag B D []"
 | "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
 
-text {*
+text \<open>
 qdelete(A, [A|L], L).
 qdelete(X, [A|Z], [A|R]) :-
   qdelete(X, Z, R).
-*}
+\<close>
 
 inductive qdelete :: "int => int list => int list => bool"
 where
   "qdelete A (A # L) L"
 | "qdelete X Z R ==> qdelete X (A # Z) (A # R)"
 
-text {*
+text \<open>
 qperm([], []).
 qperm([X|Y], K) :-
   qdelete(U, [X|Y], Z),
   K = [U|V],
   qperm(Z, V).
-*}
+\<close>
 
 inductive qperm :: "int list => int list => bool"
 where
   "qperm [] []"
 | "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
 
-text {*
+text \<open>
 safe([]).
 safe([N|L]) :-
   nodiag(N, 1, L),
   safe(L).
-*}
+\<close>
 
 inductive safe :: "int list => bool"
 where
   "safe []"
 | "nodiag N 1 L ==> safe L ==> safe (N # L)"
 
-text {*
+text \<open>
 queen(Data, Out) :-
   qperm(Data, Out),
   safe(Out)
-*}
+\<close>
 
 inductive queen :: "int list => int list => bool"
 where
   "qperm Data Out ==> safe Out ==> queen Data Out"
 

   "queen [1,2,3,4,5,6,7,8,9] ys ==> queen_9 ys"
 
 values_prolog 10 "{ys. queen_9 ys}"
 
 
-section {* Example symbolic derivation *}
+section \<open>Example symbolic derivation\<close>
 
 hide_const Pow
 
 datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
 
-text {*
+text \<open>
 
 d(U + V, X, DU + DV) :-
   cut,
   d(U, X, DU),
   d(V, X, DV).

   d(U, X, DU).
 d(x, X, num(1)) :-
   cut.
 d(num(_), _, num(0)).
 
-*}
+\<close>
 
 inductive d :: "expr => expr => expr => bool"
 where
   "d U X DU ==> d V X DV ==> d (Plus U V) X (Plus DU DV)"
 | "d U X DU ==> d V X DV ==> d (Minus U V) X (Minus DU DV)"

 | "d U X DU ==> d (Exp U) X (Mult (Exp U) DU)"
 | "d U X DU ==> d (Log U) X (Div DU U)"
 | "d x X (Num 1)"
 | "d (Num n) X (Num 0)"
 
-text {*
+text \<open>
 ops8(E) :-
   d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, E).
 
 divide10(E) :-
   d(((((((((x / x) / x) / x) / x) / x) / x) / x) / x) / x, x, E).

 log10(E) :-
   d(log(log(log(log(log(log(log(log(log(log(x)))))))))), x, E).
 
 times10(E) :-
   d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
-*}
+\<close>
 
 inductive ops8 :: "expr => bool"
 where
   "d (Mult (Plus x (Num 1)) (Mult (Plus (Pow x 2) (Num 2)) (Plus (Pow x 3) (Num 3)))) x e ==> ops8 e"
 

 values_prolog "{e. ops8 e}"
 values_prolog "{e. divide10 e}"
 values_prolog "{e. log10 e}"
 values_prolog "{e. times10 e}"
 
-section {* Example negation *}
+section \<open>Example negation\<close>
 
 datatype abc = A | B | C
 
 inductive notB :: "abc => bool"
 where
   "y \<noteq> B \<Longrightarrow> notB y"
 
-setup {* Code_Prolog.map_code_options (K
+setup \<open>Code_Prolog.map_code_options (K
   {ensure_groundness = true,
    limit_globally = NONE,
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = []}) *}
+   manual_reorder = []})\<close>
 
 values_prolog 2 "{y. notB y}"
 
 inductive notAB :: "abc * abc \<Rightarrow> bool"
 where
   "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
 
 values_prolog 5 "{y. notAB y}"
 
-section {* Example prolog conform variable names *}
+section \<open>Example prolog conform variable names\<close>
 
 inductive equals :: "abc => abc => bool"
 where
   "equals y' y'"