Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from lal.cs.byu.edu (actually leopard.cs.byu.edu !OR! info-hol-request@lal.cs.byu.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Tue, 27 Sep 1994 16:08:09 +0100
Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA23870;
          Tue, 27 Sep 1994 08:56:58 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by lal.cs.byu.edu with SMTP (1.38.193.4/16.2) 
          id AA23866; Tue, 27 Sep 1994 08:56:43 -0600
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 27 Sep 1994 15:27:51 +0100
To: info-hol@lal.cs.byu.edu
Subject: Re: Could anyone prove this for me?
In-Reply-To: Your message of "Mon, 22 Aug 94 13:11:39 BST." <24957.9408221211@eng.warwick.ac.uk>
Date: Tue, 27 Sep 94 15:27:31 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:185040:940927142815"@cl.cam.ac.uk>


Nam writes:

|
| I am trying to prove "!x. sqrt (x pow 2) = abs x" using library `reals`.
|

Indeed, many of these theorems are a bit tedious, as there's not much support
yet. Anyway here is a proof:

  can unlink `NAM.th`;;

  new_theory `NAM`;;

  load_library `reals`;;

  set_interface_map real_interface_map;;

  let ROOT_POS_POW_LT = prove_thm(`ROOT_POS_POW_LT`,
    "!n x. &0 < x ==> (root(SUC n) (x pow (SUC n)) = x)",
    REPEAT GEN_TAC THEN DISCH_TAC THEN
    FIRST_ASSUM(MP_TAC o SPEC "n:num" o MATCH_MP POW_POS_LT) THEN
    DISCH_THEN(SUBST1_TAC o SPEC "n:num" o MATCH_MP ROOT_LN) THEN
    FIRST_ASSUM(\th. REWRITE_TAC[MATCH_MP LN_POW th]) THEN
    POP_ASSUM(MP_TAC o REWRITE_RULE[GSYM EXP_LN]) THEN
    DISCH_THEN(\th. GEN_REWRITE_TAC RAND_CONV [] [GSYM th]) THEN
    AP_TERM_TAC THEN REWRITE_TAC[real_div] THEN
    ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
    GEN_REWRITE_TAC RAND_CONV [] [GSYM REAL_MUL_LID] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN
    REWRITE_TAC[REAL_INJ; NOT_SUC]);;

  let ROOT_POS_POW_LE = prove_thm(`ROOT_POS_POW_LE`,
    "!n x. &0 <= x ==> (root(SUC n) (x pow (SUC n)) = x)",
    REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN
    DISCH_THEN(DISJ_CASES_THEN2 MP_TAC (SUBST1_TAC o SYM)) THEN
    REWRITE_TAC[ROOT_POS_POW_LT; ROOT_0; POW_0]);;

  let SQRT_POW_POS = prove_thm(`SQRT_POW_POS`,
    "!x. &0 <= x ==> (sqrt(x pow 2) = abs x)",
    GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[sqrt; num_CONV "2"] THEN
    FIRST_ASSUM(\th. REWRITE_TAC[MATCH_MP ROOT_POS_POW_LE th]) THEN
    ASM_REWRITE_TAC[abs]);;

  let SQRT_POW = prove_thm(`SQRT_POW`,
    "!x. sqrt(x pow 2) = abs x",
    GEN_TAC THEN DISJ_CASES_THEN MP_TAC (SPEC "x:real" REAL_LE_NEGTOTAL) THEN
    DISCH_THEN(MP_TAC o MATCH_MP SQRT_POW_POS) THEN REWRITE_TAC[ABS_NEG] THEN
    REWRITE_TAC[POW_2; GSYM REAL_NEG_LMUL; GSYM REAL_NEG_RMUL; REAL_NEGNEG]);;

John.