author wenzelm Tue May 16 13:01:22 2006 +0200 (2006-05-16) changeset 19640 40ec89317425 parent 19639 d9079a9ccbfb child 19641 f1de44e61ec1
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
 src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy file | annotate | diff | revisions src/HOL/Complex/ex/ROOT.ML file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Real/Ferrante_Rackoff.thy file | annotate | diff | revisions src/HOL/Real/Real.thy file | annotate | diff | revisions src/HOL/Real/ferrante_rackoff.ML file | annotate | diff | revisions src/HOL/Real/ferrante_rackoff_proof.ML file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.372 +	    in if ntc + nsc = 0
7.373 +	       then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)]
7.375 +	       else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)]
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.389 +
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.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.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
```