src/HOL/ex/Transitive_Closure_Table_Ex.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Simple example for table-based implementation of the reflexive transitive closure *}
     4 
     5 theory Transitive_Closure_Table_Ex
     6 imports "~~/src/HOL/Library/Transitive_Closure_Table"
     7 begin
     8 
     9 datatype ty = A | B | C
    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