Lines Matching refs:f2
74 val sum_prod_duality = prove(``!f1 f2.
75 (prod_retrieve f1 f2) =
76 (combin$C (sum_retrieve (combin$C f1) (combin$C f2)))``,
109 prove(``!f1 g1 f2 g2.
110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) =
111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)``
119 val sum_inj_pair_thm = prove(``!f1 g1 f2 g2.
121 (inj_pair f2 g2) ==>
122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``,
130 val sum_retrieve_map_thm = prove(``!f1 g1 f2 g2.
131 (sum_retrieve g1 g2) o (sum_map f1 f2) =
132 (sum_retrieve (g1 o f1) (g2 o f2))
146 val sum_all_map_thm = prove(``!P1 P2 f1 f2.
147 (sum_all P1 P2) o (sum_map f1 f2) = sum_all (P1 o f1) (P2 o f2)
178 val prod_inj_pair_thm = prove(``!f1 g1 f2 g2.
180 (inj_pair f2 g2) ==>
181 (inj_pair (f1 ## f2) (prod_retrieve g1 g2))``,
192 val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2.
193 (prod_retrieve g1 g2) o (f1 ## f2) =
194 (prod_retrieve (g1 o f1) (g2 o f2))
208 val prod_all_map_thm = prove(``!P1 P2 f1 f2.
209 (prod_all P1 P2) o (prod_map f1 f2) = prod_all (P1 o f1) (P2 o f2)
277 val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2.
278 (prod_retrieve g1 g2) o (f1 ## f2) =
279 (prod_retrieve (g1 o f1) (g2 o f2))
368 val option_map_map_thm = prove(``!f1 f2.
369 (option_map f1) o (option_map f2) = (option_map (f1 o f2))