Theory Transitive_Closure_Table_Ex

theory Transitive_Closure_Table_Ex
imports Transitive_Closure_Table
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)

section ‹Simple example for table-based implementation of the reflexive transitive closure›

theory Transitive_Closure_Table_Ex
imports "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 [nbe] "test** A C"
value [nbe] "test** C A"

end