| author | wenzelm |
| Wed, 21 Jun 2023 15:20:58 +0200 | |
| changeset 78188 | fd68b98de1f6 |
| 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 |