src/HOL/ex/Executable_Relation.thy
author griff
Tue Apr 03 17:26:30 2012 +0900 (2012-04-03)
changeset 47433 07f4bf913230
parent 47097 987cb55cac44
child 47435 e1b761c216ac
permissions -rw-r--r--
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
bulwahn@46395
     1
theory Executable_Relation
bulwahn@46395
     2
imports Main
bulwahn@46395
     3
begin
bulwahn@46395
     4
bulwahn@46871
     5
subsection {* Preliminaries on the raw type of relations *}
bulwahn@46871
     6
bulwahn@46871
     7
definition rel_raw :: "'a set => ('a * 'a) set => ('a * 'a) set"
bulwahn@46871
     8
where
bulwahn@46871
     9
  "rel_raw X R = Id_on X Un R"
bulwahn@46871
    10
bulwahn@46871
    11
lemma member_raw:
bulwahn@46871
    12
  "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
bulwahn@46871
    13
unfolding rel_raw_def by auto
bulwahn@46871
    14
kuncar@47097
    15
bulwahn@46871
    16
lemma Id_raw:
bulwahn@46871
    17
  "Id = rel_raw UNIV {}"
bulwahn@46871
    18
unfolding rel_raw_def by auto
bulwahn@46871
    19
bulwahn@46871
    20
lemma converse_raw:
bulwahn@46871
    21
  "converse (rel_raw X R) = rel_raw X (converse R)"
bulwahn@46871
    22
unfolding rel_raw_def by auto
bulwahn@46871
    23
bulwahn@46871
    24
lemma union_raw:
bulwahn@46871
    25
  "(rel_raw X R) Un (rel_raw Y S) = rel_raw (X Un Y) (R Un S)"
bulwahn@46871
    26
unfolding rel_raw_def by auto
bulwahn@46871
    27
bulwahn@46871
    28
lemma comp_Id_on:
bulwahn@46871
    29
  "Id_on X O R = Set.project (%(x, y). x : X) R"
griff@47433
    30
by (auto intro!: relcompI)
bulwahn@46395
    31
bulwahn@46871
    32
lemma comp_Id_on':
bulwahn@46871
    33
  "R O Id_on X = Set.project (%(x, y). y : X) R"
bulwahn@46871
    34
by auto
bulwahn@46871
    35
bulwahn@46871
    36
lemma project_Id_on:
bulwahn@46871
    37
  "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
bulwahn@46871
    38
by auto
bulwahn@46395
    39
griff@47433
    40
lemma relcomp_raw:
bulwahn@46871
    41
  "(rel_raw X R) O (rel_raw Y S) = rel_raw (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
bulwahn@46871
    42
unfolding rel_raw_def
bulwahn@46871
    43
apply simp
bulwahn@46871
    44
apply (simp add: comp_Id_on)
bulwahn@46871
    45
apply (simp add: project_Id_on)
bulwahn@46871
    46
apply (simp add: comp_Id_on')
bulwahn@46871
    47
apply auto
bulwahn@46871
    48
done
bulwahn@46395
    49
bulwahn@46871
    50
lemma rtrancl_raw:
bulwahn@46871
    51
  "(rel_raw X R)^* = rel_raw UNIV (R^+)"
bulwahn@46871
    52
unfolding rel_raw_def
bulwahn@46871
    53
apply auto
bulwahn@46871
    54
apply (metis Id_on_iff Un_commute iso_tuple_UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
bulwahn@46871
    55
by (metis in_rtrancl_UnI trancl_into_rtrancl)
bulwahn@46871
    56
bulwahn@46871
    57
lemma Image_raw:
bulwahn@46871
    58
  "(rel_raw X R) `` S = (X Int S) Un (R `` S)"
bulwahn@46871
    59
unfolding rel_raw_def by auto
bulwahn@46871
    60
bulwahn@46871
    61
subsection {* A dedicated type for relations *}
bulwahn@46871
    62
bulwahn@46871
    63
subsubsection {* Definition of the dedicated type for relations *}
bulwahn@46395
    64
bulwahn@46395
    65
quotient_type 'a rel = "('a * 'a) set" / "(op =)"
bulwahn@46395
    66
morphisms set_of_rel rel_of_set by (metis identity_equivp)
bulwahn@46395
    67
bulwahn@46395
    68
lemma [simp]:
bulwahn@46395
    69
  "rel_of_set (set_of_rel S) = S"
bulwahn@46395
    70
by (rule Quotient_abs_rep[OF Quotient_rel])
bulwahn@46395
    71
bulwahn@46395
    72
lemma [simp]:
bulwahn@46395
    73
  "set_of_rel (rel_of_set R) = R"
bulwahn@46395
    74
by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
bulwahn@46395
    75
bulwahn@46871
    76
lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
bulwahn@46871
    77
kuncar@47097
    78
quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
bulwahn@46871
    79
bulwahn@46871
    80
subsubsection {* Constant definitions on relations *}
bulwahn@46871
    81
griff@47433
    82
hide_const (open) converse relcomp rtrancl Image
bulwahn@46395
    83
bulwahn@46395
    84
quotient_definition member :: "'a * 'a => 'a rel => bool" where
kuncar@47097
    85
  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
bulwahn@46395
    86
bulwahn@46871
    87
quotient_definition converse :: "'a rel => 'a rel"
bulwahn@46871
    88
where
kuncar@47097
    89
  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
bulwahn@46395
    90
bulwahn@46871
    91
quotient_definition union :: "'a rel => 'a rel => 'a rel"
bulwahn@46871
    92
where
kuncar@47097
    93
  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
bulwahn@46395
    94
griff@47433
    95
quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
bulwahn@46871
    96
where
griff@47433
    97
  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
bulwahn@46871
    98
bulwahn@46871
    99
quotient_definition rtrancl :: "'a rel => 'a rel"
bulwahn@46871
   100
where
kuncar@47097
   101
  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
bulwahn@46395
   102
bulwahn@46871
   103
quotient_definition Image :: "'a rel => 'a set => 'a set"
bulwahn@46871
   104
where
kuncar@47097
   105
  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
bulwahn@46871
   106
bulwahn@46871
   107
subsubsection {* Code generation *}
bulwahn@46395
   108
bulwahn@46871
   109
code_datatype rel
bulwahn@46395
   110
bulwahn@46871
   111
lemma [code]:
bulwahn@46871
   112
  "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
kuncar@47097
   113
by (lifting member_raw)
bulwahn@46395
   114
bulwahn@46871
   115
lemma [code]:
bulwahn@46871
   116
  "converse (rel X R) = rel X (R^-1)"
kuncar@47097
   117
by (lifting converse_raw)
bulwahn@46871
   118
bulwahn@46871
   119
lemma [code]:
bulwahn@46871
   120
  "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
kuncar@47097
   121
by (lifting union_raw)
bulwahn@46395
   122
bulwahn@46871
   123
lemma [code]:
griff@47433
   124
   "relcomp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
griff@47433
   125
by (lifting relcomp_raw)
bulwahn@46395
   126
bulwahn@46871
   127
lemma [code]:
bulwahn@46871
   128
  "rtrancl (rel X R) = rel UNIV (R^+)"
kuncar@47097
   129
by (lifting rtrancl_raw)
bulwahn@46395
   130
bulwahn@46871
   131
lemma [code]:
bulwahn@46871
   132
  "Image (rel X R) S = (X Int S) Un (R `` S)"
kuncar@47097
   133
by (lifting Image_raw)
bulwahn@46871
   134
bulwahn@46871
   135
quickcheck_generator rel constructors: rel
bulwahn@46395
   136
bulwahn@46395
   137
lemma
bulwahn@46871
   138
  "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
bulwahn@46871
   139
quickcheck[exhaustive, expect = counterexample]
bulwahn@46395
   140
oops
bulwahn@46395
   141
bulwahn@46395
   142
end