|
56922
|
1 |
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
|
|
|
2 |
|
|
58889
|
3 |
section {* Simple example for table-based implementation of the reflexive transitive closure *}
|
|
56922
|
4 |
|
|
|
5 |
theory Transitive_Closure_Table_Ex
|
|
|
6 |
imports "~~/src/HOL/Library/Transitive_Closure_Table"
|
|
|
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 |
|
|
|
18 |
text {* Invoking with the predicate compiler and the generic code generator *}
|
|
|
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 |
|
|
|
27 |
value "test\<^sup>*\<^sup>* A C"
|
|
|
28 |
value "test\<^sup>*\<^sup>* C A"
|
|
|
29 |
|
|
|
30 |
end
|