src/HOL/ex/Executable_Relation.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 49834 b27bbb021df1 child 61343 5b5656a63bd6 permissions -rw-r--r--
introduce order topology
1 theory Executable_Relation
2 imports Main
3 begin
5 subsection {* A dedicated type for relations *}
7 subsubsection {* Definition of the dedicated type for relations *}
9 typedef 'a rel = "UNIV :: (('a * 'a) set) set"
10 morphisms set_of_rel rel_of_set by simp
12 setup_lifting type_definition_rel
14 lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
16 subsubsection {* Constant definitions on relations *}
18 hide_const (open) converse relcomp rtrancl Image
20 lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
22 lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
24 lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
26 lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
28 lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
30 lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
32 subsubsection {* Code generation *}
34 code_datatype Rel
36 lemma [code]:
37   "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
38 by transfer auto
40 lemma [code]:
41   "converse (Rel X R) = Rel X (R^-1)"
42 by transfer auto
44 lemma [code]:
45   "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
46 by transfer auto
48 lemma [code]:
49    "relcomp (Rel X R) (Rel Y S) = Rel (X Int Y) (Set.filter (%(x, y). y : Y) R Un (Set.filter (%(x, y). x : X) S Un R O S))"
50 by transfer (auto simp add: Id_on_eqI relcomp.simps)
52 lemma [code]:
53   "rtrancl (Rel X R) = Rel UNIV (R^+)"
54 apply transfer
55 apply auto
56 apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
57 by (metis in_rtrancl_UnI trancl_into_rtrancl)
59 lemma [code]:
60   "Image (Rel X R) S = (X Int S) Un (R `` S)"
61 by transfer auto
63 quickcheck_generator rel constructors: Rel
65 lemma
66   "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
67 quickcheck[exhaustive, expect = counterexample]
68 oops
70 end