1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definitions: (General definitions file) *)
5 (* Chapter: Packings *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
12 Support for functions f {a,b} defined by lambda abstraction.
15 module Beta_pair = struct
18 let pre_beta = prove_by_refinement
19 (`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==>
20 ((\ { u, v}. g u v) {u',v'} = g u' v')`,
22 REWRITE_TAC[GABS_DEF;GEQ_DEF];
27 let WELLDEFINED_FUNCTION_2 = prove_by_refinement(
28 `(?f:C->D. (!x:A y:B. f(s x y) = t x y)) <=>
29 (!x x' y y'. (s x y = s x' y') ==> t x y = t x' y')`,
31 MATCH_MP_TAC EQ_TRANS ;
32 EXISTS_TAC `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
35 REWRITE_TAC[GSYM SKOLEM_THM];
39 let well_defined_unordered_pair = prove_by_refinement
40 (`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
41 (! u v. g u v = g v u)`,
43 REWRITE_TAC[WELLDEFINED_FUNCTION_2];
44 SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
51 let BETA_PAIR_THM = prove_by_refinement(
52 `!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==>
53 ((\ { u, v}. g u v) {u',v'} = g u' v')`,
56 MATCH_MP_TAC pre_beta;
57 REWRITE_TAC[well_defined_unordered_pair];