1theory Executable_Relation
2imports Main
3begin
4
5subsection \<open>A dedicated type for relations\<close>
6
7subsubsection \<open>Definition of the dedicated type for relations\<close>
8
9typedef 'a rel = "UNIV :: (('a * 'a) set) set"
10morphisms set_of_rel rel_of_set by simp
11
12setup_lifting type_definition_rel
13
14lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
15
16subsubsection \<open>Constant definitions on relations\<close>
17
18hide_const (open) converse relcomp rtrancl Image
19
20lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
21
22lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
23
24lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
25
26lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
27
28lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
29
30lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
31
32subsubsection \<open>Code generation\<close>
33
34code_datatype Rel
35
36lemma [code]:
37  "member (x, y) (Rel X R) = ((x = y \<and> x \<in> X) \<or> (x, y) \<in> R)"
38by transfer auto
39
40lemma [code]:
41  "converse (Rel X R) = Rel X (R\<inverse>)"
42by transfer auto
43
44lemma [code]:
45  "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
46by transfer auto
47
48lemma [code]:
49   "relcomp (Rel X R) (Rel Y S) = Rel (X \<inter> Y) (Set.filter (\<lambda>(x, y). y \<in> Y) R \<union> (Set.filter (\<lambda>(x, y). x \<in> X) S \<union> R O S))"
50by transfer (auto simp add: Id_on_eqI relcomp.simps)
51
52lemma [code]:
53  "rtrancl (Rel X R) = Rel UNIV (R\<^sup>+)"
54apply transfer
55apply auto
56apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
57by (metis in_rtrancl_UnI trancl_into_rtrancl)
58
59lemma [code]:
60  "Image (Rel X R) S = (X Int S) Un (R `` S)"
61by transfer auto
62
63quickcheck_generator rel constructors: Rel
64
65lemma
66  "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
67quickcheck[exhaustive, expect = counterexample]
68oops
69
70end
71