From 1e3adb3b850d4cf863463e1231fcecf36020e106 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 16 Apr 2004 09:41:45 +0000 Subject: New files. --- hol98/root2.sml | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 hol98/root2.sml (limited to 'hol98') diff --git a/hol98/root2.sml b/hol98/root2.sml new file mode 100644 index 00000000..0644fc3e --- /dev/null +++ b/hol98/root2.sml @@ -0,0 +1,83 @@ +(* Example proof by Konrad Slind. See http://www.cs.kun.nl/~freek/comparison/ + Taken from HOL4 distribution hol98/examples/root2.sml *) + +(*---------------------------------------------------------------------------*) +(* Challenge from Freek Wiedijk: the square root of two is not rational. *) +(* I've adapted a proof in HOL Light by John Harrison. *) +(*---------------------------------------------------------------------------*) + +load "transcTheory"; open arithmeticTheory BasicProvers; + +(*---------------------------------------------------------------------------*) +(* Need a predicate on reals that picks out the rational ones *) +(*---------------------------------------------------------------------------*) + +val Rational_def = Define `Rational r = ?p q. ~(q=0) /\ (abs(r) = &p / &q)`; + +(*---------------------------------------------------------------------------*) +(* Trivial lemmas *) +(*---------------------------------------------------------------------------*) + +val EXP_2 = Q.prove(`!n:num. n**2 = n*n`, + REWRITE_TAC [TWO,ONE,EXP] THEN RW_TAC arith_ss []); + +val EXP2_LEM = Q.prove(`!x y:num. ((2*x)**2 = 2*(y**2)) = (2*(x**2) = y**2)`, + REWRITE_TAC [TWO,EXP_2] + THEN PROVE_TAC [MULT_MONO_EQ,MULT_ASSOC,MULT_SYM]); + +(*---------------------------------------------------------------------------*) +(* Lemma: squares are not doublings of squares, except trivially. *) +(*---------------------------------------------------------------------------*) + +val lemma = Q.prove +(`!m n. (m**2 = 2 * n**2) ==> (m=0) /\ (n=0)`, + completeInduct_on `m` THEN NTAC 2 STRIP_TAC THEN + `?k. m = 2*k` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT,EVEN_EXISTS] + THEN VAR_EQ_TAC THEN + `?p. n = 2*p` by PROVE_TAC[EVEN_DOUBLE,EXP_2,EVEN_MULT, + EVEN_EXISTS,EXP2_LEM] + THEN VAR_EQ_TAC THEN + `k**2 = 2*(p**2)` by PROVE_TAC [EXP2_LEM] THEN + `(k=0) \/ k < 2*k` by numLib.ARITH_TAC + THENL [FULL_SIMP_TAC arith_ss [EXP_2], + PROVE_TAC [MULT_EQ_0, DECIDE (Term `~(2 = 0n)`)]]); + +(*---------------------------------------------------------------------------*) +(* The proof moves the problem from R to N, then uses lemma *) +(*---------------------------------------------------------------------------*) + +local open realTheory transcTheory +in +val SQRT_2_IRRATIONAL = Q.prove +(`~Rational (sqrt 2r)`, + RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS] + THEN Cases_on `q = 0` THEN ASM_REWRITE_TAC [] + THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`) + THEN RW_TAC arith_ss [SQRT_POW_2, REAL_POS, REAL_POW_DIV, + REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT] + THEN REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL, REAL_INJ] + THEN PROVE_TAC [lemma]) +end; + +(*---------------------------------------------------------------------------*) +(* The following is a bit more declarative *) +(*---------------------------------------------------------------------------*) + +infix THEN1; +fun ie q tac = Q_TAC SUFF_TAC q THEN1 tac; + +local open realTheory transcTheory +in +val SQRT_2_IRRATIONAL = Q.prove +(`~Rational (sqrt 2r)`, + ie `!p q. ~(q=0) ==> ~(sqrt 2 = & p / & q)` + (RW_TAC std_ss [Rational_def,abs,SQRT_POS_LE,REAL_POS] + THEN PROVE_TAC[]) THEN RW_TAC std_ss [] THEN + ie `~(sqrt 2 = & p / & q)` (PROVE_TAC []) THEN + ie `~(2 * q**2 = p**2)` + (DISCH_TAC THEN SPOSE_NOT_THEN (MP_TAC o Q.AP_TERM `\x. x pow 2`) + THEN RW_TAC arith_ss [SQRT_POW_2,REAL_POS, + REAL_POW_DIV,REAL_EQ_RDIV_EQ,REAL_LT, REAL_POW_LT] + THEN ASM_REWRITE_TAC [REAL_OF_NUM_POW, REAL_MUL,REAL_INJ]) + THEN PROVE_TAC [lemma]) +end; -- cgit v1.2.3