src/HOL/ex/Executable_Relation.thy
author wenzelm
Tue Oct 06 17:47:28 2015 +0200 (2015-10-06)
changeset 61343 5b5656a63bd6
parent 49834 b27bbb021df1
child 67613 ce654b0e6d69
permissions -rw-r--r--
isabelle update_cartouches;
bulwahn@46395
     1
theory Executable_Relation
bulwahn@46395
     2
imports Main
bulwahn@46395
     3
begin
bulwahn@46395
     4
wenzelm@61343
     5
subsection \<open>A dedicated type for relations\<close>
bulwahn@46871
     6
wenzelm@61343
     7
subsubsection \<open>Definition of the dedicated type for relations\<close>
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
wenzelm@61343
    16
subsubsection \<open>Constant definitions on relations\<close>
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
wenzelm@61343
    32
subsubsection \<open>Code generation\<close>
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