Theory Transitive_Closure_Table_Ex

(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)

header {* Simple example for table-based implementation of the reflexive transitive closure *}

theory Transitive_Closure_Table_Ex
imports "~~/src/HOL/Library/Transitive_Closure_Table"
begin

datatype ty = A | B | C

inductive test :: "ty => ty => bool"
where
  "test A B"
| "test B A"
| "test B C"


text {* Invoking with the predicate compiler and the generic code generator *}

code_pred test .

values "{x. test⇧*⇧* A C}"
values "{x. test⇧*⇧* C A}"
values "{x. test⇧*⇧* A x}"
values "{x. test⇧*⇧* x C}"

value "test⇧*⇧* A C"
value "test⇧*⇧* C A"

end