new directory HOL/Real/ex of real examples
authorpaulson
Mon Aug 30 15:25:16 1999 +0200 (1999-08-30)
changeset 73924137c951b36b
parent 7391 b7ca64c8fa64
child 7393 c6ce498b4767
new directory HOL/Real/ex of real examples
src/HOL/IsaMakefile
src/HOL/Real/ex/BinEx.ML
src/HOL/Real/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Aug 30 14:11:47 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 30 15:25:16 1999 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
     1.5    HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML \
     1.6    HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
     1.7 -  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples TLA-Inc \
     1.8 -  TLA-Buffer TLA-Memory
     1.9 +  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-Ex \
    1.10 +  TLA-Inc TLA-Buffer TLA-Memory
    1.11  
    1.12  all: images test
    1.13  
    1.14 @@ -85,6 +85,11 @@
    1.15    Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
    1.16  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
    1.17  
    1.18 +## HOL-Real-Ex
    1.19 +
    1.20 +HOL-Real-Ex: HOL-Real $(LOG)/HOL-Real-Ex.gz
    1.21 +
    1.22 +$(LOG)/HOL-Real-Ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML Real/ex/BinEx.ML
    1.23  
    1.24  ## HOL-Subst
    1.25  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Real/ex/BinEx.ML	Mon Aug 30 15:25:16 1999 +0200
     2.3 @@ -0,0 +1,69 @@
     2.4 +(*  Title:      HOL/Real/ex/BinEx.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1999  University of Cambridge
     2.8 +
     2.9 +Examples of performing binary arithmetic by simplification
    2.10 +This time we use the reals, though the representation is just of integers.
    2.11 +*)
    2.12 +
    2.13 +(*** Addition ***)
    2.14 +
    2.15 +Goal "(#1359::real)  +  #-2468 = #-1109";
    2.16 +by (Simp_tac 1);
    2.17 +result();
    2.18 +
    2.19 +Goal "(#93746::real) +  #-46375 = #47371";
    2.20 +by (Simp_tac 1);
    2.21 +result();
    2.22 +
    2.23 +(*** Negation ***)
    2.24 +
    2.25 +Goal "- (#65745::real) = #-65745";
    2.26 +by (Simp_tac 1);
    2.27 +result();
    2.28 +
    2.29 +Goal "- (#-54321::real) = #54321";
    2.30 +by (Simp_tac 1);
    2.31 +result();
    2.32 +
    2.33 +
    2.34 +(*** Multiplication ***)
    2.35 +
    2.36 +Goal "(#-84::real)  *  #51 = #-4284";
    2.37 +by (Simp_tac 1);
    2.38 +result();
    2.39 +
    2.40 +Goal "(#255::real)  *  #255 = #65025";
    2.41 +by (Simp_tac 1);
    2.42 +result();
    2.43 +
    2.44 +Goal "(#1359::real)  *  #-2468 = #-3354012";
    2.45 +by (Simp_tac 1);
    2.46 +result();
    2.47 +
    2.48 +(*** Inequalities ***)
    2.49 +
    2.50 +Goal "(#89::real) * #10 ~= #889";  
    2.51 +by (Simp_tac 1); 
    2.52 +result();
    2.53 +
    2.54 +Goal "(#13::real) < #18 - #4";  
    2.55 +by (Simp_tac 1); 
    2.56 +result();
    2.57 +
    2.58 +Goal "(#-345::real) < #-242 + #-100";  
    2.59 +by (Simp_tac 1); 
    2.60 +result();
    2.61 +
    2.62 +Goal "(#13557456::real) < #18678654";  
    2.63 +by (Simp_tac 1); 
    2.64 +result();
    2.65 +
    2.66 +Goal "(#999999::real) <= (#1000001 + #1)-#2";  
    2.67 +by (Simp_tac 1); 
    2.68 +result();
    2.69 +
    2.70 +Goal "(#1234567::real) <= #1234567";  
    2.71 +by (Simp_tac 1); 
    2.72 +result();
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Real/ex/ROOT.ML	Mon Aug 30 15:25:16 1999 +0200
     3.3 @@ -0,0 +1,12 @@
     3.4 +(*  Title:      HOL/Real/ex/ROOT
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1999  University of Cambridge
     3.8 +
     3.9 +HOL/Real examples
    3.10 +*)
    3.11 +
    3.12 +writeln "Root file for HOL/Real examples";
    3.13 +
    3.14 +set proof_timing;
    3.15 +