added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
authorwenzelm
Tue May 16 13:01:22 2006 +0200 (2006-05-16)
changeset 1964040ec89317425
parent 19639 d9079a9ccbfb
child 19641 f1de44e61ec1
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy
src/HOL/Complex/ex/ROOT.ML
src/HOL/IsaMakefile
src/HOL/Real/Ferrante_Rackoff.thy
src/HOL/Real/Real.thy
src/HOL/Real/ferrante_rackoff.ML
src/HOL/Real/ferrante_rackoff_proof.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy	Tue May 16 13:01:22 2006 +0200
     1.3 @@ -0,0 +1,169 @@
     1.4 +(*
     1.5 +    ID:         $Id$
     1.6 +    Author:     Amine Chaieb, TU Muenchen
     1.7 +
     1.8 +Examples for Ferrante and Rackoff Algorithm.
     1.9 +*)
    1.10 +
    1.11 +theory Ferrante_Rackoff_Ex
    1.12 +imports Complex_Main
    1.13 +begin
    1.14 +
    1.15 +lemma "~ (ALL (x::real) y. x < y --> 10*x < 11*y)"
    1.16 +apply ferrack
    1.17 +done
    1.18 +
    1.19 +lemma "ALL (x::real) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
    1.20 +apply ferrack
    1.21 +done
    1.22 +
    1.23 +lemma "EX (x::real) y. x ~= y --> x < y"
    1.24 +  apply ferrack
    1.25 +  done
    1.26 +
    1.27 +lemma "EX (x::real) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
    1.28 +  apply ferrack
    1.29 +  done
    1.30 +lemma "ALL (x::real) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
    1.31 +  apply ferrack
    1.32 +  done
    1.33 +
    1.34 +  (* 1 Alternations *)
    1.35 +lemma "ALL (x::real). (EX (y::real). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
    1.36 +  by ferrack
    1.37 +lemma "ALL (x::real) < 0. (EX (y::real) > 0. 7*x + y > 0 & x - y <= 9)"
    1.38 +  by ferrack
    1.39 +lemma "EX (x::real). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
    1.40 +  apply ferrack
    1.41 +  done
    1.42 +lemma "EX (x::real). (ALL y. y < 2 -->  2*(y - x) \<le> 0 )"
    1.43 +  apply ferrack
    1.44 +  done
    1.45 +lemma "ALL (x::real). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
    1.46 +  apply ferrack
    1.47 +  done
    1.48 +    (* Formulae with 3 quantifiers *)
    1.49 +  (* 0 Alternations *)
    1.50 +lemma "ALL (x::real) y z. x + y < z --> y >= z --> x < 0"
    1.51 +apply ferrack
    1.52 +done
    1.53 +lemma "EX (x::real) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
    1.54 +apply ferrack
    1.55 +done
    1.56 +lemma "ALL (x::real) y z. abs (x + y) <= z --> (abs z = z)"
    1.57 +apply ferrack
    1.58 +done
    1.59 +
    1.60 +lemma "EX (x::real) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
    1.61 +apply ferrack
    1.62 +done
    1.63 +
    1.64 +lemma "ALL (x::real) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))"
    1.65 +apply ferrack
    1.66 +done
    1.67 +  (* 1 Alternations *)
    1.68 +lemma "ALL (x::real) y. x < y --> (EX z>0. x+z = y)"
    1.69 +  by ferrack
    1.70 +lemma "ALL (x::real) y. (EX z>0. abs (x - y) <= z )"
    1.71 +  by ferrack
    1.72 +
    1.73 +lemma "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    1.74 +  apply ferrack
    1.75 +  done
    1.76 +
    1.77 +lemma "EX (x::real) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
    1.78 +  apply ferrack
    1.79 +  done
    1.80 +lemma "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
    1.81 +  apply ferrack
    1.82 +  done
    1.83 +  (* 2 Alternations *)
    1.84 +lemma "EX (x::real)>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
    1.85 +  apply ferrack
    1.86 +  done
    1.87 +lemma "EX (x::real). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \<noteq> 0 \<longrightarrow> (EX z. 5*x - 3*abs y <= 7*z))"
    1.88 +  apply ferrack
    1.89 +  done
    1.90 +
    1.91 +lemma "ALL (x::real). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" 
    1.92 +  apply ferrack
    1.93 +  done
    1.94 +
    1.95 +lemma "ALL (x::real). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" 
    1.96 +  apply ferrack
    1.97 +  done
    1.98 +
    1.99 +lemma "EX (x::real). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
   1.100 +  apply ferrack
   1.101 +  done
   1.102 +
   1.103 +    (* Formulae with 4 quantifiers *)
   1.104 +    (* 0 Alternations *)
   1.105 +lemma "ALL (x::real) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
   1.106 +  apply ferrack
   1.107 +  done
   1.108 +lemma "ALL (x::real) y. ALL z >x. ALL w > y. abs (z-x) + abs (y-w + x) <= z - x + w-y+abs x"
   1.109 +  apply ferrack
   1.110 +  done
   1.111 +lemma "EX (x::real) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
   1.112 +  apply ferrack
   1.113 +  done
   1.114 +
   1.115 +lemma "EX (x::real) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
   1.116 +  apply ferrack
   1.117 +  done
   1.118 +
   1.119 +lemma "EX (x::real) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)"
   1.120 +  apply ferrack
   1.121 +  done
   1.122 +    (* 1 Alternations *)
   1.123 +lemma "ALL (x::real) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
   1.124 +  apply ferrack
   1.125 +  done
   1.126 +lemma "~(ALL (x::real). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
   1.127 +  apply ferrack
   1.128 +  done
   1.129 +lemma "ALL (x::real) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
   1.130 +  apply ferrack
   1.131 +  done
   1.132 +lemma "ALL (x::real). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))"
   1.133 +  apply ferrack
   1.134 +  done
   1.135 +lemma "EX (x::real) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
   1.136 +  apply ferrack
   1.137 +  done
   1.138 +    (* 2 Alternations *)
   1.139 +lemma "EX z. (ALL (x::real) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
   1.140 +  apply ferrack
   1.141 +  done
   1.142 +lemma "EX z. (ALL (x::real) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
   1.143 +  apply ferrack
   1.144 +  done
   1.145 +lemma "ALL (x::real) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
   1.146 +  apply ferrack
   1.147 +  done
   1.148 +lemma "EX y. (ALL (x::real). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))"
   1.149 +  apply ferrack
   1.150 +  done
   1.151 +lemma "EX (x::real) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
   1.152 +  apply ferrack
   1.153 +  done
   1.154 +    (* 3 Alternations *)
   1.155 +lemma "EX (x::real). (ALL y < x. (EX z > (x+y). 
   1.156 +  (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))"
   1.157 +  apply ferrack
   1.158 +  done
   1.159 +lemma "EX (x::real). (ALL y. (EX z > y. 
   1.160 +  (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
   1.161 +  apply ferrack
   1.162 +  done
   1.163 +lemma "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
   1.164 +  apply ferrack
   1.165 +  done
   1.166 +lemma "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
   1.167 +  apply ferrack
   1.168 +  done
   1.169 +lemma "ALL (x::real). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))"
   1.170 +  apply ferrack
   1.171 +  done
   1.172 +end
     2.1 --- a/src/HOL/Complex/ex/ROOT.ML	Tue May 16 09:19:12 2006 +0200
     2.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Tue May 16 13:01:22 2006 +0200
     2.3 @@ -20,3 +20,5 @@
     2.4  
     2.5  no_document use_thy "NatPair";
     2.6  use_thy "DenumRat";
     2.7 +
     2.8 +use_thy "Ferrante_Rackoff_Ex";
     3.1 --- a/src/HOL/IsaMakefile	Tue May 16 09:19:12 2006 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue May 16 13:01:22 2006 +0200
     3.3 @@ -156,11 +156,11 @@
     3.4  HOL-Complex: HOL $(OUT)/HOL-Complex
     3.5  
     3.6  $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy			\
     3.7 -  Real/Lubs.thy Real/rat_arith.ML						\
     3.8 -  Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
     3.9 -  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
    3.10 -  Real/RealPow.thy Real/document/root.tex					\
    3.11 -  Real/Float.thy Real/Float.ML                                                  \
    3.12 +  Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/Float.ML			\
    3.13 +  Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy		\
    3.14 +  Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy			\
    3.15 +  Real/RealPow.thy Real/document/root.tex Real/ferrante_rackoff_proof.ML	\
    3.16 +  Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML			\
    3.17    Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
    3.18    Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
    3.19    Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
    3.20 @@ -185,7 +185,7 @@
    3.21  
    3.22  $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
    3.23    Complex/ex/ROOT.ML Complex/ex/document/root.tex \
    3.24 -  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
    3.25 +  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy Complex/ex/Ferrante_Rackoff_Ex.thy \
    3.26    Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
    3.27  	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
    3.28  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Real/Ferrante_Rackoff.thy	Tue May 16 13:01:22 2006 +0200
     4.3 @@ -0,0 +1,487 @@
     4.4 +(*
     4.5 +    ID:         $Id$
     4.6 +    Author:     Amine Chaieb, TU Muenchen
     4.7 +
     4.8 +Ferrante and Rackoff Algorithm: LCF-proof-synthesis version.
     4.9 +*)
    4.10 +
    4.11 +theory Ferrante_Rackoff
    4.12 +imports RealPow
    4.13 +uses ("ferrante_rackoff_proof.ML") ("ferrante_rackoff.ML")
    4.14 +begin
    4.15 +
    4.16 +  (* Synthesis of \<exists>z. \<forall>x<z. P x = P1 *)
    4.17 +lemma minf: 
    4.18 +  "\<exists>(z::real) . \<forall>x<z. x < t = True "  "\<exists>(z::real) . \<forall>x<z. x > t = False "
    4.19 +  "\<exists>(z::real) . \<forall>x<z. x \<le> t = True "  "\<exists>(z::real) . \<forall>x<z. x \<ge> t = False "
    4.20 +  "\<exists>(z::real) . \<forall>x<z. (x = t) = False "  "\<exists>(z::real) . \<forall>x<z. (x \<noteq> t) = True "
    4.21 +  "\<exists>z. \<forall>(x::real)<z. (P::bool) = P"
    4.22 +  "\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
    4.23 +  \<exists>z. \<forall>x<z. (P1 x \<and> P2 x) = (P1' \<and> P2')"
    4.24 +  "\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
    4.25 +  \<exists>z. \<forall>x<z. (P1 x \<or> P2 x) = (P1' \<or> P2')"
    4.26 +  by (rule_tac x="t" in exI,simp)+
    4.27 +(clarsimp,rule_tac x="min z1 z2" in exI,simp)+
    4.28 +
    4.29 +lemma minf_ex: "\<lbrakk>\<exists>z. \<forall>x<z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x"
    4.30 +  by clarsimp (rule_tac x="z - 1" in exI, auto)
    4.31 +
    4.32 +  (* Synthesis of \<exists>z. \<forall>x>z. P x = P1 *)
    4.33 +lemma pinf: 
    4.34 +  "\<exists>(z::real) . \<forall>x>z. x < t = False "  "\<exists>(z::real) . \<forall>x>z. x > t = True "
    4.35 +  "\<exists>(z::real) . \<forall>x>z. x \<le> t = False "  "\<exists>(z::real) . \<forall>x>z. x \<ge> t = True "
    4.36 +  "\<exists>(z::real) . \<forall>x>z. (x = t) = False "  "\<exists>(z::real) . \<forall>x>z. (x \<noteq> t) = True "
    4.37 +  "\<exists>z. \<forall>(x::real)>z. (P::bool) = P"
    4.38 +  "\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
    4.39 +  \<exists>z. \<forall>x>z. (P1 x \<and> P2 x) = (P1' \<and> P2')"
    4.40 +  "\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
    4.41 +  \<exists>z. \<forall>x>z. (P1 x \<or> P2 x) = (P1' \<or> P2')"
    4.42 +  by (rule_tac x="t" in exI,simp)+
    4.43 +(clarsimp,rule_tac x="max z1 z2" in exI,simp)+
    4.44 +
    4.45 +lemma pinf_ex: "\<lbrakk>\<exists>z. \<forall>x>z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x"
    4.46 +  by clarsimp (rule_tac x="z+1" in exI, auto)
    4.47 +
    4.48 +    (* The ~P1 \<and> ~P2 \<and> P x \<longrightarrow> \<exists> u,u' \<in> U. u \<le> x \<le> u'*)
    4.49 +lemma nmilbnd: 
    4.50 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.51 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) > t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.52 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.53 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) \<ge> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.54 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.55 +  "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )"
    4.56 +  "\<forall> (x::real). ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )"
    4.57 +  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ; 
    4.58 +  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> 
    4.59 +  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.60 +  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ; 
    4.61 +  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> 
    4.62 +  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    4.63 +  by auto (rule_tac x="t" in bexI,simp,simp)
    4.64 +
    4.65 +lemma npiubnd: 
    4.66 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) < t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.67 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) > t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.68 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) \<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.69 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<ge> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.70 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) = t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.71 +  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )"
    4.72 +  "\<forall> (x::real). ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )"
    4.73 +  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )\<rbrakk> 
    4.74 +  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.75 +  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )\<rbrakk> 
    4.76 +  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
    4.77 +  by auto (rule_tac x="t" in bexI,simp,simp)
    4.78 +lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)\<rbrakk> 
    4.79 +  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
    4.80 +by auto
    4.81 +
    4.82 +  (* Synthesis of  (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x<u \<and> P x \<and> l < y < u \<longrightarrow> P y*)
    4.83 +lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y< t)"
    4.84 +proof(clarsimp)
    4.85 +  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" 
    4.86 +    and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
    4.87 +  from tU noU ly yu have tny: "t\<noteq>y" by auto
    4.88 +  {assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp 
    4.89 +    with tU noU have "False" by auto} hence "\<not> y>t"  by auto hence "y \<le> t" by auto
    4.90 +  thus "y < t" using tny by simp 
    4.91 +qed
    4.92 +    
    4.93 +lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) > t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y> t)"
    4.94 +proof(clarsimp)
    4.95 +  fix x l u y
    4.96 +  assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
    4.97 +  and px: "x > t" and ly: "l<y" and yu:"y < u"
    4.98 +  from tU noU ly yu have tny: "t\<noteq>y" by auto
    4.99 +  {assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp 
   4.100 +    with tU noU have "False" by auto}
   4.101 +  hence	"\<not> y<t"  by auto hence "y \<ge> t" by auto
   4.102 +  thus "y > t" using tny by simp 
   4.103 +qed
   4.104 +lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
   4.105 +proof(clarsimp)
   4.106 +  fix x l u y
   4.107 +  assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   4.108 +  and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
   4.109 +  from tU noU ly yu have tny: "t\<noteq>y" by auto
   4.110 +  {assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp 
   4.111 +    with tU noU have "False" by auto}
   4.112 +  hence	"\<not> y>t"  by auto thus "y \<le> t" by auto
   4.113 +qed
   4.114 +    
   4.115 +lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<ge> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<ge> t)"
   4.116 +proof(clarsimp)
   4.117 +  fix x l u y
   4.118 +  assume tU: "t \<in> U" and noU: "\<forall>t\<Colon>real. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   4.119 +  and px: "x \<ge> t" and ly: "l<y" and yu:"y < u"
   4.120 +  from tU noU ly yu have tny: "t\<noteq>y" by auto
   4.121 +  {assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp 
   4.122 +    with tU noU have "False" by auto}
   4.123 +  hence	"\<not> y<t"  by auto thus "y \<ge> t" by auto
   4.124 +qed
   4.125 +lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"  by auto
   4.126 +lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (x::real) \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"  by auto
   4.127 +lemma lin_dense_fm: "\<forall>(x::real) l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"  by auto
   4.128 +
   4.129 +lemma lin_dense_conj: 
   4.130 +  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 (x::real) 
   4.131 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;  
   4.132 +  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 (x::real) 
   4.133 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
   4.134 +  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x) 
   4.135 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   4.136 +  by blast
   4.137 +lemma lin_dense_disj: 
   4.138 +  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 (x::real) 
   4.139 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;  
   4.140 +  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 (x::real) 
   4.141 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
   4.142 +  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x) 
   4.143 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
   4.144 +  by blast
   4.145 +
   4.146 +lemma finite_set_intervals:
   4.147 +  assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
   4.148 +  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   4.149 +  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
   4.150 +proof-
   4.151 +  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
   4.152 +  let ?xM = "{y. y\<in> S \<and> x \<le> y}"
   4.153 +  let ?a = "Max ?Mx"
   4.154 +  let ?b = "Min ?xM"
   4.155 +  have MxS: "?Mx \<subseteq> S" by blast
   4.156 +  hence fMx: "finite ?Mx" using fS finite_subset by auto
   4.157 +  from lx linS have linMx: "l \<in> ?Mx" by blast
   4.158 +  hence Mxne: "?Mx \<noteq> {}" by blast
   4.159 +  have xMS: "?xM \<subseteq> S" by blast
   4.160 +  hence fxM: "finite ?xM" using fS finite_subset by auto
   4.161 +  from xu uinS have linxM: "u \<in> ?xM" by blast
   4.162 +  hence xMne: "?xM \<noteq> {}" by blast
   4.163 +  have ax:"?a \<le> x" using Mxne fMx by auto
   4.164 +  have xb:"x \<le> ?b" using xMne fxM by auto
   4.165 +  have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
   4.166 +  have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
   4.167 +  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
   4.168 +  proof(clarsimp)
   4.169 +    fix y   assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
   4.170 +    from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto
   4.171 +    moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp}
   4.172 +    moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp}
   4.173 +    ultimately show "False" by blast
   4.174 +  qed
   4.175 +  from ainS binS noy ax xb px show ?thesis by blast
   4.176 +qed
   4.177 +
   4.178 +lemma finite_set_intervals2:
   4.179 +  assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
   4.180 +  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   4.181 +  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
   4.182 +proof-
   4.183 +  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
   4.184 +  obtain a and b where 
   4.185 +    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" 
   4.186 +    and axb: "a \<le> x \<and> x \<le> b \<and> P x"  by auto
   4.187 +  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
   4.188 +  thus ?thesis using px as bs noS by blast 
   4.189 +qed
   4.190 +
   4.191 +lemma rinf_U:
   4.192 +  assumes fU: "finite U" 
   4.193 +  and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x 
   4.194 +  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
   4.195 +  and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
   4.196 +  and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P (x::real)"
   4.197 +  shows "\<exists> u\<in> U. \<exists> u' \<in> U. P ((u + u') / 2)" 
   4.198 +proof-
   4.199 +  from ex obtain x where px: "P x" by blast
   4.200 +  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u'" by auto
   4.201 +  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<le> x" and xu':"x \<le> u'" by auto 
   4.202 +  from uU have Une: "U \<noteq> {}" by auto
   4.203 +  let ?l = "Min U"
   4.204 +  let ?u = "Max U"
   4.205 +  have linM: "?l \<in> U" using fU Une by simp
   4.206 +  have uinM: "?u \<in> U" using fU Une by simp
   4.207 +  have lM: "\<forall> t\<in> U. ?l \<le> t" using Une fU by auto
   4.208 +  have Mu: "\<forall> t\<in> U. t \<le> ?u" using Une fU by auto
   4.209 +  have "?l \<le> u" using uU Une lM by auto hence lx: "?l \<le> x" using ux by simp
   4.210 +  have "u' \<le> ?u" using uU' Une Mu by simp hence xu: "x \<le> ?u" using xu' by simp
   4.211 +  from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
   4.212 +  have "(\<exists> s\<in> U. P s) \<or> 
   4.213 +      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x)" .
   4.214 +  moreover { fix u assume um: "u\<in>U" and pu: "P u"
   4.215 +    have "(u + u) / 2 = u" by auto 
   4.216 +    with um pu have "P ((u + u) / 2)" by simp
   4.217 +    with um have ?thesis by blast}
   4.218 +  moreover{
   4.219 +    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x"
   4.220 +      then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" 
   4.221 +	and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U" and t1x: "t1 < x" and xt2: "x < t2" and px: "P x"
   4.222 +	by blast
   4.223 +      from t1x xt2 have t1t2: "t1 < t2" by simp
   4.224 +      let ?u = "(t1 + t2) / 2"
   4.225 +      from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto
   4.226 +      from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
   4.227 +      with t1M t2M have ?thesis by blast}
   4.228 +    ultimately show ?thesis by blast
   4.229 +  qed
   4.230 +
   4.231 +theorem fr_eq: 
   4.232 +  assumes fU: "finite U"
   4.233 +  and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x 
   4.234 +   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
   4.235 +  and nmibnd: "\<forall>x. \<not> MP \<and> P (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
   4.236 +  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)"
   4.237 +  and mi: "\<exists>z. \<forall>x<z. P x = MP"  and pi: "\<exists>z. \<forall>x>z. P x = PP"
   4.238 +  shows "(\<exists> x. P (x::real)) = (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P ((u + u') / 2)))" 
   4.239 +  (is "_ = (_ \<or> _ \<or> ?F)" is "?E = ?D")
   4.240 +proof
   4.241 +  assume px: "\<exists> x. P x"
   4.242 +  have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
   4.243 +  moreover {assume "MP \<or> PP" hence "?D" by blast}
   4.244 +  moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
   4.245 +    from npmibnd[OF nmibnd npibnd] 
   4.246 +    have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" .
   4.247 +    from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}   
   4.248 +  ultimately show "?D" by blast
   4.249 +next
   4.250 +  assume "?D" 
   4.251 +  moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .}
   4.252 +  moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
   4.253 +  moreover {assume f:"?F" hence "?E" by blast}
   4.254 +  ultimately show "?E" by blast
   4.255 +qed
   4.256 +
   4.257 +lemma fr_simps: 
   4.258 +  "(True | P) = True"  "(P | True) = True"  "(True & P) = P"  "(P & True) = P"
   4.259 +  "(P & P) = P"  "(P & (P & P')) = (P & P')"  "(P & (P | P')) = P"  "(False | P) = P"
   4.260 +  "(P | False) = P"  "(False & P) = False"  "(P & False) = False"  "(P | P) = P"
   4.261 +  "(P | (P | P')) = (P | P')"  "(P | (P & P')) = P"  "(~ True) = False"  "(~ False) = True"
   4.262 +  "(x::real) \<le> x"  "(\<exists> u\<in> {}. Q u) = False"
   4.263 +  "(\<exists> u\<in> (insert (x::real) U). \<exists>u'\<in> (insert x U). R ((u+u') / 2)) = 
   4.264 +  ((R x) \<or> (\<exists>u\<in>U. R((x+u) / 2))\<or> (\<exists> u\<in> U. \<exists> u'\<in> U. R ((u + u') /2)))"
   4.265 +  "(\<exists> u\<in> (insert (x::real) U). R u) = (R x \<or> (\<exists> u\<in> U. R u))"
   4.266 +  "Q' (((t::real) + t)/2) = Q' t"
   4.267 +by (auto simp add: add_ac)
   4.268 +  
   4.269 +lemma fr_prepqelim:
   4.270 +  "(\<exists> x. True) = True" "(\<exists> x. False) = False" "(ALL x. A x) = (~ (EX x. ~ (A x)))"
   4.271 +  "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" "(\<not> (P \<longrightarrow> Q)) = (P \<and> (\<not> Q))" "(\<not> (P = Q)) = ((\<not> P) = Q)" 
   4.272 +  "(\<not> (P \<and> Q)) = ((\<not> P) \<or> (\<not> Q))" "(\<not> (P \<or> Q)) = ((\<not> P) \<and> (\<not> Q))"
   4.273 +by auto
   4.274 +  (* Lemmas for the normalization of Expressions *)
   4.275 +lemma nadd_cong:  
   4.276 +  assumes m: "m'*m = l" and n: "n'*n = (l::real)"
   4.277 +  and mz: "m \<noteq> 0" and nz: "n \<noteq> 0" and lz: "l \<noteq> 0"
   4.278 +  and ad: "(m'*t + n'*s) = t'"
   4.279 +  shows "t/m + s/n = (t' / l)"
   4.280 +proof-
   4.281 +  from lz m n have mz': "m'\<noteq>0" and nz':"n' \<noteq> 0" by auto
   4.282 +  have "t' / l = (m'*t + n'*s) / l" using ad by simp
   4.283 +  also have "\<dots> = (m'*t) / l + (n'*s) / l" by (simp add: add_divide_distrib)
   4.284 +  also have "\<dots> = (m'*t) /(m'*m) + (n'*s) /(n'*n)" using m n by simp
   4.285 +  also have "\<dots> = t/m + s/n" using mz nz mz' nz' by simp
   4.286 +  finally show ?thesis  by simp
   4.287 +qed
   4.288 +
   4.289 +lemma nadd_cong_same: "\<lbrakk> (n::real) = m ; t+s = t'\<rbrakk> \<Longrightarrow> t/n + s/m = t'/n"  
   4.290 +  by (simp add: add_divide_distrib[symmetric])
   4.291 +lemma plus_cong: "\<lbrakk>t = t'; s = s'; t' + s' = r\<rbrakk> \<Longrightarrow> t+s = r"
   4.292 +  by simp
   4.293 +lemma diff_cong: "\<lbrakk>t = t'; s = s'; t' - s' = r\<rbrakk> \<Longrightarrow> t-s = r"
   4.294 +  by simp
   4.295 +lemma mult_cong2: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> t*c = r"
   4.296 +  by (simp add: mult_ac)
   4.297 +lemma mult_cong: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> c*t = r"
   4.298 +  by simp
   4.299 +lemma divide_cong: "\<lbrakk> (t::real) = t' ; t'/n = r\<rbrakk> \<Longrightarrow> t/n = r"
   4.300 +  by simp
   4.301 +lemma naddh_cong_ts: "\<lbrakk>t1 + (s::real) = t'\<rbrakk> \<Longrightarrow> (x + t1) + s = x + t'" by simp
   4.302 +lemma naddh_cong_st: "\<lbrakk>(t::real) + s = t'\<rbrakk> \<Longrightarrow> t+ (x + s) = x + t'" by simp
   4.303 +lemma naddh_cong_same: "\<lbrakk>(c1::real) + c2 = c ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = c*x + t"
   4.304 +  by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric])
   4.305 +lemma naddh_cong_same0: "\<lbrakk>(c1::real) + c2 = 0 ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = t"
   4.306 +  by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric]) simp
   4.307 +lemma ncmul_congh: "\<lbrakk> c*c' = (k::real) ; c*t = t'\<rbrakk>  \<Longrightarrow> c*(c'*x + t) = k*x + t'"
   4.308 +  by (simp add: ring_eq_simps)
   4.309 +lemma ncmul_cong: "\<lbrakk> c / n = c'/n' ; c'*t = (t'::real)\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'"
   4.310 +proof-
   4.311 +  assume "c / n = c'/n'" and "c'*t = (t'::real)"
   4.312 +  have "\<lbrakk> c' / n' = c/n ; (t'::real) = c'*t\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'"
   4.313 +    by (simp add: divide_inverse ring_eq_simps)  thus ?thesis using prems by simp
   4.314 +qed
   4.315 +
   4.316 +lemma nneg_cong: "(-1 ::real)*t = t' \<Longrightarrow> - t = t'"  by simp
   4.317 +lemma uminus_cong: "\<lbrakk> t = t' ; - t' = r\<rbrakk> \<Longrightarrow>  - t = r"  by simp
   4.318 +lemma nsub_cong: "\<lbrakk>- (s::real) = s'; t + s' = t'\<rbrakk> \<Longrightarrow> t - s = t'"  by simp
   4.319 +lemma ndivide_cong: "m*n = (m'::real) \<Longrightarrow> (t/m) / n = t / m'"  by simp
   4.320 +lemma normalizeh_var: "(x::real) = (1*x + 0) / 1"  by simp
   4.321 +lemma nrefl: "(x::real) = x/1"  by simp
   4.322 +
   4.323 +    (* cong rules for atoms normalization *)
   4.324 +  (* the < -case *)
   4.325 +lemma normalize_ltxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.326 +  and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0"
   4.327 +  shows "(s < t) = (x < r'/c')"
   4.328 +proof-
   4.329 +  from cnp have cnz: "c \<noteq> 0" by auto
   4.330 +  from cnp have nnz: "n\<noteq>0" by auto
   4.331 +  from rr' have rr'': "-(r/c) = r'/c'" by simp
   4.332 +  have "s < t = (s - t < 0)" by simp
   4.333 +  also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp
   4.334 +  also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib)
   4.335 +  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) < (n/c)*0)" 
   4.336 +    using cnp mult_less_cancel_left[where c="(n/c)" and b="0"] by simp 
   4.337 +  also have "\<dots> = (x + r/c < 0)" 
   4.338 +    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
   4.339 +  also have "\<dots> = (x < - (r/c))" by auto
   4.340 +  finally show ?thesis using rr'' by simp
   4.341 +qed
   4.342 +
   4.343 +lemma normalize_ltxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.344 +  and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0"
   4.345 +  shows "(s < t) = (x > r'/c')"
   4.346 +proof-
   4.347 +  from cnp have cnz: "c \<noteq> 0" by auto
   4.348 +  from cnp have nnz: "n\<noteq>0" by auto
   4.349 +  from cnp have cnp': "\<not> (n/c > 0)" by simp
   4.350 +  from rr' have rr'': "-(r/c) = r'/c'" by simp
   4.351 +  have "s < t = (s - t < 0)" by simp
   4.352 +  also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp
   4.353 +  also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib)
   4.354 +  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) > 0)"
   4.355 +    using zero_less_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp cnp' simp_thms]
   4.356 +    by simp 
   4.357 +  also have "\<dots> = (x + r/c > 0)" 
   4.358 +    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
   4.359 +  also have "\<dots> = (x > - (r/c))" by auto
   4.360 +  finally show ?thesis using rr'' by simp
   4.361 +qed
   4.362 +lemma normalize_ltground_cong: "\<lbrakk> s -t = (r::real) ; r < 0 = P\<rbrakk> \<Longrightarrow> s < t = P"  by auto
   4.363 +lemma normalize_ltnoxpos_cong: 
   4.364 +  assumes st: "s - t = (r::real) / n" and mp: "n > 0"
   4.365 +  shows "s < t = (r <0)"
   4.366 +proof-  
   4.367 +  have "s < t = (s - t < 0)" by simp
   4.368 +  also have "\<dots> = (r / n < 0)" using st by simp
   4.369 +  also have "\<dots> = (n* (r/n) < 0)" using mult_less_0_iff[where a="n" and b="r/n"] mp by simp
   4.370 +  finally show ?thesis using mp by auto
   4.371 +qed
   4.372 +
   4.373 +lemma normalize_ltnoxneg_cong: 
   4.374 +  assumes st: "s - t = (r::real) / n" and mp: "n < 0"
   4.375 +  shows "s < t = (r > 0)"
   4.376 +proof-  
   4.377 +  have "s < t = (s - t < 0)" by simp
   4.378 +  also have "\<dots> = (r / n < 0)" using st by simp
   4.379 +  also have "\<dots> = (n* (r/n) > 0)" using zero_less_mult_iff[where a="n" and b="r/n"] mp by simp
   4.380 +  finally show ?thesis using mp by auto
   4.381 +qed
   4.382 +
   4.383 +  (* the <= -case *)
   4.384 +lemma normalize_lexpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.385 +  and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0"
   4.386 +  shows "(s \<le> t) = (x \<le> r'/c')"
   4.387 +proof-
   4.388 +  from cnp have cnz: "c \<noteq> 0" by auto
   4.389 +  from cnp have nnz: "n\<noteq>0" by auto
   4.390 +  from rr' have rr'': "-(r/c) = r'/c'" by simp
   4.391 +  have "s \<le> t = (s - t \<le> 0)" by simp
   4.392 +  also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp
   4.393 +  also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib)
   4.394 +  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<le> (n/c)*0)" 
   4.395 +    using cnp mult_le_cancel_left[where c="(n/c)" and b="0"] by simp 
   4.396 +  also have "\<dots> = (x + r/c \<le> 0)" 
   4.397 +    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
   4.398 +  also have "\<dots> = (x \<le> - (r/c))" by auto
   4.399 +  finally show ?thesis using rr'' by simp
   4.400 +qed
   4.401 +
   4.402 +lemma normalize_lexneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.403 +  and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0"
   4.404 +  shows "(s \<le> t) = (x \<ge> r'/c')"
   4.405 +proof-
   4.406 +  from cnp have cnz: "c \<noteq> 0" by auto
   4.407 +  from cnp have nnz: "n\<noteq>0" by auto
   4.408 +  from cnp have cnp': "\<not> (n/c \<ge> 0) \<and> n/c \<le> 0" by simp
   4.409 +  from rr' have rr'': "-(r/c) = r'/c'" by simp
   4.410 +  have "s \<le> t = (s - t \<le> 0)" by simp
   4.411 +  also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp
   4.412 +  also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib)
   4.413 +  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<ge> 0)"
   4.414 +    using zero_le_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp' simp_thms]
   4.415 +    by simp 
   4.416 +  also have "\<dots> = (x + r/c \<ge> 0)" 
   4.417 +    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
   4.418 +  also have "\<dots> = (x \<ge> - (r/c))" by auto
   4.419 +  finally show ?thesis using rr'' by simp
   4.420 +qed
   4.421 +lemma normalize_leground_cong: "\<lbrakk> s -t = (r::real) ; r \<le> 0 = P\<rbrakk> \<Longrightarrow> s \<le> t = P"  by auto
   4.422 +lemma normalize_lenoxpos_cong: 
   4.423 +  assumes st: "s - t = (r::real) / n" and mp: "n > 0"
   4.424 +  shows "s \<le> t = (r \<le>0)"
   4.425 +proof-  
   4.426 +  have "s \<le> t = (s - t \<le> 0)" by simp
   4.427 +  also have "\<dots> = (r / n \<le> 0)" using st by simp
   4.428 +  also have "\<dots> = (n* (r/n) \<le> 0)" using mult_le_0_iff[where a="n" and b="r/n"] mp by simp
   4.429 +  finally show ?thesis using mp by auto
   4.430 +qed
   4.431 +
   4.432 +lemma normalize_lenoxneg_cong: 
   4.433 +  assumes st: "s - t = (r::real) / n" and mp: "n < 0"
   4.434 +  shows "s \<le> t = (r \<ge> 0)"
   4.435 +proof-  
   4.436 +  have "s \<le> t = (s - t \<le> 0)" by simp
   4.437 +  also have "\<dots> = (r / n \<le> 0)" using st by simp
   4.438 +  also have "\<dots> = (n* (r/n) \<ge> 0)" using zero_le_mult_iff[where a="n" and b="r/n"] mp by simp
   4.439 +  finally show ?thesis using mp by auto
   4.440 +qed
   4.441 +    (* The = -case *)
   4.442 +
   4.443 +lemma normalize_eqxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.444 +  and cp: "c > 0" and nnz: "n \<noteq> 0" and rr': "r+ r' = 0"
   4.445 +  shows "(s = t) = (x = r'/c)"
   4.446 +proof-
   4.447 +  from rr' have rr'': "-r = r'" by simp
   4.448 +  have "(s = t) = (s - t = 0)" by simp
   4.449 +  also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp
   4.450 +  also have "\<dots> = (c*x = -r)" using nnz by auto
   4.451 +  also have "\<dots> = (x = (-r) / c)" using cp eq_divide_eq[where c="c" and a="x" and b="-r"]
   4.452 +    by (simp add: mult_ac)
   4.453 +  finally show ?thesis using rr'' by simp
   4.454 +qed
   4.455 +
   4.456 +lemma normalize_eqxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
   4.457 +  and cp: "c < 0" and nnz: "n \<noteq> 0" and cc': "c+ c' = 0"
   4.458 +  shows "(s = t) = (x = r/c')"
   4.459 +proof-
   4.460 +  from cc' have cc'': "-c = c'" by simp
   4.461 +  have "(s = t) = (s - t = 0)" by simp
   4.462 +  also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp
   4.463 +  also have "\<dots> = ((-c)*x = r)" using nnz by auto
   4.464 +  also have "\<dots> = (x = r / (-c))" using cp eq_divide_eq[where c="-c" and a="x" and b="r"]
   4.465 +    by (simp add: mult_ac)
   4.466 +  finally show ?thesis using cc'' by simp
   4.467 +qed
   4.468 +
   4.469 +lemma normalize_eqnox_cong: "\<lbrakk>s - t = (r::real) / n;n \<noteq> 0\<rbrakk> \<Longrightarrow> s = t = (r = 0)" by auto
   4.470 +
   4.471 +lemma normalize_eqground_cong: "\<lbrakk>s - t =(r::real)/n;n \<noteq> 0;(r = 0) = P \<rbrakk> \<Longrightarrow> s=t = P" by auto
   4.472 +
   4.473 +lemma trivial_sum_of_opposites: "-t = t' \<Longrightarrow> t + t' = (0::real)" by simp
   4.474 +lemma sum_of_opposite_denoms: 
   4.475 +  assumes cc': "(c::real) + c' = 0" shows "r/c + r/c' = 0"
   4.476 +proof-
   4.477 +  from cc' have "c' = -c" by simp
   4.478 +  thus ?thesis by simp
   4.479 +qed
   4.480 +lemma sum_of_same_denoms: " -r = (r'::real) \<Longrightarrow> r/c + r'/c = 0"  by auto
   4.481 +lemma normalize_not_lt: "t \<le> (s::real) = P \<Longrightarrow> (\<not> s<t) = P"  by auto
   4.482 +lemma normalize_not_le: "t < (s::real) = P \<Longrightarrow> (\<not> s\<le>t) = P"  by auto
   4.483 +lemma normalize_not_eq: "\<lbrakk> t = (s::real) = P ; (~P) = P' \<rbrakk> \<Longrightarrow> (s\<noteq>t) = P'"  by auto
   4.484 +lemma ex_eq_cong: "(!! x. A x = B x) \<Longrightarrow> ((\<exists>x. A x) = (\<exists> x. B x))"  by blast
   4.485 +
   4.486 +use "ferrante_rackoff_proof.ML"
   4.487 +use "ferrante_rackoff.ML"
   4.488 +setup "Ferrante_Rackoff.setup"
   4.489 +
   4.490 +end
     5.1 --- a/src/HOL/Real/Real.thy	Tue May 16 09:19:12 2006 +0200
     5.2 +++ b/src/HOL/Real/Real.thy	Tue May 16 13:01:22 2006 +0200
     5.3 @@ -1,4 +1,7 @@
     5.4 +
     5.5 +(* $Id$ *)
     5.6 +
     5.7  theory Real
     5.8 -imports ContNotDenum RealPow
     5.9 +imports ContNotDenum Ferrante_Rackoff
    5.10  begin
    5.11 -end
    5.12 \ No newline at end of file
    5.13 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Tue May 16 13:01:22 2006 +0200
     6.3 @@ -0,0 +1,129 @@
     6.4 +(*
     6.5 +    ID:         $Id$
     6.6 +    Author:     Amine Chaieb, TU Muenchen
     6.7 +
     6.8 +Ferrante and Rackoff Algorithm.
     6.9 +*)
    6.10 +
    6.11 +structure Ferrante_Rackoff:
    6.12 +sig
    6.13 +  val trace : bool ref
    6.14 +  val ferrack_tac : bool -> int -> tactic
    6.15 +  val setup : theory -> theory
    6.16 +end =
    6.17 +struct
    6.18 +
    6.19 +val trace = ref false;
    6.20 +fun trace_msg s = if !trace then tracing s else ();
    6.21 +
    6.22 +val context_ss = simpset_of (the_context ());
    6.23 +
    6.24 +val nT = HOLogic.natT;
    6.25 +val binarith = map thm
    6.26 +  ["Pls_0_eq", "Min_1_eq",
    6.27 + "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    6.28 +  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    6.29 +  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
    6.30 +  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
    6.31 +  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
    6.32 +  "bin_add_Pls_right", "bin_add_Min_right"];
    6.33 + val intarithrel = 
    6.34 +     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
    6.35 +		"int_le_number_of_eq","int_iszero_number_of_0",
    6.36 +		"int_less_number_of_eq_neg"]) @
    6.37 +     (map (fn s => thm s RS thm "lift_bool") 
    6.38 +	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    6.39 +	   "int_neg_number_of_Min"])@
    6.40 +     (map (fn s => thm s RS thm "nlift_bool") 
    6.41 +	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    6.42 +     
    6.43 +val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    6.44 +			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    6.45 +val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    6.46 +			"mult_nat_number_of", "eq_nat_number_of",
    6.47 +			"less_nat_number_of"]
    6.48 +val powerarith = 
    6.49 +    (map thm ["nat_number_of", "zpower_number_of_even", 
    6.50 +	      "zpower_Pls", "zpower_Min"]) @ 
    6.51 +    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
    6.52 +			   thm "one_eq_Numeral1_nring"] 
    6.53 +  (thm "zpower_number_of_odd"))]
    6.54 +
    6.55 +val comp_arith = binarith @ intarith @ intarithrel @ natarith 
    6.56 +	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    6.57 +
    6.58 +fun prepare_for_linr sg q fm = 
    6.59 +  let
    6.60 +    val ps = Logic.strip_params fm
    6.61 +    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
    6.62 +    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
    6.63 +    fun mk_all ((s, T), (P,n)) =
    6.64 +      if 0 mem loose_bnos P then
    6.65 +        (HOLogic.all_const T $ Abs (s, T, P), n)
    6.66 +      else (incr_boundvars ~1 P, n-1)
    6.67 +    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
    6.68 +      val rhs = hs
    6.69 +(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
    6.70 +    val np = length ps
    6.71 +    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    6.72 +      (foldr HOLogic.mk_imp c rhs, np) ps
    6.73 +    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    6.74 +      (term_frees fm' @ term_vars fm');
    6.75 +    val fm2 = foldr mk_all2 fm' vs
    6.76 +  in (fm2, np + length vs, length rhs) end;
    6.77 +
    6.78 +(*Object quantifier to meta --*)
    6.79 +fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
    6.80 +
    6.81 +(* object implication to meta---*)
    6.82 +fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
    6.83 +
    6.84 +
    6.85 +fun ferrack_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
    6.86 +  let
    6.87 +    val g = List.nth (prems_of st, i - 1)
    6.88 +    val sg = sign_of_thm st
    6.89 +    (* Transform the term*)
    6.90 +    val (t,np,nh) = prepare_for_linr sg q g
    6.91 +    (* Some simpsets for dealing with mod div abs and nat*)
    6.92 +    val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
    6.93 +    (* simp rules for elimination of abs *)
    6.94 +    val simpset3 = HOL_basic_ss addsplits [abs_split]
    6.95 +    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
    6.96 +    (* Theorem for the nat --> int transformation *)
    6.97 +    val pre_thm = Seq.hd (EVERY
    6.98 +      [simp_tac simpset0 1,
    6.99 +       TRY (simp_tac simpset3 1), TRY (simp_tac context_ss 1)]
   6.100 +      (trivial ct))
   6.101 +    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
   6.102 +    (* The result of the quantifier elimination *)
   6.103 +    val (th, tac) = case (prop_of pre_thm) of
   6.104 +        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
   6.105 +    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of sg (Pattern.eta_long [] t1))
   6.106 +    in 
   6.107 +          (trace_msg ("calling procedure with term:\n" ^
   6.108 +             Sign.string_of_term sg t1);
   6.109 +           ((pth RS iffD2) RS pre_thm,
   6.110 +            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
   6.111 +    end
   6.112 +      | _ => (pre_thm, assm_tac i)
   6.113 +  in (rtac (((mp_step nh) o (spec_step np)) th) i 
   6.114 +      THEN tac) st
   6.115 +  end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
   6.116 +
   6.117 +fun ferrack_args meth =
   6.118 + let val parse_flag = 
   6.119 +         Args.$$$ "no_quantify" >> (K (K false));
   6.120 + in
   6.121 +   Method.simple_args 
   6.122 +  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
   6.123 +    curry (Library.foldl op |>) true)
   6.124 +    (fn q => fn _ => meth q 1)
   6.125 +  end;
   6.126 +
   6.127 +val setup =
   6.128 +  Method.add_method ("ferrack",
   6.129 +     ferrack_args (Method.SIMPLE_METHOD oo ferrack_tac),
   6.130 +     "LCF-proof-producing decision procedure for linear real arithmetic");
   6.131 +
   6.132 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Tue May 16 13:01:22 2006 +0200
     7.3 @@ -0,0 +1,818 @@
     7.4 +(*
     7.5 +    ID:         $Id$
     7.6 +    Author:     Amine Chaieb, TU Muenchen
     7.7 +
     7.8 +LCF proof synthesis for Ferrante and Rackoff.
     7.9 +*)
    7.10 +
    7.11 +structure Ferrante_Rackoff_Proof:
    7.12 +sig
    7.13 +  val qelim: cterm -> thm
    7.14 +  exception FAILURE of string
    7.15 +end =
    7.16 +struct
    7.17 +
    7.18 +    (* Some certified types *)
    7.19 +val cbT = ctyp_of (the_context()) HOLogic.boolT;
    7.20 +val rT = Type("RealDef.real",[]);
    7.21 +val crT = ctyp_of (the_context()) (Type("RealDef.real",[]));
    7.22 +    (* Normalization*)
    7.23 +
    7.24 +
    7.25 +	(* Computation of uset *)
    7.26 +fun uset x fm = 
    7.27 +    case fm of
    7.28 +	Const("op &",_)$p$q => (uset x p) union (uset x q)
    7.29 +      | Const("op |",_)$p$q => (uset x p) union (uset x q)
    7.30 +      | Const("Orderings.less",_)$s$t => if s=x then [t] 
    7.31 +			       else if t = x then [s]
    7.32 +			       else []
    7.33 +      | Const("Orderings.less_eq",_)$s$t => if s=x then [t] 
    7.34 +			       else if t = x then [s]
    7.35 +			       else []
    7.36 +      | Const("op =",_)$s$t => if s=x then [t] 
    7.37 +			       else []
    7.38 +      | Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t] 
    7.39 +						 else []
    7.40 +      | _ => [];
    7.41 +val rsT = Type("set",[rT]);
    7.42 +fun holrealset [] = Const("{}",rsT)
    7.43 +  | holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
    7.44 +fun prove_bysimp thy ss t = Goal.prove thy [] [] 
    7.45 +		       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
    7.46 +
    7.47 +fun inusetthms sg x fm = 
    7.48 +    let val U = uset x fm
    7.49 +	val hU = holrealset U
    7.50 +	fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
    7.51 +	val ss = simpset_of sg
    7.52 +	fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
    7.53 +	val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
    7.54 +    in (U,cterm_of sg hU,map proveinU U,uf)
    7.55 +    end;
    7.56 +
    7.57 +	(* Theorems for minus/plusinfinity *)
    7.58 +val [minf_lt,minf_gt,minf_le,minf_ge,minf_eq,minf_neq,minf_fm,minf_conj,minf_disj] = thms"minf";
    7.59 +val [pinf_lt,pinf_gt,pinf_le,pinf_ge,pinf_eq,pinf_neq,pinf_fm,pinf_conj,pinf_disj] = thms"pinf";
    7.60 +    (* Theorems for boundedness from below/above *)
    7.61 +val [nmilbnd_lt,nmilbnd_gt,nmilbnd_le,nmilbnd_ge,nmilbnd_eq,nmilbnd_neq,nmilbnd_fm,nmilbnd_conj,nmilbnd_disj] = thms"nmilbnd";
    7.62 +val [npiubnd_lt,npiubnd_gt,npiubnd_le,npiubnd_ge,npiubnd_eq,npiubnd_neq,npiubnd_fm,npiubnd_conj,npiubnd_disj] = thms"npiubnd";
    7.63 +
    7.64 +    (* Theorems for no changes over smallest intervals in U *)
    7.65 +val lin_dense_lt = thm "lin_dense_lt";
    7.66 +val lin_dense_le = thm "lin_dense_le";
    7.67 +val lin_dense_gt = thm "lin_dense_gt";
    7.68 +val lin_dense_ge = thm "lin_dense_ge";
    7.69 +val lin_dense_eq = thm "lin_dense_eq";
    7.70 +val lin_dense_neq = thm "lin_dense_neq";
    7.71 +val lin_dense_conj = thm "lin_dense_conj";
    7.72 +val lin_dense_disj = thm "lin_dense_disj";
    7.73 +val lin_dense_fm = thm "lin_dense_fm";
    7.74 +val fr_eq = thm "fr_eq";
    7.75 +val fr_simps = thms "fr_simps";
    7.76 +
    7.77 +fun dest5 [] = ([],[],[],[],[])
    7.78 +  | dest5 ((x,y,z,w,v)::xs) = 
    7.79 +    let val (x',y',z',w',v') = dest5 xs 
    7.80 +    in (x::x',y::y',z::z',w::w',v::v') end ;
    7.81 +
    7.82 +fun dest2 [] = ([],[])
    7.83 +  | dest2 ((x,y)::xs) = let val (x',y') = dest2 xs 
    7.84 +			    in (x::x',y::y') end ;
    7.85 +fun myfwd (th1,th2,th3,th4,th5) xs =
    7.86 +    let val (ths1,ths2,ths3,ths4,ths5) = dest5 xs
    7.87 +    in (ths1 MRS th1,ths2 MRS th2,ths3 MRS th3,ths4 MRS th4, ths5 MRS th5)
    7.88 +    end;
    7.89 +
    7.90 +fun myfwd2 (th1,th2) xs =
    7.91 +    let val (ths1,ths2) = dest2 xs
    7.92 +    in (ths1 MRS th1,ths2 MRS th2)
    7.93 +    end;
    7.94 +
    7.95 +fun decomp_mpinf sg x (U,CU,uths) fm = 
    7.96 +    let val cx = cterm_of sg x in
    7.97 +	(case fm of
    7.98 +	    Const("op &",_)$p$q => 
    7.99 +	    ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))	
   7.100 +	  | Const("op |",_)$p$q => 
   7.101 +	    ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
   7.102 +	  | Const("Orderings.less",_)$s$t => 
   7.103 +	    if s= x then 
   7.104 +		let val ct = cterm_of sg t
   7.105 +		    val tinU = nth uths (find_index (fn a => a=t) U)
   7.106 +		    val mith = instantiate' [] [SOME ct] minf_lt
   7.107 +		    val pith = instantiate' [] [SOME ct] pinf_lt
   7.108 +		    val nmilth = tinU RS nmilbnd_lt
   7.109 +		    val npiuth = tinU RS npiubnd_lt
   7.110 +		    val lindth = tinU RS lin_dense_lt
   7.111 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.112 +		end 
   7.113 +	    else if t = x then 
   7.114 +		let val ct = cterm_of sg s
   7.115 +		    val tinU = nth uths (find_index (fn a => a=s) U)
   7.116 +		    val mith = instantiate' [] [SOME ct] minf_gt
   7.117 +		    val pith = instantiate' [] [SOME ct] pinf_gt
   7.118 +		    val nmilth = tinU RS nmilbnd_gt
   7.119 +		    val npiuth = tinU RS npiubnd_gt
   7.120 +		    val lindth = tinU RS lin_dense_gt
   7.121 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.122 +		end 
   7.123 +
   7.124 +	    else
   7.125 +		let val cfm = cterm_of sg fm 
   7.126 +		    val mith = instantiate' [] [SOME cfm] minf_fm
   7.127 +		    val pith = instantiate' [] [SOME cfm] pinf_fm
   7.128 +		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   7.129 +		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   7.130 +		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   7.131 +		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   7.132 +		end
   7.133 +	  | Const("Orderings.less_eq",_)$s$t => 
   7.134 +	    if s= x then 
   7.135 +		let val ct = cterm_of sg t
   7.136 +		    val tinU = nth uths (find_index (fn a => a=t) U)
   7.137 +		    val mith = instantiate' [] [SOME ct] minf_le
   7.138 +		    val pith = instantiate' [] [SOME ct] pinf_le
   7.139 +		    val nmilth = tinU RS nmilbnd_le
   7.140 +		    val npiuth = tinU RS npiubnd_le
   7.141 +		    val lindth = tinU RS lin_dense_le
   7.142 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.143 +		end 
   7.144 +	    else if t = x then 
   7.145 +		let val ct = cterm_of sg s
   7.146 +		    val tinU = nth uths (find_index (fn a => a=s) U)
   7.147 +		    val mith = instantiate' [] [SOME ct] minf_ge
   7.148 +		    val pith = instantiate' [] [SOME ct] pinf_ge
   7.149 +		    val nmilth = tinU RS nmilbnd_ge
   7.150 +		    val npiuth = tinU RS npiubnd_ge
   7.151 +		    val lindth = tinU RS lin_dense_ge
   7.152 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.153 +		end 
   7.154 +
   7.155 +	    else
   7.156 +		let val cfm = cterm_of sg fm 
   7.157 +		    val mith = instantiate' [] [SOME cfm] minf_fm
   7.158 +		    val pith = instantiate' [] [SOME cfm] pinf_fm
   7.159 +		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   7.160 +		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   7.161 +		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   7.162 +		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   7.163 +		end
   7.164 +	  | Const("op =",_)$s$t => 
   7.165 +	    if s= x then 
   7.166 +		let val ct = cterm_of sg t
   7.167 +		    val tinU = nth uths (find_index (fn a => a=t) U)
   7.168 +		    val mith = instantiate' [] [SOME ct] minf_eq
   7.169 +		    val pith = instantiate' [] [SOME ct] pinf_eq
   7.170 +		    val nmilth = tinU RS nmilbnd_eq
   7.171 +		    val npiuth = tinU RS npiubnd_eq
   7.172 +		    val lindth = tinU RS lin_dense_eq
   7.173 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.174 +		end 
   7.175 +	    else
   7.176 +		let val cfm = cterm_of sg fm 
   7.177 +		    val mith = instantiate' [] [SOME cfm] minf_fm
   7.178 +		    val pith = instantiate' [] [SOME cfm] pinf_fm
   7.179 +		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   7.180 +		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   7.181 +		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   7.182 +		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   7.183 +		end
   7.184 +
   7.185 +	  | Const("Not",_)$(Const("op =",_)$s$t) => 
   7.186 +	    if s= x then 
   7.187 +		let val ct = cterm_of sg t
   7.188 +		    val tinU = nth uths (find_index (fn a => a=t) U)
   7.189 +		    val mith = instantiate' [] [SOME ct] minf_neq
   7.190 +		    val pith = instantiate' [] [SOME ct] pinf_neq
   7.191 +		    val nmilth = tinU RS nmilbnd_neq
   7.192 +		    val npiuth = tinU RS npiubnd_neq
   7.193 +		    val lindth = tinU RS lin_dense_neq
   7.194 +		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
   7.195 +		end 
   7.196 +	    else
   7.197 +		let val cfm = cterm_of sg fm 
   7.198 +		    val mith = instantiate' [] [SOME cfm] minf_fm
   7.199 +		    val pith = instantiate' [] [SOME cfm] pinf_fm
   7.200 +		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   7.201 +		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   7.202 +		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   7.203 +		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   7.204 +		end
   7.205 +	  | _ => let val cfm = cterm_of sg fm 
   7.206 +		     val mith = instantiate' [] [SOME cfm] minf_fm
   7.207 +		     val pith = instantiate' [] [SOME cfm] pinf_fm
   7.208 +		     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
   7.209 +		     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
   7.210 +		     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
   7.211 +		 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
   7.212 +		 end)
   7.213 +    end;
   7.214 +
   7.215 +fun ferrack_eq thy p = 
   7.216 +    case p of
   7.217 +	Const("Ex",_)$Abs(x1,T,p1) => 
   7.218 +	let val (xn,fm) = variant_abs(x1,T,p1)
   7.219 +	    val x = Free(xn,T)
   7.220 +	    val (u,cu,uths,uf) = inusetthms thy x fm
   7.221 +	    val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
   7.222 +	    val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
   7.223 +	    val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
   7.224 +	    val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   7.225 +					  (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
   7.226 +	in [frth,qth] MRS trans
   7.227 +	end
   7.228 +      | _ => instantiate' [SOME cbT] [SOME (cterm_of thy p)] refl;
   7.229 +
   7.230 +(* Code for normalization of terms and Formulae *)
   7.231 +    (* For NNF reuse the CooperProof methods*)
   7.232 +    (*FIXME:: This is copied from cooper_proof.ML *)
   7.233 +val FWD = fn th => fn ths => ths MRS th;
   7.234 +
   7.235 +val qe_Not = thm "qe_Not";
   7.236 +val qe_conjI = thm "qe_conjI";
   7.237 +val qe_disjI = thm "qe_disjI";
   7.238 +val qe_impI = thm "qe_impI";
   7.239 +val qe_eqI = thm "qe_eqI";
   7.240 +val qe_exI = thm "qe_exI";
   7.241 +val qe_ALLI = thm "qe_ALLI";
   7.242 +
   7.243 +val nnf_nn = thm "nnf_nn";
   7.244 +val nnf_im = thm "nnf_im";
   7.245 +val nnf_eq = thm "nnf_eq";
   7.246 +val nnf_sdj = thm "nnf_sdj";
   7.247 +val nnf_ncj = thm "nnf_ncj";
   7.248 +val nnf_nim = thm "nnf_nim";
   7.249 +val nnf_neq = thm "nnf_neq";
   7.250 +val nnf_ndj = thm "nnf_ndj";
   7.251 +
   7.252 +fun decomp_cnnf lfnp P = 
   7.253 +    case P of 
   7.254 +	Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
   7.255 +      | Const ("op |",_) $ p $q => ([p,q] , FWD qe_disjI)
   7.256 +      | Const ("Not",_) $ (Const("Not",_) $ p) => ([p], FWD nnf_nn)
   7.257 +      | Const("Not",_) $ (Const(opn,T) $ p $ q) => 
   7.258 +	if opn = "op |" 
   7.259 +	then 
   7.260 +	    (case (p,q) of 
   7.261 +		 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
   7.262 +		 if r1 = CooperDec.negate r 
   7.263 +		 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
   7.264 +			fn [th1_1,th1_2,th2_1,th2_2] => 
   7.265 +			   [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
   7.266 +		       
   7.267 +		 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
   7.268 +               | (_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj))
   7.269 +	else (
   7.270 +              case (opn,T) of 
   7.271 +		  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
   7.272 +		| ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
   7.273 +		| ("op =",Type ("fun",[Type ("bool", []),_])) => 
   7.274 +		  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
   7.275 +		   FWD nnf_neq)
   7.276 +		| (_,_) => ([], fn [] => lfnp P))
   7.277 +      | (Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], FWD nnf_im)
   7.278 +      | (Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
   7.279 +	([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
   7.280 +      | _ => ([], fn [] => lfnp P);
   7.281 +
   7.282 +fun nnfp afnp vs p = 
   7.283 +    let val th = divide_and_conquer (decomp_cnnf (afnp vs)) p
   7.284 +	val Pth = (Simplifier.rewrite 
   7.285 +		       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
   7.286 +		       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
   7.287 +		      RS meta_eq_to_obj_eq
   7.288 +    in [th,Pth] MRS trans
   7.289 +    end;
   7.290 +
   7.291 +
   7.292 +    (* Normalization of arithmetical expressions *)
   7.293 +val rzero = Const("0",rT);
   7.294 +val rone = Const("1",rT);
   7.295 +fun mk_real i = 
   7.296 +    case i of 
   7.297 +	0 => rzero
   7.298 +      | 1 => rone
   7.299 +      | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
   7.300 +
   7.301 +fun dest_real (Const("0",_)) = 0
   7.302 +  | dest_real (Const("1",_)) = 1
   7.303 +  | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
   7.304 +
   7.305 +	(* Normal form for terms is: 
   7.306 +	 (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
   7.307 +	(* functions to prove trivial properties about numbers *)
   7.308 +fun proveq thy n m = prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(mk_real n,mk_real m));
   7.309 +fun provenz thy n = 
   7.310 +    prove_bysimp thy (simpset_of thy) (HOLogic.Not$(HOLogic.mk_eq(mk_real n,rzero)));
   7.311 +
   7.312 +fun proveprod thy m n = 
   7.313 +    prove_bysimp thy (simpset_of thy) 
   7.314 +		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
   7.315 +fun proveadd thy m n = 
   7.316 +    prove_bysimp thy (simpset_of thy) 
   7.317 +		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
   7.318 +fun provediv thy m n = 
   7.319 +    let val g = gcd (m,n) 
   7.320 +	val m' = m div g
   7.321 +	val n'= n div g
   7.322 +    in
   7.323 +	(prove_bysimp thy (simpset_of thy) 
   7.324 +		     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
   7.325 +				    HOLogic.mk_binop "HOL.divide" 
   7.326 +						     (mk_real m',mk_real n'))),m')
   7.327 +    end;
   7.328 +		 (* Multiplication of a normal term by a constant *)
   7.329 +val ncmul_congh = thm "ncmul_congh";
   7.330 +val ncmul_cong = thm "ncmul_cong";
   7.331 +fun decomp_ncmulh thy c t = 
   7.332 +    if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else 
   7.333 +    case t of 
   7.334 +	Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
   7.335 +	([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
   7.336 +			       ((proveprod thy c (dest_real c')) RS ncmul_congh)))
   7.337 +      | _ => ([],fn _ => proveprod thy c (dest_real t));
   7.338 +
   7.339 +fun prove_ncmulh thy c = divide_and_conquer (decomp_ncmulh thy c);
   7.340 +
   7.341 +    (* prove_ncmul thy n t n = a theorem : "c*(t/n) = (t'/n')*)
   7.342 +fun prove_ncmul thy c (t,m) = 
   7.343 +    let val (eq1,c') = provediv thy c m
   7.344 +	val tt' = prove_ncmulh thy c' t
   7.345 +    in [eq1,tt'] MRS ncmul_cong
   7.346 +    end;
   7.347 +
   7.348 +    (* prove_nneg returns "-(t/n) = t'/n'" ; normally t'=t and n' = -n*)
   7.349 +val nneg_cong = thm "nneg_cong";
   7.350 +fun prove_nneg thy (t,m) = (prove_ncmul thy ~1 (t, m)) RS nneg_cong;
   7.351 +
   7.352 +(* Addition of 2 expressions in normal form*)
   7.353 +val naddh_cong_same = thm "naddh_cong_same";
   7.354 +val naddh_cong_same0 = thm "naddh_cong_same0";
   7.355 +val naddh_cong_ts = thm "naddh_cong_ts";
   7.356 +val naddh_cong_st = thm "naddh_cong_st";
   7.357 +
   7.358 +fun earlier [] x y = false 
   7.359 +  | earlier (h::t) x y =
   7.360 +    if h = y then false 
   7.361 +    else if h = x then true 
   7.362 +    else earlier t x y ; 
   7.363 +
   7.364 +fun decomp_naddh thy vs (t,s) = 
   7.365 +    case (t,s) of 
   7.366 +	(Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
   7.367 +	 Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
   7.368 +	if tv = sv then 
   7.369 +	    let val ntc = dest_real tc
   7.370 +		val nsc = dest_real sc
   7.371 +		val addth = proveadd thy ntc nsc
   7.372 +	    in if ntc + nsc = 0 
   7.373 +	       then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   7.374 +						  (addth RS naddh_cong_same0)))
   7.375 +	       else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
   7.376 +						  (addth RS naddh_cong_same)))
   7.377 +	    end
   7.378 +	else if earlier vs tv sv 
   7.379 +	then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   7.380 +	else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   7.381 +      | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) => 
   7.382 +	([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
   7.383 +      | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) => 
   7.384 +	([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
   7.385 +      | (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
   7.386 +
   7.387 +    (* prove_naddh returns "t + s = t'*) 
   7.388 +fun prove_naddh thy vs = divide_and_conquer (decomp_naddh thy vs);
   7.389 +
   7.390 +val nadd_cong_same = thm "nadd_cong_same";
   7.391 +val nadd_cong = thm "nadd_cong";
   7.392 +val plus_cong = thm "plus_cong";
   7.393 +    (* prove_nadd resturns: "t/m + s/n = t'/m'"*)
   7.394 +fun prove_nadd thy vs (t,m) (s,n) = 
   7.395 +    if n=m then 
   7.396 +	let val nm = proveq thy n m
   7.397 +	    val ts = prove_naddh thy vs (t,s)
   7.398 +	in [nm,ts] MRS nadd_cong_same
   7.399 +	end
   7.400 +    else let val l = lcm (m,n)
   7.401 +	     val m' = l div m
   7.402 +	     val n' = l div n
   7.403 +	     val mml = proveprod thy m' m
   7.404 +	     val nnl = proveprod thy n' n
   7.405 +	     val mnz = provenz thy m
   7.406 +	     val nnz = provenz thy n
   7.407 +	     val lnz = provenz thy l
   7.408 +	     val mt = prove_ncmulh thy m' t
   7.409 +	     val ns = prove_ncmulh thy n' s
   7.410 +	     val _$(_$_$t') = prop_of mt
   7.411 +	     val _$(_$_$s') = prop_of ns
   7.412 +	 in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
   7.413 +		MRS nadd_cong
   7.414 +	 end;
   7.415 +
   7.416 +    (* prove_nsub returns: "t/m - s/n = t'/m'"*)
   7.417 +val nsub_cong = thm "nsub_cong";
   7.418 +fun prove_nsub thy vs (t,m) (s,n) = 
   7.419 +    let val nsm = prove_nneg thy (s,n)
   7.420 +	val _$(_$_$(_$s'$n')) = prop_of nsm
   7.421 +	val ts = prove_nadd thy vs (t,m) (s',dest_real n')
   7.422 +    in [nsm,ts] MRS nsub_cong
   7.423 +    end;
   7.424 +
   7.425 +val ndivide_cong = thm "ndivide_cong";
   7.426 +fun prove_ndivide thy (t,m) n = instantiate' [] [SOME(cterm_of thy t)] 
   7.427 +					     ((proveprod thy m n) RS ndivide_cong);
   7.428 +
   7.429 +exception FAILURE of string;
   7.430 +
   7.431 +val divide_cong = thm"divide_cong";
   7.432 +val diff_cong = thm"diff_cong";
   7.433 +val uminus_cong = thm"uminus_cong";
   7.434 +val mult_cong = thm"mult_cong";
   7.435 +val mult_cong2 = thm"mult_cong2";
   7.436 +val normalizeh_var = thm "normalizeh_var";
   7.437 +val nrefl = thm "nrefl";
   7.438 +
   7.439 +fun decomp_normalizeh thy vs t =
   7.440 +    case t of
   7.441 +	Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
   7.442 +      | Const("HOL.uminus",_)$a => 
   7.443 +	([a], 
   7.444 +	 fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
   7.445 +			 in [tha,prove_nneg thy (a',dest_real n')] 
   7.446 +				MRS uminus_cong
   7.447 +			 end )
   7.448 +      | Const("HOL.plus",_)$a$b => 
   7.449 +	([a,b], 
   7.450 +	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   7.451 +			     val _$(_$_$(_$b'$m')) = prop_of thb
   7.452 +			 in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
   7.453 +				MRS plus_cong
   7.454 +			 end )
   7.455 +      | Const("HOL.minus",_)$a$b => 
   7.456 +	([a,b], 
   7.457 +	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
   7.458 +			     val _$(_$_$(_$b'$m')) = prop_of thb
   7.459 +			 in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
   7.460 +				MRS diff_cong
   7.461 +			 end )
   7.462 +      | Const("HOL.times",_)$a$b => 
   7.463 +	if can dest_real a 
   7.464 +	then ([b], fn [thb] => 
   7.465 +		      let val _$(_$_$(_$b'$m')) = prop_of thb
   7.466 +		      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
   7.467 +		      end )
   7.468 +	else if can dest_real b
   7.469 +	then ([a], fn [tha] => 
   7.470 +		      let val _$(_$_$(_$a'$m')) = prop_of tha
   7.471 +		      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
   7.472 +		      end )
   7.473 +	else raise FAILURE "decomp_normalizeh: non linear term"
   7.474 +      | Const("HOL.divide",_)$a$b => 
   7.475 +	if can dest_real b
   7.476 +	then ([a], fn [tha] => 
   7.477 +		      let val _$(_$_$(_$a'$m')) = prop_of tha
   7.478 +		      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
   7.479 +		      end )
   7.480 +	else raise FAILURE "decomp_normalizeh: non linear term"
   7.481 +      | _ => ([], fn _ => instantiate' [] [SOME (cterm_of thy t)] nrefl);
   7.482 +fun prove_normalizeh thy vs = divide_and_conquer (decomp_normalizeh thy vs);
   7.483 +fun dest_xth vs th = 
   7.484 +    let val _$(_$_$(_$t$n)) = prop_of th
   7.485 +    in (case t of 
   7.486 +	    Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
   7.487 +	    if vs = [] then (0,t,dest_real n)
   7.488 +	    else if hd vs = y then (dest_real c, r,dest_real n)
   7.489 +	    else (0,t,dest_real n)
   7.490 +	  | _ => (0,t,dest_real n))
   7.491 +    end;
   7.492 +
   7.493 +fun prove_strictsign thy n = 
   7.494 +    prove_bysimp thy (simpset_of thy) 
   7.495 +		 (HOLogic.mk_binrel "Orderings.less" 
   7.496 +				    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
   7.497 +fun prove_fracsign thy (m,n) = 
   7.498 +    let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
   7.499 +    in prove_bysimp thy (simpset_of thy) 
   7.500 +		 (HOLogic.mk_binrel "Orderings.less" 
   7.501 +				    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
   7.502 +    end; 
   7.503 +
   7.504 +fun holbool_of true = HOLogic.true_const
   7.505 +  | holbool_of false = HOLogic.false_const;
   7.506 +
   7.507 +fun prove_fracsign_eq thy s (m,n) = 
   7.508 +    let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
   7.509 +    in 
   7.510 +    prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
   7.511 +		 (HOLogic.mk_binrel s 
   7.512 +				    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
   7.513 +				    holbool_of (f s (m*n,0))))
   7.514 +    end;
   7.515 +
   7.516 +fun proveq_eq thy n m = 
   7.517 +    prove_bysimp thy (simpset_of thy) 
   7.518 +		 (HOLogic.mk_eq 
   7.519 +		      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
   7.520 +
   7.521 +val sum_of_same_denoms = thm "sum_of_same_denoms";
   7.522 +val sum_of_opposite_denoms = thm "sum_of_opposite_denoms";
   7.523 +val trivial_sum_of_opposites = thm "trivial_sum_of_opposites";
   7.524 +val normalize_ltground_cong = thm "normalize_ltground_cong";
   7.525 +val normalize_ltnoxpos_cong = thm "normalize_ltnoxpos_cong";
   7.526 +val normalize_ltnoxneg_cong = thm "normalize_ltnoxneg_cong";
   7.527 +val normalize_ltxpos_cong = thm "normalize_ltxpos_cong";
   7.528 +val normalize_ltxneg_cong = thm "normalize_ltxneg_cong";
   7.529 +
   7.530 +val normalize_leground_cong = thm "normalize_leground_cong";
   7.531 +val normalize_lenoxpos_cong = thm "normalize_lenoxpos_cong";
   7.532 +val normalize_lenoxneg_cong = thm "normalize_lenoxneg_cong";
   7.533 +val normalize_lexpos_cong = thm "normalize_lexpos_cong";
   7.534 +val normalize_lexneg_cong = thm "normalize_lexneg_cong";
   7.535 +
   7.536 +val normalize_eqground_cong = thm "normalize_eqground_cong";
   7.537 +val normalize_eqnox_cong = thm "normalize_eqnox_cong";
   7.538 +val normalize_eqxpos_cong = thm "normalize_eqxpos_cong";
   7.539 +val normalize_eqxneg_cong = thm "normalize_eqxneg_cong";
   7.540 +
   7.541 +val normalize_not_lt = thm "normalize_not_lt";
   7.542 +val normalize_not_le = thm "normalize_not_le";
   7.543 +val normalize_not_eq = thm "normalize_not_eq";
   7.544 +
   7.545 +fun prove_normalize thy vs at = 
   7.546 +    case at of 
   7.547 +	Const("Orderings.less",_)$s$t => 
   7.548 +	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   7.549 +	    val (cx,r,n) = dest_xth vs smtth
   7.550 +	in if cx = 0 then if can dest_real r 
   7.551 +			  then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
   7.552 +				   MRS normalize_ltground_cong
   7.553 +			  else [smtth, prove_strictsign thy n] 
   7.554 +				   MRS (if n > 0 then normalize_ltnoxpos_cong 
   7.555 +					else normalize_ltnoxneg_cong)
   7.556 +	   else let val srn = prove_fracsign thy (n,cx)
   7.557 +		    val rr' = if cx < 0 
   7.558 +			      then instantiate' [] [SOME (cterm_of thy r)]
   7.559 +						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   7.560 +			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   7.561 +						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
   7.562 +							   RS sum_of_same_denoms)
   7.563 +		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
   7.564 +					else normalize_ltxpos_cong)
   7.565 +		end
   7.566 +	end
   7.567 +      | Const("Orderings.less_eq",_)$s$t => 
   7.568 +	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   7.569 +	    val (cx,r,n) = dest_xth vs smtth
   7.570 +	in if cx = 0 then if can dest_real r 
   7.571 +			  then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
   7.572 +				   MRS normalize_leground_cong
   7.573 +			  else [smtth, prove_strictsign thy n] 
   7.574 +				   MRS (if n > 0 then normalize_lenoxpos_cong 
   7.575 +					else normalize_lenoxneg_cong)
   7.576 +	   else let val srn = prove_fracsign thy (n,cx)
   7.577 +		    val rr' = if cx < 0 
   7.578 +			      then instantiate' [] [SOME (cterm_of thy r)]
   7.579 +						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
   7.580 +			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
   7.581 +						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
   7.582 +							   RS sum_of_same_denoms)
   7.583 +		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
   7.584 +					else normalize_lexpos_cong)
   7.585 +		end
   7.586 +	end
   7.587 +      | Const("op =",_)$s$t => 
   7.588 +	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
   7.589 +	    val (cx,r,n) = dest_xth vs smtth
   7.590 +	in if cx = 0 then if can dest_real r 
   7.591 +			  then [smtth, provenz thy n, 
   7.592 +				proveq_eq thy (dest_real r) 0]
   7.593 +				   MRS normalize_eqground_cong
   7.594 +			  else [smtth, provenz thy n] 
   7.595 +				   MRS normalize_eqnox_cong
   7.596 +	   else let val scx = prove_strictsign thy cx
   7.597 +		    val nnz = provenz thy n
   7.598 +		    val rr' = if cx < 0 
   7.599 +			      then proveadd thy cx (~cx)
   7.600 +			      else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
   7.601 +				       RS trivial_sum_of_opposites
   7.602 +		in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
   7.603 +					else normalize_eqxpos_cong)
   7.604 +		end
   7.605 +	end
   7.606 +      | Const("Not",_)$(Const("Orderings.less",T)$s$t) => 
   7.607 +	(prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
   7.608 +      | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) => 
   7.609 +	(prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
   7.610 +      | (nt as Const("Not",_))$(Const("op =",T)$s$t) => 
   7.611 +	(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
   7.612 +      | _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
   7.613 +
   7.614 +     (* Generic quantifier elimination *)
   7.615 +
   7.616 +
   7.617 +val qe_ex_conj = thm "qe_ex_conj";
   7.618 +val qe_ex_nconj = thm "qe_ex_nconj";
   7.619 +val qe_ALL = thm "qe_ALL";
   7.620 +val ex_eq_cong = thm "ex_eq_cong";
   7.621 +
   7.622 +fun decomp_genqelim thy afnp nfnp qfnp (P,vs) = 
   7.623 +    case P of
   7.624 +	(Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
   7.625 +      | (Const("op |",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_disjI)
   7.626 +      | (Const("op -->",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_impI)
   7.627 +      | (Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => 
   7.628 +	([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   7.629 +      | (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
   7.630 +      | (Const("Ex",_)$Abs(xn,xT,p)) => 
   7.631 +	let val (xn1,p1) = variant_abs(xn,xT,p)
   7.632 +	    val x= Free(xn1,xT)
   7.633 +	in ([(p1,x::vs)],
   7.634 +            fn [th1_1] => 
   7.635 +               let val th2 = [th1_1,nfnp (x::vs) (snd (CooperProof.qe_get_terms th1_1))] MRS trans
   7.636 +		   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
   7.637 +		   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
   7.638 +               in [eth1,th3] MRS trans
   7.639 +               end )
   7.640 +	end
   7.641 +      | (Const("All",_)$Abs(xn,xT,p)) => 
   7.642 +	([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
   7.643 +      | _ => ([], fn [] => afnp vs P);
   7.644 +
   7.645 +val fr_prepqelim = thms "fr_prepqelim";
   7.646 +val prepare_qelim_ss = HOL_basic_ss 
   7.647 +			   addsimps simp_thms 
   7.648 +			   addsimps (List.take(ex_simps,4))
   7.649 +			   addsimps fr_prepqelim
   7.650 +			   addsimps [not_all,ex_disj_distrib];
   7.651 +
   7.652 +fun prove_genqelim thy afnp nfnp qfnp P = 
   7.653 +    let val thP = (Simplifier.rewrite prepare_qelim_ss P) RS meta_eq_to_obj_eq
   7.654 +	val _$(_$_$P') = prop_of thP
   7.655 +	val vs = term_frees P'
   7.656 +	val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
   7.657 +	val _$(_$_$p'') = prop_of qeth
   7.658 +	val thp' = nfnp vs p''
   7.659 +    in [[thP, qeth] MRS trans, thp'] MRS trans
   7.660 +    end;
   7.661 +
   7.662 +fun qelim P =
   7.663 +  let val {thy, ...} = Thm.rep_cterm P
   7.664 +  in prove_genqelim thy (prove_normalize thy) (nnfp (prove_normalize thy)) (ferrack_eq thy) P end;
   7.665 +
   7.666 +
   7.667 +    (* Just for testing!! *)
   7.668 +(*
   7.669 +val thy = the_context();
   7.670 +fun parseb s = term_of (read_cterm thy (s,HOLogic.boolT));
   7.671 +fun parser s = term_of (read_cterm thy (s,rT));
   7.672 +val fm = parseb "(x::real) < y + t & (y - 5 < x | 34 < y + t) & (x = s + 3*y) | (x ~= y - s)";
   7.673 +
   7.674 +provediv thy 4 2;
   7.675 +provediv thy ~4 2;
   7.676 +provediv thy 4 ~2;
   7.677 +provediv thy 44 32;
   7.678 +provediv thy ~34 20000;
   7.679 +provediv thy ~4000000 ~27676;
   7.680 +
   7.681 +val vs = [Free("x",rT),Free("y",rT),Free("z",rT)] ;
   7.682 +prove_nsub thy vs
   7.683 +		    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
   7.684 +
   7.685 +prove_ndivide thy (parser "4*(x::real) + (3*y + 5)" ,5) 4;
   7.686 +prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   7.687 +		    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
   7.688 +prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   7.689 +		    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
   7.690 +prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   7.691 +		    (parser "- x");
   7.692 +prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
   7.693 +		    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
   7.694 +
   7.695 +
   7.696 +
   7.697 +
   7.698 +
   7.699 +
   7.700 +fun test xn s = ferrack_eq thy (parseb ("EX (" ^ xn ^ "::real)." ^ s));
   7.701 +test "x" "(x::real) < y + t & (y - 5 < x | 34 < y + t) & (x = s + 3*y) | (x ~= y - s) & (x::real) <= y + t & (y - 5 <= x)";
   7.702 +test "x" "(x::real) < y + t & y - 5 < x & (x ~= y - s)";
   7.703 +test "x" "(x::real) < y + t";
   7.704 +test "x" "(x::real) > y + t";
   7.705 +test "x" "(x::real) = y + t";
   7.706 +test "x" "(x::real) ~= y + t";
   7.707 +test "x" "34 < y + (t::real)";
   7.708 +test "x" "(x::real) ~= y + t & 34 < y + (t::real)";
   7.709 +test "x" "(x::real) ~= y + t & (x::real) < y + t";
   7.710 +
   7.711 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + y"); 
   7.712 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= 3*x + y"); 
   7.713 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y"); 
   7.714 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 "); 
   7.715 +
   7.716 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + y"); 
   7.717 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < 3*x + y"); 
   7.718 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < (-1)*x + y"); 
   7.719 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 "); 
   7.720 +
   7.721 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + y"); 
   7.722 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = 3*x + y"); 
   7.723 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = (-1)*x + y"); 
   7.724 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + 3 + 4* (y - 15*z) / 3 "); 
   7.725 +
   7.726 +prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + y)"); 
   7.727 +prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= 3*x + y)"); 
   7.728 +prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y)"); 
   7.729 +prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 )"); 
   7.730 +
   7.731 +prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + y)"); 
   7.732 +prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < 3*x + y)"); 
   7.733 +prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < (-1)*x + y)"); 
   7.734 +prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 )"); 
   7.735 +
   7.736 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + y"); 
   7.737 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= 3*x + y"); 
   7.738 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= (-1)*x + y"); 
   7.739 +prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 "); 
   7.740 +
   7.741 +
   7.742 +nnfp (prove_normalize thy) vs
   7.743 +     (parseb "~((x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 | (~ (~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 ) & (x::real) + 4* (y - 15*z) / 3 <= x + y)))");
   7.744 +nnfp (prove_normalize thy) vs
   7.745 +     (parseb "~ ~((x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 | (~ (~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 ) & (x::real) + 4* (y - 15*z) / 3 <= x + y)))");
   7.746 +
   7.747 +fun frtest s = frqelim thy (read_cterm thy (s,HOLogic.boolT));
   7.748 +frtest "~ (ALL (x::real) y. x < y --> 10*x < 11*y)";
   7.749 +frtest "ALL (x::real) y. x < y --> (10*(x + 5*y + -1) < 60*y)";
   7.750 +frtest "EX (x::real) y. x ~= y --> x < y";
   7.751 +frtest "EX (x::real) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y";
   7.752 +frtest "ALL (x::real) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y";
   7.753 +*)
   7.754 +  (* 1 Alternations *)
   7.755 +(*
   7.756 +frtest "ALL (x::real). (EX (y::real). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)";
   7.757 +frtest "ALL (x::real) < 0. (EX (y::real) > 0. 7*x + y > 0 & x - y <= 9)";
   7.758 +frtest "EX (x::real). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)";
   7.759 +frtest "EX (x::real). 0 < x & x < 1 & (ALL y. (1 < y & y < 2) --> (1 < 2*(y - x) & 2*(y - x) <3))";
   7.760 +frtest "ALL (x::real). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)";
   7.761 +*)
   7.762 +    (* Formulae with 3 quantifiers *)
   7.763 +  (* 0 Alternations *)
   7.764 +(*
   7.765 +frtest "ALL (x::real) y z. x + y < z --> y >= z --> x < 0";
   7.766 +frtest "EX (x::real) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0";
   7.767 +frtest "ALL (x::real) y z. abs (x + y) <= z --> (abs z = z)";
   7.768 +frtest "EX (x::real) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0";
   7.769 +frtest "ALL (x::real) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))";
   7.770 +*)
   7.771 +  (* 1 Alternations *)
   7.772 +(*
   7.773 +frtest "ALL (x::real) y. x < y --> (EX z>0. x+z = y)";
   7.774 +frtest "ALL (x::real) y. (EX z>0. abs (x - y) <= z )";
   7.775 +frtest "EX (x::real) y. (ALL z>0. (z < x --> z <= 5) & (z > y --> z >= x))";
   7.776 +frtest "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))";
   7.777 +frtest "EX (x::real) y. (ALL z>0. abs (3*x - 7*y) >= 5 & abs (3*x+7*y) <= 2*z + 1)";
   7.778 +*)
   7.779 +  (* 2 Alternations *)
   7.780 +(*
   7.781 +frtest "EX (x::real)>0. (ALL y >0. (EX z>7. 5*x - 3*y <= 7*z))";
   7.782 +frtest "EX (x::real). abs x < 4 & (ALL y > 0. (EX z. 5*x - 3*y <= 7*z))";
   7.783 +frtest "ALL (x::real). (EX y > x. (ALL z < y. x+z < 2*y))" ;
   7.784 +frtest "ALL (x::real). (EX y<(3*x - 1). (ALL z >= (3*x - 1). x - y + z > x ))" ;
   7.785 +frtest "EX (x::real). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))";
   7.786 +*)
   7.787 +    (* Formulae with 4 quantifiers *)
   7.788 +    (* 0 Alternations *)
   7.789 +(*
   7.790 +frtest "ALL (x::real) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y";
   7.791 +frtest "ALL (x::real) y. ALL z >x. ALL w > y. abs (z-x) + abs (y-w + x) <= z - x + w-y+abs x";
   7.792 +frtest "EX (x::real) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89";
   7.793 +frtest "EX (x::real) y z w. abs (5*x + 3*z - 17*w) + 7* abs (y - 8*x + z) <= max y (7*z - x + w)";
   7.794 +frtest "EX (x::real) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)";
   7.795 +*)
   7.796 +    (* 1 Alternations *)
   7.797 +(*
   7.798 +frtest "ALL (x::real) y z. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z)";
   7.799 +frtest "ALL (x::real). (EX y z w. x< y & x < z & x> w & 3*x < w + y)";
   7.800 +frtest "ALL (x::real) y. (EX z w. abs (x-y) = abs (z-w) & z < x & w ~= y)";
   7.801 +frtest "ALL (x::real). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))";
   7.802 +frtest "EX (x::real) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)";
   7.803 +*)
   7.804 +    (* 2 Alternations *)
   7.805 +(*
   7.806 +frtest "EX z. (ALL (x::real) y. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z))";
   7.807 +frtest "EX z. (ALL (x::real) < z. (EX y w. x< y & x < z & x> w & 3*x < w + y))";
   7.808 +frtest "ALL (x::real) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))";
   7.809 +frtest "EX y. (ALL (x::real). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))";
   7.810 +frtest "EX (x::real) z. (ALL w >= abs (x+z). (EX y. w >= abs x + abs y + abs z))";
   7.811 +*)
   7.812 +    (* 3 Alternations *)
   7.813 +(*
   7.814 +frtest "EX (x::real). (ALL y < x. (EX z > (x+y). (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))";
   7.815 +frtest "EX (x::real). (ALL y < 3*x. (EX z > max x y. 
   7.816 +  (ALL w . abs w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))";
   7.817 +frtest "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))";
   7.818 +frtest "ALL (x::real). (EX y. (ALL z>19. abs (y) <= abs (x + z) & (EX w. abs (x + z) < w - y)))";
   7.819 +frtest "ALL (x::real). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))";
   7.820 +*)
   7.821 +end