8 inductive append |
8 inductive append |
9 where |
9 where |
10 "append [] ys ys" |
10 "append [] ys ys" |
11 | "append xs ys zs ==> append (x # xs) ys (x # zs)" |
11 | "append xs ys zs ==> append (x # xs) ys (x # zs)" |
12 |
12 |
13 ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *} |
13 ML {* Code_Prolog.options := |
|
14 {ensure_groundness = false, |
|
15 limited_types = [], limited_predicates = [], replacing = [], |
|
16 prolog_system = Code_Prolog.SWI_PROLOG} *} |
14 |
17 |
15 values "{(x, y, z). append x y z}" |
18 values "{(x, y, z). append x y z}" |
16 |
19 |
17 values 3 "{(x, y, z). append x y z}" |
20 values 3 "{(x, y, z). append x y z}" |
18 |
21 |
19 ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *} |
22 ML {* Code_Prolog.options := |
|
23 {ensure_groundness = false, |
|
24 limited_types = [], limited_predicates = [], replacing = [], |
|
25 prolog_system = Code_Prolog.YAP} *} |
20 |
26 |
21 values "{(x, y, z). append x y z}" |
27 values "{(x, y, z). append x y z}" |
22 |
28 |
23 ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *} |
29 ML {* Code_Prolog.options := |
|
30 {ensure_groundness = false, |
|
31 limited_types = [], limited_predicates = [], replacing = [], |
|
32 prolog_system = Code_Prolog.SWI_PROLOG} *} |
24 |
33 |
25 |
34 |
26 section {* Example queens *} |
35 section {* Example queens *} |
27 |
36 |
28 inductive nodiag :: "int => int => int list => bool" |
37 inductive nodiag :: "int => int => int list => bool" |
181 |
190 |
182 inductive notB :: "abc => bool" |
191 inductive notB :: "abc => bool" |
183 where |
192 where |
184 "y \<noteq> B \<Longrightarrow> notB y" |
193 "y \<noteq> B \<Longrightarrow> notB y" |
185 |
194 |
186 ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *} |
195 ML {* Code_Prolog.options := {ensure_groundness = true, |
|
196 limited_types = [], |
|
197 limited_predicates = [], |
|
198 replacing = [], |
|
199 prolog_system = Code_Prolog.SWI_PROLOG} *} |
187 |
200 |
188 values 2 "{y. notB y}" |
201 values 2 "{y. notB y}" |
189 |
202 |
190 inductive notAB :: "abc * abc \<Rightarrow> bool" |
203 inductive notAB :: "abc * abc \<Rightarrow> bool" |
191 where |
204 where |