src/HOL/ex/Transitive_Closure_Table_Ex.thy
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61343 5b5656a63bd6
child 66345 882abe912da9
permissions -rw-r--r--
proper syntax;

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

section \<open>Simple example for table-based implementation of the reflexive transitive closure\<close>

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

datatype ty = A | B | C

inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
where
  "test A B"
| "test B A"
| "test B C"


text \<open>Invoking with the predicate compiler and the generic code generator\<close>

code_pred test .

values "{x. test\<^sup>*\<^sup>* A C}"
values "{x. test\<^sup>*\<^sup>* C A}"
values "{x. test\<^sup>*\<^sup>* A x}"
values "{x. test\<^sup>*\<^sup>* x C}"

value "test\<^sup>*\<^sup>* A C"
value "test\<^sup>*\<^sup>* C A"

end