equal
deleted
inserted
replaced
70 abbreviation |
70 abbreviation |
71 rel_conj (infixr "OOO" 75) |
71 rel_conj (infixr "OOO" 75) |
72 where |
72 where |
73 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
73 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
74 |
74 |
75 lemma eq_comp_r: "op = OO R OO op = \<equiv> R" |
75 lemma eq_comp_r: "(op = OO R OO op =) = R" |
76 apply (rule eq_reflection) |
|
77 apply (rule ext)+ |
76 apply (rule ext)+ |
78 apply auto |
77 apply auto |
79 done |
78 done |
80 |
79 |
81 section {* Respects predicate *} |
80 section {* Respects predicate *} |
106 lemma fun_map_id: |
105 lemma fun_map_id: |
107 shows "(id ---> id) = id" |
106 shows "(id ---> id) = id" |
108 by (simp add: expand_fun_eq id_def) |
107 by (simp add: expand_fun_eq id_def) |
109 |
108 |
110 lemma fun_rel_eq: |
109 lemma fun_rel_eq: |
111 shows "(op =) ===> (op =) \<equiv> (op =)" |
110 shows "((op =) ===> (op =)) = (op =)" |
112 by (rule eq_reflection) (simp add: expand_fun_eq) |
111 by (simp add: expand_fun_eq) |
113 |
112 |
114 lemma fun_rel_id: |
113 lemma fun_rel_id: |
115 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
114 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
116 shows "(R1 ===> R2) f g" |
115 shows "(R1 ===> R2) f g" |
117 using a by simp |
116 using a by simp |