Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl id <26919-0@swan.cl.cam.ac.uk>; Tue, 12 Nov 1991 01:38:56 +0000 Received: by ted.cs.uidaho.edu (15.11/1.34) id AA09771; Mon, 11 Nov 91 17:22:03 pst Reply-To: info-hol@ted Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@ted.cs.uidaho.edu Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (15.11/1.34) id AA09767; Mon, 11 Nov 91 17:21:53 pst Received: from scaup.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl id <21110-0@swan.cl.cam.ac.uk>; Mon, 11 Nov 1991 18:18:25 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: finite (*)group. Date: Mon, 11 Nov 91 18:18:22 +0000 From: Tom.Melham@uk.ac.cam.cl Message-Id: <"swan.cl.ca.112:11.10.91.18.18.29"@cl.cam.ac.uk> Further to the problem posed by Phil: > So, the problem involves coming up with a group on type * (i.e. a group so > trivial its a group for every type). At least I've managed to do this under the assumption that the type * is finite. The proof works in the obvious way: assume a bijection between * and {0,1,...,N} and then inherit the usual group structure on k MOD (N+1). A HOL proof is attached, for anyone who's interested. Now, has anybody got suggestions for the infinite case? Tom ===================================================================== let fin = "?f:*->num. ?g:num->*. ?N:num. (!n. n <= N = (f(g n) = n)) /\ (!x:*. g(f x) = x)";; let lemma1 = prove ("((!n. n <= N = (f(g n) = n)) /\ (!x:*. g(f x) = x)) ==> !x:*. f x <= N", REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);; let lemma2 = prove ("(n <= m) = (n < (SUC m))", PURE_ONCE_REWRITE_TAC [LESS_OR_EQ;LESS_THM] THEN MATCH_ACCEPT_TAC DISJ_SYM);; let lemma3 = prove ("((!n. n <= N = (f(g n) = n)) /\ (!x:*. g(f x) = x)) ==> !x:*. (f x) MOD (SUC N) = f x", REPEAT STRIP_TAC THEN MATCH_MP_TAC LESS_MOD THEN IMP_RES_TAC lemma1 THEN REWRITE_TAC [SYM lemma2] THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; let lemma4 = prove ("!m. (m MOD (SUC N)) <= N", REPEAT STRIP_TAC THEN ASSUME_TAC (SPEC "N:num" LESS_0) THEN IMP_RES_TAC DIVISION THEN PURE_ONCE_REWRITE_TAC [lemma2] THEN FIRST_ASSUM MATCH_ACCEPT_TAC);; let lemma5 = prove ("(SUC n) MOD (SUC n) = 0", ASSUME_TAC (SPEC "n:num" LESS_0) THEN IMP_RES_THEN (MP_TAC o (SPEC "1")) MOD_EQ_0 THEN REWRITE_TAC [MULT_CLAUSES]);; let lemma6 = MATCH_MP MOD_MOD (SPEC "N:num" LESS_0);; let lemma7 = prove ("!m n. (0 < m) ==> (((SUC n) - m) < (SUC n))", INDUCT_TAC THEN REWRITE_TAC [LESS_REFL;LESS_THM;SUB_MONO_EQ;SUB_EQ_EQ_0] THEN GEN_TAC THEN DISCH_THEN (DISJ_CASES_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THENL [REWRITE_TAC []; REPEAT_TCL STRIP_THM_THEN SUBST1_TAC (SPEC "n:num" num_CASES) THENL [REWRITE_TAC []; RES_TAC THEN ASM_REWRITE_TAC[]]]);; let lemma8 = prove ("((!n. n <= N = (f(g n) = n)) /\ (!x:*. g(f x) = x)) ==> !x:*. ((SUC N) - (f x)) + (f x) = (SUC N)", REPEAT STRIP_TAC THEN MATCH_MP_TAC SUB_ADD THEN MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC "N:num" THEN REWRITE_TAC [LESS_EQ_SUC_REFL] THEN REPEAT_GTCL IMP_RES_THEN MATCH_ACCEPT_TAC lemma1);; let FINITE_GROUP = prove ("^fin ==> ?id:*. ?inv:*->*. ?mult:*->*->*. (!x. mult x id = x) /\ (!x. mult id x = x) /\ (!x. mult x (inv x) = id) /\ (!x. mult (inv x) x = id) /\ (!x y z. (mult x (mult y z)) = (mult (mult x y) z))", STRIP_TAC THEN EXISTS_TAC "g 0:*" THEN EXISTS_TAC "\x:*. g(((SUC N) - (f x)) MOD (SUC N)):*" THEN EXISTS_TAC "\x:*. \y:*. g((f x + f y) MOD (SUC N)):*" THEN CONV_TAC (DEPTH_CONV BETA_CONV) THEN ASSUME_TAC (SPEC "N:num" ZERO_LESS_EQ) THEN RES_THEN (\th. REWRITE_TAC [th;ADD_CLAUSES]) THEN MP_TAC lemma4 THEN REPEAT_GTCL IMP_RES_THEN (\th. ASM_REWRITE_TAC [th]) lemma3 THEN DISCH_THEN (\th. REWRITE_TAC [th]) THEN PURE_ONCE_REWRITE_TAC [SPECL ["f(x:*):num";"n MOD m"] ADD_SYM] THEN REWRITE_TAC [CONJ_ASSOC] THEN REPEAT STRIP_TAC THENL [let cases = SPEC "f(x:*):num" LESS_0_CASES in DISJ_CASES_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC cases THENL [REWRITE_TAC [SUB_0;ADD_CLAUSES;lemma6] THEN REWRITE_TAC [lemma5]; IMP_RES_THEN (ASSUME_TAC o SPEC "N:num") lemma7 THEN IMP_RES_THEN (\th. REWRITE_TAC [th]) LESS_MOD THEN REPEAT_GTCL IMP_RES_THEN (\th. REWRITE_TAC [th]) lemma8 THEN REWRITE_TAC [lemma5]]; let th1 = UNDISCH_ALL (CONV_RULE ANTE_CONJ_CONV lemma3) in SUBST1_TAC (SYM (SPEC "x:*" th1)) THEN SUBST1_TAC (SYM (SPEC "z:*" th1)) THEN REWRITE_TAC [MATCH_MP MOD_PLUS (SPEC "N:num" LESS_0)] THEN REWRITE_TAC [th1] THEN SUBST1_TAC (SPECL ["f(y:*) + f z";"f(x:*):num"] ADD_SYM) THEN REWRITE_TAC [ADD_ASSOC]]);;