src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

 | "D \<noteq> N - B ==> D \<noteq> B - N ==> Da = D + 1 ==> nodiag B Da L ==> nodiag B D (N # L)"
 
 text {*
 qdelete(A, [A|L], L).
 qdelete(X, [A|Z], [A|R]) :-
-	qdelete(X, Z, R).
+  qdelete(X, Z, R).
 *}
 
 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 {*
 qperm([], []).
 qperm([X|Y], K) :-
-	qdelete(U, [X|Y], Z),
-	K = [U|V],
-	qperm(Z, V).
+  qdelete(U, [X|Y], Z),
+  K = [U|V],
+  qperm(Z, V).
 *}
 
 inductive qperm :: "int list => int list => bool"
 where
   "qperm [] []"
 | "qdelete U (X # Y) Z ==> qperm Z V ==> qperm (X # Y) (U # V)"
 
 text {*
 safe([]).
 safe([N|L]) :-
-	nodiag(N, 1, L),
-	safe(L).
+  nodiag(N, 1, L),
+  safe(L).
 *}
 
 inductive safe :: "int list => bool"
 where
   "safe []"
 | "nodiag N 1 L ==> safe L ==> safe (N # L)"
 
 text {*
 queen(Data, Out) :-
-	qperm(Data, Out),
-	safe(Out)
+  qperm(Data, Out),
+  safe(Out)
 *}
 
 inductive queen :: "int list => int list => bool"
 where
   "qperm Data Out ==> safe Out ==> queen Data Out"

   | Minus expr expr | Uminus expr | Pow expr int | Exp expr
 
 text {*
 
 d(U + V, X, DU + DV) :-
-	cut,
-	d(U, X, DU),
-	d(V, X, DV).
+  cut,
+  d(U, X, DU),
+  d(V, X, DV).
 d(U - V, X, DU - DV) :-
-	cut,
-	d(U, X, DU),
-	d(V, X, DV).
+  cut,
+  d(U, X, DU),
+  d(V, X, DV).
 d(U * V, X, DU * V + U * DV) :-
-	cut,
-	d(U, X, DU),
-	d(V, X, DV).
+  cut,
+  d(U, X, DU),
+  d(V, X, DV).
 d(U / V, X, (DU * V - U * DV) / ^(V, 2)) :-
-	cut,
-	d(U, X, DU),
-	d(V, X, DV).
+  cut,
+  d(U, X, DU),
+  d(V, X, DV).
 d(^(U, N), X, DU * num(N) * ^(U, N1)) :-
-	cut,
-	N1 is N - 1,
-	d(U, X, DU).
+  cut,
+  N1 is N - 1,
+  d(U, X, DU).
 d(-U, X, -DU) :-
-	cut,
-	d(U, X, DU).
+  cut,
+  d(U, X, DU).
 d(exp(U), X, exp(U) * DU) :-
-	cut,
-	d(U, X, DU).
+  cut,
+  d(U, X, DU).
 d(log(U), X, DU / U) :-
-	cut,
-	d(U, X, DU).
+  cut,
+  d(U, X, DU).
 d(x, X, num(1)) :-
-	cut.
+  cut.
 d(num(_), _, num(0)).
 
 *}
 
 inductive d :: "expr => expr => expr => bool"

 | "d x X (Num 1)"
 | "d (Num n) X (Num 0)"
 
 text {*
 ops8(E) :-
-	d((x + num(1)) * ((^(x, 2) + num(2)) * (^(x, 3) + num(3))), x, 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).
+  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).
+  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)
+  d(((((((((x * x) * x) * x) * x) * x) * x) * x) * x) * x, x, E)
 *}
 
 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"