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
bulwahn@46395
     1
theory Executable_Relation
bulwahn@46395
     2
imports Main
bulwahn@46395
     3
begin
bulwahn@46395
     4
bulwahn@46871
     5
subsection {* A dedicated type for relations *}
bulwahn@46871
     6
bulwahn@46871
     7
subsubsection {* Definition of the dedicated type for relations *}
bulwahn@46395
     8
wenzelm@49834
     9
typedef 'a rel = "UNIV :: (('a * 'a) set) set"
bulwahn@47894
    10
morphisms set_of_rel rel_of_set by simp
bulwahn@46395
    11
bulwahn@47894
    12
setup_lifting type_definition_rel
bulwahn@46395
    13
bulwahn@47894
    14
lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
bulwahn@46871
    15
bulwahn@46871
    16
subsubsection {* Constant definitions on relations *}
bulwahn@46871
    17
griff@47433
    18
hide_const (open) converse relcomp rtrancl Image
bulwahn@46395
    19
bulwahn@47894
    20
lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
bulwahn@46395
    21
bulwahn@47894
    22
lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
bulwahn@46395
    23
bulwahn@47894
    24
lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
bulwahn@46395
    25
bulwahn@47894
    26
lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
bulwahn@46871
    27
bulwahn@47894
    28
lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
bulwahn@46395
    29
bulwahn@47894
    30
lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
bulwahn@46871
    31
bulwahn@46871
    32
subsubsection {* Code generation *}
bulwahn@46395
    33
bulwahn@47894
    34
code_datatype Rel
bulwahn@47894
    35
bulwahn@47894
    36
lemma [code]:
bulwahn@47894
    37
  "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
bulwahn@47894
    38
by transfer auto
bulwahn@46395
    39
bulwahn@46871
    40
lemma [code]:
bulwahn@47894
    41
  "converse (Rel X R) = Rel X (R^-1)"
bulwahn@47894
    42
by transfer auto
bulwahn@46395
    43
bulwahn@46871
    44
lemma [code]:
bulwahn@47894
    45
  "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
bulwahn@47894
    46
by transfer auto
bulwahn@46871
    47
bulwahn@46871
    48
lemma [code]:
kuncar@49757
    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))"
bulwahn@47894
    50
by transfer (auto simp add: Id_on_eqI relcomp.simps)
bulwahn@46395
    51
bulwahn@46871
    52
lemma [code]:
bulwahn@47894
    53
  "rtrancl (Rel X R) = Rel UNIV (R^+)"
bulwahn@47894
    54
apply transfer
bulwahn@47894
    55
apply auto
bulwahn@47894
    56
apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
bulwahn@47894
    57
by (metis in_rtrancl_UnI trancl_into_rtrancl)
bulwahn@46395
    58
bulwahn@46871
    59
lemma [code]:
bulwahn@47894
    60
  "Image (Rel X R) S = (X Int S) Un (R `` S)"
bulwahn@47894
    61
by transfer auto
bulwahn@46871
    62
bulwahn@47894
    63
quickcheck_generator rel constructors: Rel
bulwahn@46395
    64
bulwahn@46395
    65
lemma
bulwahn@46871
    66
  "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
bulwahn@46871
    67
quickcheck[exhaustive, expect = counterexample]
bulwahn@46395
    68
oops
bulwahn@46395
    69
bulwahn@46395
    70
end