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