equal
deleted
inserted
replaced
70 |
70 |
71 lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v" |
71 lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v" |
72 by clarsimp |
72 by clarsimp |
73 |
73 |
74 lemma image_comp: |
74 lemma image_comp: |
75 "(f o g) ` r = f ` (g ` r)" |
75 "f ` (g ` r) = (f o g) ` r" |
76 by auto |
76 by auto |
77 |
77 |
78 lemma vimage_comp: |
78 lemma vimage_comp: |
79 "(g \<circ> f) -` x = f -` (g -` x)" |
79 "f -` (g -` x) = (g \<circ> f) -` x" |
80 by auto |
80 by auto |
81 |
81 |
82 code_printing |
82 code_printing |
83 constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "." |
83 constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "." |
84 |
84 |
833 lemmas o_id = comp_id |
833 lemmas o_id = comp_id |
834 lemmas o_eq_dest = comp_eq_dest |
834 lemmas o_eq_dest = comp_eq_dest |
835 lemmas o_eq_elim = comp_eq_elim |
835 lemmas o_eq_elim = comp_eq_elim |
836 lemmas o_eq_dest_lhs = comp_eq_dest_lhs |
836 lemmas o_eq_dest_lhs = comp_eq_dest_lhs |
837 lemmas o_eq_id_dest = comp_eq_id_dest |
837 lemmas o_eq_id_dest = comp_eq_id_dest |
838 lemmas image_compose = image_comp |
|
839 lemmas vimage_compose = vimage_comp |
|
840 |
838 |
841 end |
839 end |
842 |
840 |