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