(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definitions: (General definitions file)         *)
(* Chapter: Packings                                                     *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-01                                                           *)
(* ========================================================================== *)


(*
Support for functions f {a,b} defined by lambda abstraction.
*)

module Beta_pair = struct


let pre_beta = 
prove_by_refinement
(`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==> 
    ((\ { u, v}. g u v) {u',v'} = g u' v')`,

[
REWRITE_TAC[GABS_DEF;GEQ_DEF];
SELECT_ELIM_TAC;
MESON_TAC[];
]);;
let WELLDEFINED_FUNCTION_2 = 
prove_by_refinement(
`(?f:C->D. (!x:A y:B.  f(s x y) = t x y)) <=> 
   (!x x' y y'.  (s x y = s x' y') ==> t x y = t x' y')`,

[
  MATCH_MP_TAC EQ_TRANS ;
  EXISTS_TAC  `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
  CONJ_TAC;
  MESON_TAC[];
  REWRITE_TAC[GSYM SKOLEM_THM];
  MESON_TAC[];
]);;
let well_defined_unordered_pair = 
prove_by_refinement
(`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
   (! u v. g u v = g v u)`,

[
REWRITE_TAC[WELLDEFINED_FUNCTION_2];
SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
SET_TAC[];
ASM_REWRITE_TAC[];
MESON_TAC[];
]
);;
let BETA_PAIR_THM = 
prove_by_refinement(
`!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==> 
    ((\ { u, v}. g u v) {u',v'} = g u' v')`,

[
REPEAT STRIP_TAC;
MATCH_MP_TAC pre_beta;
REWRITE_TAC[well_defined_unordered_pair];
ASM_REWRITE_TAC[];
]
);;

end;;