2 let pre_beta = prove_by_refinement
3 (`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==>
4 ((\ { u, v}. g u v) {u',v'} = g u' v')`,
6 REWRITE_TAC[GABS_DEF;GEQ_DEF];
11 let WELLDEFINED_FUNCTION_2 = prove_by_refinement(
12 `(?f:C->D. (!x:A y:B. f(s x y) = t x y)) <=>
13 (!x x' y y'. (s x y = s x' y') ==> t x y = t x' y')`,
15 MATCH_MP_TAC EQ_TRANS ;
16 EXISTS_TAC `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
19 REWRITE_TAC[GSYM SKOLEM_THM];
23 let well_defined_unordered_pair = prove_by_refinement
24 (`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
25 (! u v. g u v = g v u)`,
27 REWRITE_TAC[WELLDEFINED_FUNCTION_2];
28 SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
35 let BETA_PAIR_THM = prove_by_refinement(
36 `!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==>
37 ((\ { u, v}. g u v) {u',v'} = g u' v')`,
40 MATCH_MP_TAC pre_beta;
41 REWRITE_TAC[well_defined_unordered_pair];