author | haftmann |
Wed, 27 Nov 2019 16:54:33 +0000 | |
changeset 71181 | 8331063570d6 |
parent 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
56922 | 1 |
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) |
2 |
||
61343 | 3 |
section \<open>Simple example for table-based implementation of the reflexive transitive closure\<close> |
56922 | 4 |
|
5 |
theory Transitive_Closure_Table_Ex |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66345
diff
changeset
|
6 |
imports "HOL-Library.Transitive_Closure_Table" |
56922 | 7 |
begin |
8 |
||
58310 | 9 |
datatype ty = A | B | C |
56922 | 10 |
|
11 |
inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool" |
|
12 |
where |
|
13 |
"test A B" |
|
14 |
| "test B A" |
|
15 |
| "test B C" |
|
16 |
||
17 |
||
61343 | 18 |
text \<open>Invoking with the predicate compiler and the generic code generator\<close> |
56922 | 19 |
|
20 |
code_pred test . |
|
21 |
||
22 |
values "{x. test\<^sup>*\<^sup>* A C}" |
|
23 |
values "{x. test\<^sup>*\<^sup>* C A}" |
|
24 |
values "{x. test\<^sup>*\<^sup>* A x}" |
|
25 |
values "{x. test\<^sup>*\<^sup>* x C}" |
|
26 |
||
66345
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
61343
diff
changeset
|
27 |
value [nbe] "test\<^sup>*\<^sup>* A C" |
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
61343
diff
changeset
|
28 |
value [nbe] "test\<^sup>*\<^sup>* C A" |
56922 | 29 |
|
30 |
end |