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