Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* ------------------------------------------------------------------------- *) (* Volume of a solid triangle (from Flyspeck). *) (* ------------------------------------------------------------------------- *) let VOLUME_SOLID_TRIANGLE = prove (`!r v0 v1 v2 v3:real^3. &0 < r /\ ~coplanar{v0, v1, v2, v3} ==> measure(ball(v0,r) INTER aff_gt {v0} {v1,v2,v3}) = let a123 = dihV v0 v1 v2 v3 in let a231 = dihV v0 v2 v3 v1 in let a312 = dihV v0 v3 v1 v2 in (a123 + a231 + a312 - pi) * r pow 3 / &3`, let tac convl = W(MP_TAC o PART_MATCH (lhs o rand) MEASURE_BALL_AFF_GT_SHUFFLE o convl o lhand o lhand o snd) THEN ASM_REWRITE_TAC[UNION_EMPTY; IN_INSERT; IN_UNION; NOT_IN_EMPTY] THEN REWRITE_TAC[SET_RULE `(a INSERT s) UNION t = a INSERT (s UNION t)`] THEN ASM_SIMP_TAC[UNION_EMPTY; REAL_LT_IMP_LE] THEN ANTS_TAC THENL [CONJ_TAC THENL [DISCH_THEN(STRIP_THM_THEN SUBST_ALL_TAC) THEN RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN RULE_ASSUM_TAC(REWRITE_RULE[COPLANAR_3]) THEN FIRST_ASSUM CONTR_TAC; MATCH_MP_TAC NOT_COPLANAR_0_4_IMP_INDEPENDENT THEN RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN ASM_REWRITE_TAC[INSERT_AC]]; DISCH_THEN SUBST1_TAC] in GEN_TAC THEN GEOM_ORIGIN_TAC `v0:real^3` THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `measure(ball(vec 0:real^3,r) INTER aff_gt {vec 0,v1,v2,v3} {}) = &4 / &3 * pi * r pow 3` MP_TAC THENL [MP_TAC(SPECL [`vec 0:real^3`; `r:real`] VOLUME_BALL) THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE `t = UNIV ==> s INTER t = s`) THEN REWRITE_TAC[AFF_GT_EQ_AFFINE_HULL] THEN SIMP_TAC[AFFINE_HULL_EQ_SPAN; HULL_INC; IN_INSERT; SPAN_INSERT_0] THEN REWRITE_TAC[SET_RULE `s = UNIV <=> UNIV SUBSET s`] THEN MATCH_MP_TAC CARD_GE_DIM_INDEPENDENT THEN ASM_SIMP_TAC[DIM_UNIV; DIMINDEX_3; SUBSET_UNIV] THEN ASM_SIMP_TAC[NOT_COPLANAR_0_4_IMP_INDEPENDENT] THEN SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [FIRST_X_ASSUM SUBST_ALL_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC; COPLANAR_3]) THEN ASM_MESON_TAC[]; ASM_REWRITE_TAC[]]) [`v3:real^3 = v2`; `v3:real^3 = v1`; `v2:real^3 = v1`] THEN CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN SUBGOAL_THEN `~(coplanar {vec 0:real^3,v1,v2,v3}) /\ ~(coplanar {vec 0,--v1,v2,v3}) /\ ~(coplanar {vec 0,v1,--v2,v3}) /\ ~(coplanar {vec 0,--v1,--v2,v3}) /\ ~(coplanar {vec 0,--v1,--v2,v3}) /\ ~(coplanar {vec 0,--v1,v2,--v3}) /\ ~(coplanar {vec 0,v1,--v2,--v3}) /\ ~(coplanar {vec 0,--v1,--v2,--v3}) /\ ~(coplanar {vec 0,--v1,--v2,--v3})` STRIP_ASSUME_TAC THENL [REPLICATE_TAC 3 (REWRITE_TAC[COPLANAR_INSERT_0_NEG] THEN ONCE_REWRITE_TAC[SET_RULE `{vec 0,a,b,c} = {vec 0,b,c,a}`]) THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN MAP_EVERY tac [I; lhand; rand; lhand o lhand; rand o lhand; lhand o rand; rand o rand] THEN MP_TAC(ISPECL [`v1:real^3`; `v2:real^3`; `v3:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN MP_TAC(ISPECL [`v2:real^3`; `v3:real^3`; `v1:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN MP_TAC(ISPECL [`v3:real^3`; `v1:real^3`; `v2:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN MP_TAC(ISPECL [`--v1:real^3`; `--v2:real^3`; `--v3:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN MP_TAC(ISPECL [`--v2:real^3`; `--v3:real^3`; `--v1:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN MP_TAC(ISPECL [`--v3:real^3`; `--v1:real^3`; `--v2:real^3`] MEASURE_LUNE_DECOMPOSITION) THEN ASM_REWRITE_TAC[VECTOR_NEG_NEG] THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; INSERT_AC] THEN RULE_ASSUM_TAC(REWRITE_RULE[INSERT_AC]) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DIHV_NEG_0] THEN REWRITE_TAC[SOLID_TRIANGLE_CONGRUENT_NEG] THEN REWRITE_TAC[INSERT_AC] THEN REAL_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* Automation in number theory. *) (* ------------------------------------------------------------------------- *) let COPRIME_SOS = NUMBER_RULE `!x y:num. coprime(x,y) <=> coprime(x * y,x EXP 2 + y EXP 2)`;; let SOLVABLE_GCD = INTEGER_RULE `!a b n:int. gcd(a,n) divides b <=> ?x. (a * x == b) (mod n)`;; let COVERING_CONGRUENCES_1 = prove (`!n. (n == 0) (mod 2) \/ (n == 0) (mod 3) \/ (n == 1) (mod 4) \/ (n == 3) (mod 8) \/ (n == 7) (mod 12) \/ (n == 23) (mod 24)`, GEN_TAC THEN REWRITE_TAC[num_congruent; int_congruent] THEN SPEC_TAC(`&n:int`,`x:int`) THEN CONV_TAC COOPER_CONV);; (* ------------------------------------------------------------------------- *) (* Automation of algebraic reasoning. *) (* ------------------------------------------------------------------------- *) let CUBIC_BASIC = COMPLEX_FIELD `!i t s. s pow 2 = q pow 2 + p pow 3 /\ (s1 pow 3 = if p = Cx(&0) then Cx(&2) * q else q + s) /\ s2 = --s1 * (Cx(&1) + i * t) / Cx(&2) /\ s3 = --s1 * (Cx(&1) - i * t) / Cx(&2) /\ i pow 2 + Cx(&1) = Cx(&0) /\ t pow 2 = Cx(&3) ==> if p = Cx(&0) then (y pow 3 + Cx(&3) * p * y - Cx(&2) * q = Cx(&0) <=> y = s1 \/ y = s2 \/ y = s3) else ~(s1 = Cx(&0)) /\ (y pow 3 + Cx(&3) * p * y - Cx(&2) * q = Cx(&0) <=> (y = s1 - p / s1 \/ y = s2 - p / s2 \/ y = s3 - p / s3))`;; (* ------------------------------------------------------------------------- *) (* Extended example of "friend" theorem. *) (* ------------------------------------------------------------------------- *) let FRIENDS = prove (`!s:person->bool. FINITE(s) /\ 2 <= CARD s /\ (!x. ~friend(x,x)) /\ (!x y. friend(x,y) <=> friend(y,x)) ==> ?p q. p IN s /\ q IN s /\ ~(p = q) /\ CARD {r | r IN s /\ friend(p,r)} = CARD {r | r IN s /\ friend(q,r)}`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`s:person->bool`; `0..(CARD(s:person->bool) - 1)`; `\p:person. CARD {r:person | r IN s /\ friend(p,r)}`] SURJECTIVE_IFF_INJECTIVE_GEN) THEN SIMP_TAC[] THEN ANTS_TAC THENL [ASM_SIMP_TAC[FINITE_NUMSEG; CARD_NUMSEG; SUBSET; FORALL_IN_IMAGE] THEN ASM_SIMP_TAC[SUB_ADD; ARITH_RULE `2 <= n ==> 1 <= n`; SUB_0] THEN REWRITE_TAC[IN_NUMSEG; LE_0] THEN X_GEN_TAC `p:person` THEN DISCH_TAC THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD(s DELETE (p:person))` THEN CONJ_TAC THENL [MATCH_MP_TAC CARD_SUBSET; ASM_SIMP_TAC[CARD_DELETE]] THEN ASM_SIMP_TAC[FINITE_DELETE; LE_REFL] THEN ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(TAUT `(~p' <=> q) /\ ~p ==> (p <=> p') ==> q`) THEN CONJ_TAC THENL [MESON_TAC[]; REWRITE_TAC[NOT_FORALL_THM; NOT_IMP]] THEN MATCH_MP_TAC(MESON[] `P 0 \/ P(CARD(s:person->bool) - 1) ==> ?y. P y`) THEN REWRITE_TAC[IN_NUMSEG; LE_REFL; LE_0; GSYM DE_MORGAN_THM] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `p:person` STRIP_ASSUME_TAC) (X_CHOOSE_THEN `q:person` STRIP_ASSUME_TAC)) THEN ASM_CASES_TAC `p:person = q` THENL [ASM_MESON_TAC[ARITH_RULE `2 <= n ==> ~(n - 1 = 0)`]; ALL_TAC] THEN SUBGOAL_THEN `{r:person | r IN s /\ friend(q,r)} = s DELETE q` MP_TAC THENL [MATCH_MP_TAC CARD_SUBSET_EQ THEN ASM_SIMP_TAC[FINITE_DELETE; CARD_DELETE] THEN ASM SET_TAC[]; UNDISCH_TAC `CARD {r | r IN s /\ friend(p:person,r:person)} = 0` THEN ASM_SIMP_TAC[CARD_EQ_0; FINITE_RESTRICT] THEN ASM SET_TAC[]]);;