src/HOL/ex/Transitive_Closure_Table_Ex.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61343 5b5656a63bd6
permissions -rw-r--r--
prefer symbols;
haftmann@56922
     1
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
haftmann@56922
     2
wenzelm@58889
     3
section {* Simple example for table-based implementation of the reflexive transitive closure *}
haftmann@56922
     4
haftmann@56922
     5
theory Transitive_Closure_Table_Ex
haftmann@56922
     6
imports "~~/src/HOL/Library/Transitive_Closure_Table"
haftmann@56922
     7
begin
haftmann@56922
     8
blanchet@58310
     9
datatype ty = A | B | C
haftmann@56922
    10
haftmann@56922
    11
inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
haftmann@56922
    12
where
haftmann@56922
    13
  "test A B"
haftmann@56922
    14
| "test B A"
haftmann@56922
    15
| "test B C"
haftmann@56922
    16
haftmann@56922
    17
haftmann@56922
    18
text {* Invoking with the predicate compiler and the generic code generator *}
haftmann@56922
    19
haftmann@56922
    20
code_pred test .
haftmann@56922
    21
haftmann@56922
    22
values "{x. test\<^sup>*\<^sup>* A C}"
haftmann@56922
    23
values "{x. test\<^sup>*\<^sup>* C A}"
haftmann@56922
    24
values "{x. test\<^sup>*\<^sup>* A x}"
haftmann@56922
    25
values "{x. test\<^sup>*\<^sup>* x C}"
haftmann@56922
    26
haftmann@56922
    27
value "test\<^sup>*\<^sup>* A C"
haftmann@56922
    28
value "test\<^sup>*\<^sup>* C A"
haftmann@56922
    29
haftmann@56922
    30
end