src/HOL/ex/Transitive_Closure_Table_Ex.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58310 91ea607a34d8
child 61343 5b5656a63bd6
permissions -rw-r--r--
modernized header uniformly as section;
     1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
     2 
     3 section {* 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