src/HOL/ex/Executable_Relation.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 49834 b27bbb021df1
child 61343 5b5656a63bd6
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 theory Executable_Relation
     2 imports Main
     3 begin
     4 
     5 subsection {* A dedicated type for relations *}
     6 
     7 subsubsection {* Definition of the dedicated type for relations *}
     8 
     9 typedef 'a rel = "UNIV :: (('a * 'a) set) set"
    10 morphisms set_of_rel rel_of_set by simp
    11 
    12 setup_lifting type_definition_rel
    13 
    14 lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
    15 
    16 subsubsection {* Constant definitions on relations *}
    17 
    18 hide_const (open) converse relcomp rtrancl Image
    19 
    20 lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
    21 
    22 lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
    23 
    24 lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
    25 
    26 lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
    27 
    28 lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
    29 
    30 lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
    31 
    32 subsubsection {* Code generation *}
    33 
    34 code_datatype Rel
    35 
    36 lemma [code]:
    37   "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
    38 by transfer auto
    39 
    40 lemma [code]:
    41   "converse (Rel X R) = Rel X (R^-1)"
    42 by transfer auto
    43 
    44 lemma [code]:
    45   "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
    46 by transfer auto
    47 
    48 lemma [code]:
    49    "relcomp (Rel X R) (Rel Y S) = Rel (X Int Y) (Set.filter (%(x, y). y : Y) R Un (Set.filter (%(x, y). x : X) S Un R O S))"
    50 by transfer (auto simp add: Id_on_eqI relcomp.simps)
    51 
    52 lemma [code]:
    53   "rtrancl (Rel X R) = Rel UNIV (R^+)"
    54 apply transfer
    55 apply auto
    56 apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
    57 by (metis in_rtrancl_UnI trancl_into_rtrancl)
    58 
    59 lemma [code]:
    60   "Image (Rel X R) S = (X Int S) Un (R `` S)"
    61 by transfer auto
    62 
    63 quickcheck_generator rel constructors: Rel
    64 
    65 lemma
    66   "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
    67 quickcheck[exhaustive, expect = counterexample]
    68 oops
    69 
    70 end