equal
deleted
inserted
replaced
101 prod_rel |
101 prod_rel |
102 where |
102 where |
103 "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)" |
103 "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)" |
104 |
104 |
105 fun |
105 fun |
106 fun_map |
106 fun_map |
107 where |
107 where |
108 "fun_map f g h x = g (h (f x))" |
108 "fun_map f g h x = g (h (f x))" |
109 |
109 |
|
110 |
110 abbreviation |
111 abbreviation |
111 fun_map_syn ("_ ---> _") |
112 fun_map_syn (infixr "--->" 55) |
112 where |
113 where |
113 "f ---> g \<equiv> fun_map f g" |
114 "f ---> g \<equiv> fun_map f g" |
114 |
115 |
115 lemma FUN_MAP_I: |
116 lemma FUN_MAP_I: |
116 shows "(\<lambda>x. x ---> \<lambda>x. x) = (\<lambda>x. x)" |
117 shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)" |
117 by (simp add: expand_fun_eq) |
118 by (simp add: expand_fun_eq) |
118 |
119 |
119 lemma IN_FUN: |
120 lemma IN_FUN: |
120 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
121 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
121 by (simp add: mem_def) |
122 by (simp add: mem_def) |