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