equal
deleted
inserted
replaced
32 subsubsection \<open>Code generation\<close> |
32 subsubsection \<open>Code generation\<close> |
33 |
33 |
34 code_datatype Rel |
34 code_datatype Rel |
35 |
35 |
36 lemma [code]: |
36 lemma [code]: |
37 "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)" |
37 "member (x, y) (Rel X R) = ((x = y \<and> x \<in> X) \<or> (x, y) \<in> R)" |
38 by transfer auto |
38 by transfer auto |
39 |
39 |
40 lemma [code]: |
40 lemma [code]: |
41 "converse (Rel X R) = Rel X (R^-1)" |
41 "converse (Rel X R) = Rel X (R\<inverse>)" |
42 by transfer auto |
42 by transfer auto |
43 |
43 |
44 lemma [code]: |
44 lemma [code]: |
45 "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)" |
45 "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)" |
46 by transfer auto |
46 by transfer auto |
47 |
47 |
48 lemma [code]: |
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))" |
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))" |
50 by transfer (auto simp add: Id_on_eqI relcomp.simps) |
50 by transfer (auto simp add: Id_on_eqI relcomp.simps) |
51 |
51 |
52 lemma [code]: |
52 lemma [code]: |
53 "rtrancl (Rel X R) = Rel UNIV (R^+)" |
53 "rtrancl (Rel X R) = Rel UNIV (R\<^sup>+)" |
54 apply transfer |
54 apply transfer |
55 apply auto |
55 apply auto |
56 apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl) |
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) |
57 by (metis in_rtrancl_UnI trancl_into_rtrancl) |
58 |
58 |