New files.

1 files changed, 83 insertions, 0 deletions

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;