added Ferrante and Rackoff Algorithm -- by Amine Chaieb;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy	Tue May 16 13:01:22 2006 +0200
@@ -0,0 +1,169 @@
+(*
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+
+Examples for Ferrante and Rackoff Algorithm.
+*)
+
+theory Ferrante_Rackoff_Ex
+imports Complex_Main
+begin
+
+lemma "~ (ALL (x::real) y. x < y --> 10*x < 11*y)"
+apply ferrack
+done
+
+lemma "ALL (x::real) y. x < y --> (10*(x + 5*y + -1) < 60*y)"
+apply ferrack
+done
+
+lemma "EX (x::real) y. x ~= y --> x < y"
+  apply ferrack
+  done
+
+lemma "EX (x::real) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y"
+  apply ferrack
+  done
+lemma "ALL (x::real) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y"
+  apply ferrack
+  done
+
+  (* 1 Alternations *)
+lemma "ALL (x::real). (EX (y::real). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)"
+  by ferrack
+lemma "ALL (x::real) < 0. (EX (y::real) > 0. 7*x + y > 0 & x - y <= 9)"
+  by ferrack
+lemma "EX (x::real). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)"
+  apply ferrack
+  done
+lemma "EX (x::real). (ALL y. y < 2 -->  2*(y - x) \<le> 0 )"
+  apply ferrack
+  done
+lemma "ALL (x::real). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)"
+  apply ferrack
+  done
+    (* Formulae with 3 quantifiers *)
+  (* 0 Alternations *)
+lemma "ALL (x::real) y z. x + y < z --> y >= z --> x < 0"
+apply ferrack
+done
+lemma "EX (x::real) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0"
+apply ferrack
+done
+lemma "ALL (x::real) y z. abs (x + y) <= z --> (abs z = z)"
+apply ferrack
+done
+
+lemma "EX (x::real) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0"
+apply ferrack
+done
+
+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))"
+apply ferrack
+done
+  (* 1 Alternations *)
+lemma "ALL (x::real) y. x < y --> (EX z>0. x+z = y)"
+  by ferrack
+lemma "ALL (x::real) y. (EX z>0. abs (x - y) <= z )"
+  by ferrack
+
+lemma "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+  apply ferrack
+  done
+
+lemma "EX (x::real) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)"
+  apply ferrack
+  done
+lemma "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))"
+  apply ferrack
+  done
+  (* 2 Alternations *)
+lemma "EX (x::real)>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))"
+  apply ferrack
+  done
+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))"
+  apply ferrack
+  done
+
+lemma "ALL (x::real). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" 
+  apply ferrack
+  done
+
+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) ))" 
+  apply ferrack
+  done
+
+lemma "EX (x::real). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))"
+  apply ferrack
+  done
+
+    (* Formulae with 4 quantifiers *)
+    (* 0 Alternations *)
+lemma "ALL (x::real) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y"
+  apply ferrack
+  done
+lemma "ALL (x::real) y. ALL z >x. ALL w > y. abs (z-x) + abs (y-w + x) <= z - x + w-y+abs x"
+  apply ferrack
+  done
+lemma "EX (x::real) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89"
+  apply ferrack
+  done
+
+lemma "EX (x::real) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)"
+  apply ferrack
+  done
+
+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)"
+  apply ferrack
+  done
+    (* 1 Alternations *)
+lemma "ALL (x::real) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)"
+  apply ferrack
+  done
+lemma "~(ALL (x::real). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))"
+  apply ferrack
+  done
+lemma "ALL (x::real) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)"
+  apply ferrack
+  done
+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))"
+  apply ferrack
+  done
+lemma "EX (x::real) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)"
+  apply ferrack
+  done
+    (* 2 Alternations *)
+lemma "EX z. (ALL (x::real) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))"
+  apply ferrack
+  done
+lemma "EX z. (ALL (x::real) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))"
+  apply ferrack
+  done
+lemma "ALL (x::real) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))"
+  apply ferrack
+  done
+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)))"
+  apply ferrack
+  done
+lemma "EX (x::real) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))"
+  apply ferrack
+  done
+    (* 3 Alternations *)
+lemma "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)))"
+  apply ferrack
+  done
+lemma "EX (x::real). (ALL y. (EX z > y. 
+  (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))"
+  apply ferrack
+  done
+lemma "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))"
+  apply ferrack
+  done
+lemma "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))"
+  apply ferrack
+  done
+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)))"
+  apply ferrack
+  done
+end

--- a/src/HOL/Complex/ex/ROOT.ML	Tue May 16 09:19:12 2006 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Tue May 16 13:01:22 2006 +0200
@@ -20,3 +20,5 @@
 
 no_document use_thy "NatPair";
 use_thy "DenumRat";
+
+use_thy "Ferrante_Rackoff_Ex";

--- a/src/HOL/IsaMakefile	Tue May 16 09:19:12 2006 +0200
+++ b/src/HOL/IsaMakefile	Tue May 16 13:01:22 2006 +0200
@@ -156,11 +156,11 @@
 HOL-Complex: HOL $(OUT)/HOL-Complex
 
 $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML Library/Zorn.thy			\
-  Real/Lubs.thy Real/rat_arith.ML						\
-  Real/Rational.thy Real/PReal.thy Real/RComplete.thy				\
-  Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy		\
-  Real/RealPow.thy Real/document/root.tex					\
-  Real/Float.thy Real/Float.ML                                                  \
+  Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/Float.ML			\
+  Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy		\
+  Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy			\
+  Real/RealPow.thy Real/document/root.tex Real/ferrante_rackoff_proof.ML	\
+  Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML			\
   Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
   Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
@@ -185,7 +185,7 @@
 
 $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
-  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
+  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy Complex/ex/Ferrante_Rackoff_Ex.thy \
   Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/Ferrante_Rackoff.thy	Tue May 16 13:01:22 2006 +0200
@@ -0,0 +1,487 @@
+(*
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+
+Ferrante and Rackoff Algorithm: LCF-proof-synthesis version.
+*)
+
+theory Ferrante_Rackoff
+imports RealPow
+uses ("ferrante_rackoff_proof.ML") ("ferrante_rackoff.ML")
+begin
+
+  (* Synthesis of \<exists>z. \<forall>x<z. P x = P1 *)
+lemma minf: 
+  "\<exists>(z::real) . \<forall>x<z. x < t = True "  "\<exists>(z::real) . \<forall>x<z. x > t = False "
+  "\<exists>(z::real) . \<forall>x<z. x \<le> t = True "  "\<exists>(z::real) . \<forall>x<z. x \<ge> t = False "
+  "\<exists>(z::real) . \<forall>x<z. (x = t) = False "  "\<exists>(z::real) . \<forall>x<z. (x \<noteq> t) = True "
+  "\<exists>z. \<forall>(x::real)<z. (P::bool) = P"
+  "\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
+  \<exists>z. \<forall>x<z. (P1 x \<and> P2 x) = (P1' \<and> P2')"
+  "\<lbrakk>\<exists>(z1::real). \<forall>x<z1. P1 x = P1'; \<exists>z2. \<forall>x<z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
+  \<exists>z. \<forall>x<z. (P1 x \<or> P2 x) = (P1' \<or> P2')"
+  by (rule_tac x="t" in exI,simp)+
+(clarsimp,rule_tac x="min z1 z2" in exI,simp)+
+
+lemma minf_ex: "\<lbrakk>\<exists>z. \<forall>x<z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x"
+  by clarsimp (rule_tac x="z - 1" in exI, auto)
+
+  (* Synthesis of \<exists>z. \<forall>x>z. P x = P1 *)
+lemma pinf: 
+  "\<exists>(z::real) . \<forall>x>z. x < t = False "  "\<exists>(z::real) . \<forall>x>z. x > t = True "
+  "\<exists>(z::real) . \<forall>x>z. x \<le> t = False "  "\<exists>(z::real) . \<forall>x>z. x \<ge> t = True "
+  "\<exists>(z::real) . \<forall>x>z. (x = t) = False "  "\<exists>(z::real) . \<forall>x>z. (x \<noteq> t) = True "
+  "\<exists>z. \<forall>(x::real)>z. (P::bool) = P"
+  "\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
+  \<exists>z. \<forall>x>z. (P1 x \<and> P2 x) = (P1' \<and> P2')"
+  "\<lbrakk>\<exists>(z1::real). \<forall>x>z1. P1 x = P1'; \<exists>z2. \<forall>x>z2. P2 x = P2'\<rbrakk> \<Longrightarrow>
+  \<exists>z. \<forall>x>z. (P1 x \<or> P2 x) = (P1' \<or> P2')"
+  by (rule_tac x="t" in exI,simp)+
+(clarsimp,rule_tac x="max z1 z2" in exI,simp)+
+
+lemma pinf_ex: "\<lbrakk>\<exists>z. \<forall>x>z. P (x::real) = P1 ; P1\<rbrakk> \<Longrightarrow> \<exists> x. P x"
+  by clarsimp (rule_tac x="z+1" in exI, auto)
+
+    (* The ~P1 \<and> ~P2 \<and> P x \<longrightarrow> \<exists> u,u' \<in> U. u \<le> x \<le> u'*)
+lemma nmilbnd: 
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) > t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> (x::real) \<ge> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )"
+  "\<forall> (x::real). ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )"
+  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ; 
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> 
+  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 (x::real) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ; 
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x )\<rbrakk> \<Longrightarrow> 
+  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
+  by auto (rule_tac x="t" in bexI,simp,simp)
+
+lemma npiubnd: 
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) < t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) > t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) \<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<ge> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  (x::real) = t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> (x::real) \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )"
+  "\<forall> (x::real). ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x )"
+  "\<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> 
+  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  "\<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> 
+  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<ge> x)"
+  by auto (rule_tac x="t" in bexI,simp,simp)
+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> 
+  \<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')"
+by auto
+
+  (* 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*)
+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)"
+proof(clarsimp)
+  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" 
+    and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
+  from tU noU ly yu have tny: "t\<noteq>y" by auto
+  {assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp 
+    with tU noU have "False" by auto} hence "\<not> y>t"  by auto hence "y \<le> t" by auto
+  thus "y < t" using tny by simp 
+qed
+    
+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)"
+proof(clarsimp)
+  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" and xu: "x<u"
+  and px: "x > t" and ly: "l<y" and yu:"y < u"
+  from tU noU ly yu have tny: "t\<noteq>y" by auto
+  {assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp 
+    with tU noU have "False" by auto}
+  hence	"\<not> y<t"  by auto hence "y \<ge> t" by auto
+  thus "y > t" using tny by simp 
+qed
+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)"
+proof(clarsimp)
+  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" and xu: "x<u"
+  and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
+  from tU noU ly yu have tny: "t\<noteq>y" by auto
+  {assume H: "y> t" hence "l < t \<and> t < u" using px lx yu by simp 
+    with tU noU have "False" by auto}
+  hence	"\<not> y>t"  by auto thus "y \<le> t" by auto
+qed
+    
+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)"
+proof(clarsimp)
+  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" and xu: "x<u"
+  and px: "x \<ge> t" and ly: "l<y" and yu:"y < u"
+  from tU noU ly yu have tny: "t\<noteq>y" by auto
+  {assume H: "y< t" hence "l < t \<and> t < u" using px xu ly by simp 
+    with tU noU have "False" by auto}
+  hence	"\<not> y<t"  by auto thus "y \<ge> t" by auto
+qed
+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
+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
+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
+
+lemma lin_dense_conj: 
+  "\<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;  
+  \<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
+  \<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
+  by blast
+lemma lin_dense_disj: 
+  "\<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;  
+  \<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow> 
+  \<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) 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
+  by blast
+
+lemma finite_set_intervals:
+  assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
+  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"
+  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"
+proof-
+  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
+  let ?xM = "{y. y\<in> S \<and> x \<le> y}"
+  let ?a = "Max ?Mx"
+  let ?b = "Min ?xM"
+  have MxS: "?Mx \<subseteq> S" by blast
+  hence fMx: "finite ?Mx" using fS finite_subset by auto
+  from lx linS have linMx: "l \<in> ?Mx" by blast
+  hence Mxne: "?Mx \<noteq> {}" by blast
+  have xMS: "?xM \<subseteq> S" by blast
+  hence fxM: "finite ?xM" using fS finite_subset by auto
+  from xu uinS have linxM: "u \<in> ?xM" by blast
+  hence xMne: "?xM \<noteq> {}" by blast
+  have ax:"?a \<le> x" using Mxne fMx by auto
+  have xb:"x \<le> ?b" using xMne fxM by auto
+  have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
+  have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
+  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
+  proof(clarsimp)
+    fix y   assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
+    from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by auto
+    moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by simp}
+    moreover {assume "y \<in> ?xM" hence "y \<ge> ?b" using xMne fxM by auto with yb have "False" by simp}
+    ultimately show "False" by blast
+  qed
+  from ainS binS noy ax xb px show ?thesis by blast
+qed
+
+lemma finite_set_intervals2:
+  assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
+  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"
+  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)"
+proof-
+  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
+  obtain a and b where 
+    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S" 
+    and axb: "a \<le> x \<and> x \<le> b \<and> P x"  by auto
+  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by auto
+  thus ?thesis using px as bs noS by blast 
+qed
+
+lemma rinf_U:
+  assumes fU: "finite U" 
+  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 
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
+  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')"
+  and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P (x::real)"
+  shows "\<exists> u\<in> U. \<exists> u' \<in> U. P ((u + u') / 2)" 
+proof-
+  from ex obtain x where px: "P x" by blast
+  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u'" by auto
+  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 
+  from uU have Une: "U \<noteq> {}" by auto
+  let ?l = "Min U"
+  let ?u = "Max U"
+  have linM: "?l \<in> U" using fU Une by simp
+  have uinM: "?u \<in> U" using fU Une by simp
+  have lM: "\<forall> t\<in> U. ?l \<le> t" using Une fU by auto
+  have Mu: "\<forall> t\<in> U. t \<le> ?u" using Une fU by auto
+  have "?l \<le> u" using uU Une lM by auto hence lx: "?l \<le> x" using ux by simp
+  have "u' \<le> ?u" using uU' Une Mu by simp hence xu: "x \<le> ?u" using xu' by simp
+  from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
+  have "(\<exists> s\<in> U. P s) \<or> 
+      (\<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)" .
+  moreover { fix u assume um: "u\<in>U" and pu: "P u"
+    have "(u + u) / 2 = u" by auto 
+    with um pu have "P ((u + u) / 2)" by simp
+    with um have ?thesis by blast}
+  moreover{
+    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"
+      then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U" 
+	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"
+	by blast
+      from t1x xt2 have t1t2: "t1 < t2" by simp
+      let ?u = "(t1 + t2) / 2"
+      from less_half_sum[OF t1t2] gt_half_sum[OF t1t2] have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto
+      from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
+      with t1M t2M have ?thesis by blast}
+    ultimately show ?thesis by blast
+  qed
+
+theorem fr_eq: 
+  assumes fU: "finite U"
+  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 
+   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
+  and nmibnd: "\<forall>x. \<not> MP \<and> P (x::real) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
+  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<ge> x)"
+  and mi: "\<exists>z. \<forall>x<z. P x = MP"  and pi: "\<exists>z. \<forall>x>z. P x = PP"
+  shows "(\<exists> x. P (x::real)) = (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P ((u + u') / 2)))" 
+  (is "_ = (_ \<or> _ \<or> ?F)" is "?E = ?D")
+proof
+  assume px: "\<exists> x. P x"
+  have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
+  moreover {assume "MP \<or> PP" hence "?D" by blast}
+  moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
+    from npmibnd[OF nmibnd npibnd] 
+    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')" .
+    from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}   
+  ultimately show "?D" by blast
+next
+  assume "?D" 
+  moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .}
+  moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
+  moreover {assume f:"?F" hence "?E" by blast}
+  ultimately show "?E" by blast
+qed
+
+lemma fr_simps: 
+  "(True | P) = True"  "(P | True) = True"  "(True & P) = P"  "(P & True) = P"
+  "(P & P) = P"  "(P & (P & P')) = (P & P')"  "(P & (P | P')) = P"  "(False | P) = P"
+  "(P | False) = P"  "(False & P) = False"  "(P & False) = False"  "(P | P) = P"
+  "(P | (P | P')) = (P | P')"  "(P | (P & P')) = P"  "(~ True) = False"  "(~ False) = True"
+  "(x::real) \<le> x"  "(\<exists> u\<in> {}. Q u) = False"
+  "(\<exists> u\<in> (insert (x::real) U). \<exists>u'\<in> (insert x U). R ((u+u') / 2)) = 
+  ((R x) \<or> (\<exists>u\<in>U. R((x+u) / 2))\<or> (\<exists> u\<in> U. \<exists> u'\<in> U. R ((u + u') /2)))"
+  "(\<exists> u\<in> (insert (x::real) U). R u) = (R x \<or> (\<exists> u\<in> U. R u))"
+  "Q' (((t::real) + t)/2) = Q' t"
+by (auto simp add: add_ac)
+  
+lemma fr_prepqelim:
+  "(\<exists> x. True) = True" "(\<exists> x. False) = False" "(ALL x. A x) = (~ (EX x. ~ (A x)))"
+  "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" "(\<not> (P \<longrightarrow> Q)) = (P \<and> (\<not> Q))" "(\<not> (P = Q)) = ((\<not> P) = Q)" 
+  "(\<not> (P \<and> Q)) = ((\<not> P) \<or> (\<not> Q))" "(\<not> (P \<or> Q)) = ((\<not> P) \<and> (\<not> Q))"
+by auto
+  (* Lemmas for the normalization of Expressions *)
+lemma nadd_cong:  
+  assumes m: "m'*m = l" and n: "n'*n = (l::real)"
+  and mz: "m \<noteq> 0" and nz: "n \<noteq> 0" and lz: "l \<noteq> 0"
+  and ad: "(m'*t + n'*s) = t'"
+  shows "t/m + s/n = (t' / l)"
+proof-
+  from lz m n have mz': "m'\<noteq>0" and nz':"n' \<noteq> 0" by auto
+  have "t' / l = (m'*t + n'*s) / l" using ad by simp
+  also have "\<dots> = (m'*t) / l + (n'*s) / l" by (simp add: add_divide_distrib)
+  also have "\<dots> = (m'*t) /(m'*m) + (n'*s) /(n'*n)" using m n by simp
+  also have "\<dots> = t/m + s/n" using mz nz mz' nz' by simp
+  finally show ?thesis  by simp
+qed
+
+lemma nadd_cong_same: "\<lbrakk> (n::real) = m ; t+s = t'\<rbrakk> \<Longrightarrow> t/n + s/m = t'/n"  
+  by (simp add: add_divide_distrib[symmetric])
+lemma plus_cong: "\<lbrakk>t = t'; s = s'; t' + s' = r\<rbrakk> \<Longrightarrow> t+s = r"
+  by simp
+lemma diff_cong: "\<lbrakk>t = t'; s = s'; t' - s' = r\<rbrakk> \<Longrightarrow> t-s = r"
+  by simp
+lemma mult_cong2: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> t*c = r"
+  by (simp add: mult_ac)
+lemma mult_cong: "\<lbrakk>(t ::real) = t'; c*t' = r\<rbrakk> \<Longrightarrow> c*t = r"
+  by simp
+lemma divide_cong: "\<lbrakk> (t::real) = t' ; t'/n = r\<rbrakk> \<Longrightarrow> t/n = r"
+  by simp
+lemma naddh_cong_ts: "\<lbrakk>t1 + (s::real) = t'\<rbrakk> \<Longrightarrow> (x + t1) + s = x + t'" by simp
+lemma naddh_cong_st: "\<lbrakk>(t::real) + s = t'\<rbrakk> \<Longrightarrow> t+ (x + s) = x + t'" by simp
+lemma naddh_cong_same: "\<lbrakk>(c1::real) + c2 = c ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = c*x + t"
+  by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric])
+lemma naddh_cong_same0: "\<lbrakk>(c1::real) + c2 = 0 ; t1 + t2 = t\<rbrakk> \<Longrightarrow> (c1*x + t1) + (c2*x+t2) = t"
+  by (simp add: ring_eq_simps,simp only: ring_distrib(2)[symmetric]) simp
+lemma ncmul_congh: "\<lbrakk> c*c' = (k::real) ; c*t = t'\<rbrakk>  \<Longrightarrow> c*(c'*x + t) = k*x + t'"
+  by (simp add: ring_eq_simps)
+lemma ncmul_cong: "\<lbrakk> c / n = c'/n' ; c'*t = (t'::real)\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'"
+proof-
+  assume "c / n = c'/n'" and "c'*t = (t'::real)"
+  have "\<lbrakk> c' / n' = c/n ; (t'::real) = c'*t\<rbrakk> \<Longrightarrow> c* (t/n) = t'/n'"
+    by (simp add: divide_inverse ring_eq_simps)  thus ?thesis using prems by simp
+qed
+
+lemma nneg_cong: "(-1 ::real)*t = t' \<Longrightarrow> - t = t'"  by simp
+lemma uminus_cong: "\<lbrakk> t = t' ; - t' = r\<rbrakk> \<Longrightarrow>  - t = r"  by simp
+lemma nsub_cong: "\<lbrakk>- (s::real) = s'; t + s' = t'\<rbrakk> \<Longrightarrow> t - s = t'"  by simp
+lemma ndivide_cong: "m*n = (m'::real) \<Longrightarrow> (t/m) / n = t / m'"  by simp
+lemma normalizeh_var: "(x::real) = (1*x + 0) / 1"  by simp
+lemma nrefl: "(x::real) = x/1"  by simp
+
+    (* cong rules for atoms normalization *)
+  (* the < -case *)
+lemma normalize_ltxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0"
+  shows "(s < t) = (x < r'/c')"
+proof-
+  from cnp have cnz: "c \<noteq> 0" by auto
+  from cnp have nnz: "n\<noteq>0" by auto
+  from rr' have rr'': "-(r/c) = r'/c'" by simp
+  have "s < t = (s - t < 0)" by simp
+  also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp
+  also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib)
+  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) < (n/c)*0)" 
+    using cnp mult_less_cancel_left[where c="(n/c)" and b="0"] by simp 
+  also have "\<dots> = (x + r/c < 0)" 
+    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
+  also have "\<dots> = (x < - (r/c))" by auto
+  finally show ?thesis using rr'' by simp
+qed
+
+lemma normalize_ltxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0"
+  shows "(s < t) = (x > r'/c')"
+proof-
+  from cnp have cnz: "c \<noteq> 0" by auto
+  from cnp have nnz: "n\<noteq>0" by auto
+  from cnp have cnp': "\<not> (n/c > 0)" by simp
+  from rr' have rr'': "-(r/c) = r'/c'" by simp
+  have "s < t = (s - t < 0)" by simp
+  also have "\<dots> = ((c*x+r) / n < 0)" using smt by simp
+  also have "\<dots> = ((c/n)*x + r/n < 0)" by (simp add: add_divide_distrib)
+  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) > 0)"
+    using zero_less_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp cnp' simp_thms]
+    by simp 
+  also have "\<dots> = (x + r/c > 0)" 
+    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
+  also have "\<dots> = (x > - (r/c))" by auto
+  finally show ?thesis using rr'' by simp
+qed
+lemma normalize_ltground_cong: "\<lbrakk> s -t = (r::real) ; r < 0 = P\<rbrakk> \<Longrightarrow> s < t = P"  by auto
+lemma normalize_ltnoxpos_cong: 
+  assumes st: "s - t = (r::real) / n" and mp: "n > 0"
+  shows "s < t = (r <0)"
+proof-  
+  have "s < t = (s - t < 0)" by simp
+  also have "\<dots> = (r / n < 0)" using st by simp
+  also have "\<dots> = (n* (r/n) < 0)" using mult_less_0_iff[where a="n" and b="r/n"] mp by simp
+  finally show ?thesis using mp by auto
+qed
+
+lemma normalize_ltnoxneg_cong: 
+  assumes st: "s - t = (r::real) / n" and mp: "n < 0"
+  shows "s < t = (r > 0)"
+proof-  
+  have "s < t = (s - t < 0)" by simp
+  also have "\<dots> = (r / n < 0)" using st by simp
+  also have "\<dots> = (n* (r/n) > 0)" using zero_less_mult_iff[where a="n" and b="r/n"] mp by simp
+  finally show ?thesis using mp by auto
+qed
+
+  (* the <= -case *)
+lemma normalize_lexpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cnp: "n/c > 0" and rr': "r/c + r'/c' = 0"
+  shows "(s \<le> t) = (x \<le> r'/c')"
+proof-
+  from cnp have cnz: "c \<noteq> 0" by auto
+  from cnp have nnz: "n\<noteq>0" by auto
+  from rr' have rr'': "-(r/c) = r'/c'" by simp
+  have "s \<le> t = (s - t \<le> 0)" by simp
+  also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp
+  also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib)
+  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<le> (n/c)*0)" 
+    using cnp mult_le_cancel_left[where c="(n/c)" and b="0"] by simp 
+  also have "\<dots> = (x + r/c \<le> 0)" 
+    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
+  also have "\<dots> = (x \<le> - (r/c))" by auto
+  finally show ?thesis using rr'' by simp
+qed
+
+lemma normalize_lexneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cnp: "n/c < 0" and rr': "r/c + r'/c' = 0"
+  shows "(s \<le> t) = (x \<ge> r'/c')"
+proof-
+  from cnp have cnz: "c \<noteq> 0" by auto
+  from cnp have nnz: "n\<noteq>0" by auto
+  from cnp have cnp': "\<not> (n/c \<ge> 0) \<and> n/c \<le> 0" by simp
+  from rr' have rr'': "-(r/c) = r'/c'" by simp
+  have "s \<le> t = (s - t \<le> 0)" by simp
+  also have "\<dots> = ((c*x+r) / n \<le> 0)" using smt by simp
+  also have "\<dots> = ((c/n)*x + r/n \<le> 0)" by (simp add: add_divide_distrib)
+  also have "\<dots> = ( (n/c)*((c/n)*x + r/n) \<ge> 0)"
+    using zero_le_mult_iff[where a="n/c" and b="(c/n)*x + r/n", simplified cnp' simp_thms]
+    by simp 
+  also have "\<dots> = (x + r/c \<ge> 0)" 
+    using cnz nnz by (simp add: add_divide_distrib ring_eq_simps)
+  also have "\<dots> = (x \<ge> - (r/c))" by auto
+  finally show ?thesis using rr'' by simp
+qed
+lemma normalize_leground_cong: "\<lbrakk> s -t = (r::real) ; r \<le> 0 = P\<rbrakk> \<Longrightarrow> s \<le> t = P"  by auto
+lemma normalize_lenoxpos_cong: 
+  assumes st: "s - t = (r::real) / n" and mp: "n > 0"
+  shows "s \<le> t = (r \<le>0)"
+proof-  
+  have "s \<le> t = (s - t \<le> 0)" by simp
+  also have "\<dots> = (r / n \<le> 0)" using st by simp
+  also have "\<dots> = (n* (r/n) \<le> 0)" using mult_le_0_iff[where a="n" and b="r/n"] mp by simp
+  finally show ?thesis using mp by auto
+qed
+
+lemma normalize_lenoxneg_cong: 
+  assumes st: "s - t = (r::real) / n" and mp: "n < 0"
+  shows "s \<le> t = (r \<ge> 0)"
+proof-  
+  have "s \<le> t = (s - t \<le> 0)" by simp
+  also have "\<dots> = (r / n \<le> 0)" using st by simp
+  also have "\<dots> = (n* (r/n) \<ge> 0)" using zero_le_mult_iff[where a="n" and b="r/n"] mp by simp
+  finally show ?thesis using mp by auto
+qed
+    (* The = -case *)
+
+lemma normalize_eqxpos_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cp: "c > 0" and nnz: "n \<noteq> 0" and rr': "r+ r' = 0"
+  shows "(s = t) = (x = r'/c)"
+proof-
+  from rr' have rr'': "-r = r'" by simp
+  have "(s = t) = (s - t = 0)" by simp
+  also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp
+  also have "\<dots> = (c*x = -r)" using nnz by auto
+  also have "\<dots> = (x = (-r) / c)" using cp eq_divide_eq[where c="c" and a="x" and b="-r"]
+    by (simp add: mult_ac)
+  finally show ?thesis using rr'' by simp
+qed
+
+lemma normalize_eqxneg_cong: assumes smt: "s - t = (c*x+r) / (n::real)"
+  and cp: "c < 0" and nnz: "n \<noteq> 0" and cc': "c+ c' = 0"
+  shows "(s = t) = (x = r/c')"
+proof-
+  from cc' have cc'': "-c = c'" by simp
+  have "(s = t) = (s - t = 0)" by simp
+  also have "\<dots> = ((c*x + r) /n = 0)" using smt by simp
+  also have "\<dots> = ((-c)*x = r)" using nnz by auto
+  also have "\<dots> = (x = r / (-c))" using cp eq_divide_eq[where c="-c" and a="x" and b="r"]
+    by (simp add: mult_ac)
+  finally show ?thesis using cc'' by simp
+qed
+
+lemma normalize_eqnox_cong: "\<lbrakk>s - t = (r::real) / n;n \<noteq> 0\<rbrakk> \<Longrightarrow> s = t = (r = 0)" by auto
+
+lemma normalize_eqground_cong: "\<lbrakk>s - t =(r::real)/n;n \<noteq> 0;(r = 0) = P \<rbrakk> \<Longrightarrow> s=t = P" by auto
+
+lemma trivial_sum_of_opposites: "-t = t' \<Longrightarrow> t + t' = (0::real)" by simp
+lemma sum_of_opposite_denoms: 
+  assumes cc': "(c::real) + c' = 0" shows "r/c + r/c' = 0"
+proof-
+  from cc' have "c' = -c" by simp
+  thus ?thesis by simp
+qed
+lemma sum_of_same_denoms: " -r = (r'::real) \<Longrightarrow> r/c + r'/c = 0"  by auto
+lemma normalize_not_lt: "t \<le> (s::real) = P \<Longrightarrow> (\<not> s<t) = P"  by auto
+lemma normalize_not_le: "t < (s::real) = P \<Longrightarrow> (\<not> s\<le>t) = P"  by auto
+lemma normalize_not_eq: "\<lbrakk> t = (s::real) = P ; (~P) = P' \<rbrakk> \<Longrightarrow> (s\<noteq>t) = P'"  by auto
+lemma ex_eq_cong: "(!! x. A x = B x) \<Longrightarrow> ((\<exists>x. A x) = (\<exists> x. B x))"  by blast
+
+use "ferrante_rackoff_proof.ML"
+use "ferrante_rackoff.ML"
+setup "Ferrante_Rackoff.setup"
+
+end

--- a/src/HOL/Real/Real.thy	Tue May 16 09:19:12 2006 +0200
+++ b/src/HOL/Real/Real.thy	Tue May 16 13:01:22 2006 +0200
@@ -1,4 +1,7 @@
+
+(* $Id$ *)
+
 theory Real
-imports ContNotDenum RealPow
+imports ContNotDenum Ferrante_Rackoff
 begin
-end
\ No newline at end of file
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ferrante_rackoff.ML	Tue May 16 13:01:22 2006 +0200
@@ -0,0 +1,129 @@
+(*
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+
+Ferrante and Rackoff Algorithm.
+*)
+
+structure Ferrante_Rackoff:
+sig
+  val trace : bool ref
+  val ferrack_tac : bool -> int -> tactic
+  val setup : theory -> theory
+end =
+struct
+
+val trace = ref false;
+fun trace_msg s = if !trace then tracing s else ();
+
+val context_ss = simpset_of (the_context ());
+
+val nT = HOLogic.natT;
+val binarith = map thm
+  ["Pls_0_eq", "Min_1_eq",
+ "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
+  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
+  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
+  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
+  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
+  "bin_add_Pls_right", "bin_add_Min_right"];
+ val intarithrel = 
+     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
+		"int_le_number_of_eq","int_iszero_number_of_0",
+		"int_less_number_of_eq_neg"]) @
+     (map (fn s => thm s RS thm "lift_bool") 
+	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
+	   "int_neg_number_of_Min"])@
+     (map (fn s => thm s RS thm "nlift_bool") 
+	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
+     
+val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
+			"int_number_of_diff_sym", "int_number_of_mult_sym"];
+val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
+			"mult_nat_number_of", "eq_nat_number_of",
+			"less_nat_number_of"]
+val powerarith = 
+    (map thm ["nat_number_of", "zpower_number_of_even", 
+	      "zpower_Pls", "zpower_Min"]) @ 
+    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
+			   thm "one_eq_Numeral1_nring"] 
+  (thm "zpower_number_of_odd"))]
+
+val comp_arith = binarith @ intarith @ intarithrel @ natarith 
+	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
+
+fun prepare_for_linr sg q fm = 
+  let
+    val ps = Logic.strip_params fm
+    val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
+    val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
+    fun mk_all ((s, T), (P,n)) =
+      if 0 mem loose_bnos P then
+        (HOLogic.all_const T $ Abs (s, T, P), n)
+      else (incr_boundvars ~1 P, n-1)
+    fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
+      val rhs = hs
+(*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
+    val np = length ps
+    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+      (foldr HOLogic.mk_imp c rhs, np) ps
+    val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
+      (term_frees fm' @ term_vars fm');
+    val fm2 = foldr mk_all2 fm' vs
+  in (fm2, np + length vs, length rhs) end;
+
+(*Object quantifier to meta --*)
+fun spec_step n th = if (n=0) then th else (spec_step (n-1) th) RS spec ;
+
+(* object implication to meta---*)
+fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
+
+
+fun ferrack_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
+  let
+    val g = List.nth (prems_of st, i - 1)
+    val sg = sign_of_thm st
+    (* Transform the term*)
+    val (t,np,nh) = prepare_for_linr sg q g
+    (* Some simpsets for dealing with mod div abs and nat*)
+    val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [split_min, split_max]
+    (* simp rules for elimination of abs *)
+    val simpset3 = HOL_basic_ss addsplits [abs_split]
+    val ct = cterm_of sg (HOLogic.mk_Trueprop t)
+    (* Theorem for the nat --> int transformation *)
+    val pre_thm = Seq.hd (EVERY
+      [simp_tac simpset0 1,
+       TRY (simp_tac simpset3 1), TRY (simp_tac context_ss 1)]
+      (trivial ct))
+    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
+    (* The result of the quantifier elimination *)
+    val (th, tac) = case (prop_of pre_thm) of
+        Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+    let val pth = Ferrante_Rackoff_Proof.qelim (cterm_of sg (Pattern.eta_long [] t1))
+    in 
+          (trace_msg ("calling procedure with term:\n" ^
+             Sign.string_of_term sg t1);
+           ((pth RS iffD2) RS pre_thm,
+            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
+    end
+      | _ => (pre_thm, assm_tac i)
+  in (rtac (((mp_step nh) o (spec_step np)) th) i 
+      THEN tac) st
+  end handle Subscript => no_tac st | Ferrante_Rackoff_Proof.FAILURE _ => no_tac st);
+
+fun ferrack_args meth =
+ let val parse_flag = 
+         Args.$$$ "no_quantify" >> (K (K false));
+ in
+   Method.simple_args 
+  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
+    curry (Library.foldl op |>) true)
+    (fn q => fn _ => meth q 1)
+  end;
+
+val setup =
+  Method.add_method ("ferrack",
+     ferrack_args (Method.SIMPLE_METHOD oo ferrack_tac),
+     "LCF-proof-producing decision procedure for linear real arithmetic");
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Tue May 16 13:01:22 2006 +0200
@@ -0,0 +1,818 @@
+(*
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+
+LCF proof synthesis for Ferrante and Rackoff.
+*)
+
+structure Ferrante_Rackoff_Proof:
+sig
+  val qelim: cterm -> thm
+  exception FAILURE of string
+end =
+struct
+
+    (* Some certified types *)
+val cbT = ctyp_of (the_context()) HOLogic.boolT;
+val rT = Type("RealDef.real",[]);
+val crT = ctyp_of (the_context()) (Type("RealDef.real",[]));
+    (* Normalization*)
+
+
+	(* Computation of uset *)
+fun uset x fm = 
+    case fm of
+	Const("op &",_)$p$q => (uset x p) union (uset x q)
+      | Const("op |",_)$p$q => (uset x p) union (uset x q)
+      | Const("Orderings.less",_)$s$t => if s=x then [t] 
+			       else if t = x then [s]
+			       else []
+      | Const("Orderings.less_eq",_)$s$t => if s=x then [t] 
+			       else if t = x then [s]
+			       else []
+      | Const("op =",_)$s$t => if s=x then [t] 
+			       else []
+      | Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t] 
+						 else []
+      | _ => [];
+val rsT = Type("set",[rT]);
+fun holrealset [] = Const("{}",rsT)
+  | holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
+fun prove_bysimp thy ss t = Goal.prove thy [] [] 
+		       (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);
+
+fun inusetthms sg x fm = 
+    let val U = uset x fm
+	val hU = holrealset U
+	fun inC T = Const("op :",[T,Type("set",[T])] ---> HOLogic.boolT);
+	val ss = simpset_of sg
+	fun proveinU t = prove_bysimp sg ss ((inC rT)$t$hU)
+	val uf = prove_bysimp sg ss ((inC rsT)$hU$Const("Finite_Set.Finites",Type("set",[rsT])))
+    in (U,cterm_of sg hU,map proveinU U,uf)
+    end;
+
+	(* Theorems for minus/plusinfinity *)
+val [minf_lt,minf_gt,minf_le,minf_ge,minf_eq,minf_neq,minf_fm,minf_conj,minf_disj] = thms"minf";
+val [pinf_lt,pinf_gt,pinf_le,pinf_ge,pinf_eq,pinf_neq,pinf_fm,pinf_conj,pinf_disj] = thms"pinf";
+    (* Theorems for boundedness from below/above *)
+val [nmilbnd_lt,nmilbnd_gt,nmilbnd_le,nmilbnd_ge,nmilbnd_eq,nmilbnd_neq,nmilbnd_fm,nmilbnd_conj,nmilbnd_disj] = thms"nmilbnd";
+val [npiubnd_lt,npiubnd_gt,npiubnd_le,npiubnd_ge,npiubnd_eq,npiubnd_neq,npiubnd_fm,npiubnd_conj,npiubnd_disj] = thms"npiubnd";
+
+    (* Theorems for no changes over smallest intervals in U *)
+val lin_dense_lt = thm "lin_dense_lt";
+val lin_dense_le = thm "lin_dense_le";
+val lin_dense_gt = thm "lin_dense_gt";
+val lin_dense_ge = thm "lin_dense_ge";
+val lin_dense_eq = thm "lin_dense_eq";
+val lin_dense_neq = thm "lin_dense_neq";
+val lin_dense_conj = thm "lin_dense_conj";
+val lin_dense_disj = thm "lin_dense_disj";
+val lin_dense_fm = thm "lin_dense_fm";
+val fr_eq = thm "fr_eq";
+val fr_simps = thms "fr_simps";
+
+fun dest5 [] = ([],[],[],[],[])
+  | dest5 ((x,y,z,w,v)::xs) = 
+    let val (x',y',z',w',v') = dest5 xs 
+    in (x::x',y::y',z::z',w::w',v::v') end ;
+
+fun dest2 [] = ([],[])
+  | dest2 ((x,y)::xs) = let val (x',y') = dest2 xs 
+			    in (x::x',y::y') end ;
+fun myfwd (th1,th2,th3,th4,th5) xs =
+    let val (ths1,ths2,ths3,ths4,ths5) = dest5 xs
+    in (ths1 MRS th1,ths2 MRS th2,ths3 MRS th3,ths4 MRS th4, ths5 MRS th5)
+    end;
+
+fun myfwd2 (th1,th2) xs =
+    let val (ths1,ths2) = dest2 xs
+    in (ths1 MRS th1,ths2 MRS th2)
+    end;
+
+fun decomp_mpinf sg x (U,CU,uths) fm = 
+    let val cx = cterm_of sg x in
+	(case fm of
+	    Const("op &",_)$p$q => 
+	    ([p,q],myfwd (minf_conj,pinf_conj, nmilbnd_conj, npiubnd_conj,lin_dense_conj))	
+	  | Const("op |",_)$p$q => 
+	    ([p,q],myfwd (minf_disj,pinf_disj, nmilbnd_disj,npiubnd_disj,lin_dense_disj))
+	  | Const("Orderings.less",_)$s$t => 
+	    if s= x then 
+		let val ct = cterm_of sg t
+		    val tinU = nth uths (find_index (fn a => a=t) U)
+		    val mith = instantiate' [] [SOME ct] minf_lt
+		    val pith = instantiate' [] [SOME ct] pinf_lt
+		    val nmilth = tinU RS nmilbnd_lt
+		    val npiuth = tinU RS npiubnd_lt
+		    val lindth = tinU RS lin_dense_lt
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+	    else if t = x then 
+		let val ct = cterm_of sg s
+		    val tinU = nth uths (find_index (fn a => a=s) U)
+		    val mith = instantiate' [] [SOME ct] minf_gt
+		    val pith = instantiate' [] [SOME ct] pinf_gt
+		    val nmilth = tinU RS nmilbnd_gt
+		    val npiuth = tinU RS npiubnd_gt
+		    val lindth = tinU RS lin_dense_gt
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+
+	    else
+		let val cfm = cterm_of sg fm 
+		    val mith = instantiate' [] [SOME cfm] minf_fm
+		    val pith = instantiate' [] [SOME cfm] pinf_fm
+		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+		end
+	  | Const("Orderings.less_eq",_)$s$t => 
+	    if s= x then 
+		let val ct = cterm_of sg t
+		    val tinU = nth uths (find_index (fn a => a=t) U)
+		    val mith = instantiate' [] [SOME ct] minf_le
+		    val pith = instantiate' [] [SOME ct] pinf_le
+		    val nmilth = tinU RS nmilbnd_le
+		    val npiuth = tinU RS npiubnd_le
+		    val lindth = tinU RS lin_dense_le
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+	    else if t = x then 
+		let val ct = cterm_of sg s
+		    val tinU = nth uths (find_index (fn a => a=s) U)
+		    val mith = instantiate' [] [SOME ct] minf_ge
+		    val pith = instantiate' [] [SOME ct] pinf_ge
+		    val nmilth = tinU RS nmilbnd_ge
+		    val npiuth = tinU RS npiubnd_ge
+		    val lindth = tinU RS lin_dense_ge
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+
+	    else
+		let val cfm = cterm_of sg fm 
+		    val mith = instantiate' [] [SOME cfm] minf_fm
+		    val pith = instantiate' [] [SOME cfm] pinf_fm
+		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+		end
+	  | Const("op =",_)$s$t => 
+	    if s= x then 
+		let val ct = cterm_of sg t
+		    val tinU = nth uths (find_index (fn a => a=t) U)
+		    val mith = instantiate' [] [SOME ct] minf_eq
+		    val pith = instantiate' [] [SOME ct] pinf_eq
+		    val nmilth = tinU RS nmilbnd_eq
+		    val npiuth = tinU RS npiubnd_eq
+		    val lindth = tinU RS lin_dense_eq
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+	    else
+		let val cfm = cterm_of sg fm 
+		    val mith = instantiate' [] [SOME cfm] minf_fm
+		    val pith = instantiate' [] [SOME cfm] pinf_fm
+		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+		end
+
+	  | Const("Not",_)$(Const("op =",_)$s$t) => 
+	    if s= x then 
+		let val ct = cterm_of sg t
+		    val tinU = nth uths (find_index (fn a => a=t) U)
+		    val mith = instantiate' [] [SOME ct] minf_neq
+		    val pith = instantiate' [] [SOME ct] pinf_neq
+		    val nmilth = tinU RS nmilbnd_neq
+		    val npiuth = tinU RS npiubnd_neq
+		    val lindth = tinU RS lin_dense_neq
+		in ([],myfwd (mith,pith,nmilth,npiuth,lindth))
+		end 
+	    else
+		let val cfm = cterm_of sg fm 
+		    val mith = instantiate' [] [SOME cfm] minf_fm
+		    val pith = instantiate' [] [SOME cfm] pinf_fm
+		    val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+		    val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+		    val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+		in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+		end
+	  | _ => let val cfm = cterm_of sg fm 
+		     val mith = instantiate' [] [SOME cfm] minf_fm
+		     val pith = instantiate' [] [SOME cfm] pinf_fm
+		     val nmilth = instantiate' [] [SOME cfm, SOME CU] nmilbnd_fm
+		     val npiuth = instantiate' [] [SOME cfm, SOME CU] npiubnd_fm
+		     val lindth = instantiate' [] [SOME CU, SOME cfm] lin_dense_fm
+		 in ([], myfwd (mith,pith,nmilth,npiuth,lindth))
+		 end)
+    end;
+
+fun ferrack_eq thy p = 
+    case p of
+	Const("Ex",_)$Abs(x1,T,p1) => 
+	let val (xn,fm) = variant_abs(x1,T,p1)
+	    val x = Free(xn,T)
+	    val (u,cu,uths,uf) = inusetthms thy x fm
+	    val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
+	    val frth = [uf,lind,nmi,npi,mi,pi] MRS fr_eq
+	    val (cTp,ceq) = Thm.dest_comb (cprop_of frth)
+	    val qth = (Simplifier.rewrite (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
+					  (snd (Thm.dest_comb ceq))) RS meta_eq_to_obj_eq
+	in [frth,qth] MRS trans
+	end
+      | _ => instantiate' [SOME cbT] [SOME (cterm_of thy p)] refl;
+
+(* Code for normalization of terms and Formulae *)
+    (* For NNF reuse the CooperProof methods*)
+    (*FIXME:: This is copied from cooper_proof.ML *)
+val FWD = fn th => fn ths => ths MRS th;
+
+val qe_Not = thm "qe_Not";
+val qe_conjI = thm "qe_conjI";
+val qe_disjI = thm "qe_disjI";
+val qe_impI = thm "qe_impI";
+val qe_eqI = thm "qe_eqI";
+val qe_exI = thm "qe_exI";
+val qe_ALLI = thm "qe_ALLI";
+
+val nnf_nn = thm "nnf_nn";
+val nnf_im = thm "nnf_im";
+val nnf_eq = thm "nnf_eq";
+val nnf_sdj = thm "nnf_sdj";
+val nnf_ncj = thm "nnf_ncj";
+val nnf_nim = thm "nnf_nim";
+val nnf_neq = thm "nnf_neq";
+val nnf_ndj = thm "nnf_ndj";
+
+fun decomp_cnnf lfnp P = 
+    case P of 
+	Const ("op &",_) $ p $q => ([p,q] , FWD qe_conjI )
+      | Const ("op |",_) $ p $q => ([p,q] , FWD qe_disjI)
+      | Const ("Not",_) $ (Const("Not",_) $ p) => ([p], FWD nnf_nn)
+      | Const("Not",_) $ (Const(opn,T) $ p $ q) => 
+	if opn = "op |" 
+	then 
+	    (case (p,q) of 
+		 (A as (Const ("op &",_) $ r $ s),B as (Const ("op &",_) $ r1 $ t)) =>
+		 if r1 = CooperDec.negate r 
+		 then  ([r,HOLogic.Not$s,r1,HOLogic.Not$t],
+			fn [th1_1,th1_2,th2_1,th2_2] => 
+			   [[th1_1,th1_1] MRS qe_conjI,[th2_1,th2_2] MRS qe_conjI] MRS nnf_sdj)
+		       
+		 else ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj)
+               | (_,_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ndj))
+	else (
+              case (opn,T) of 
+		  ("op &",_) => ([HOLogic.Not $ p,HOLogic.Not $ q ], FWD nnf_ncj )
+		| ("op -->",_) => ([p,HOLogic.Not $ q ], FWD nnf_nim )
+		| ("op =",Type ("fun",[Type ("bool", []),_])) => 
+		  ([HOLogic.conj $ p $ (HOLogic.Not $ q),HOLogic.conj $ (HOLogic.Not $ p) $ q], 
+		   FWD nnf_neq)
+		| (_,_) => ([], fn [] => lfnp P))
+      | (Const ("op -->",_) $ p $ q) => ([HOLogic.Not$p,q], FWD nnf_im)
+      | (Const ("op =", Type ("fun",[Type ("bool", []),_])) $ p $ q) =>
+	([HOLogic.conj $ p $ q,HOLogic.conj $ (HOLogic.Not $ p) $ (HOLogic.Not $ q) ], FWD nnf_eq )
+      | _ => ([], fn [] => lfnp P);
+
+fun nnfp afnp vs p = 
+    let val th = divide_and_conquer (decomp_cnnf (afnp vs)) p
+	val Pth = (Simplifier.rewrite 
+		       (HOL_basic_ss addsimps fr_simps addsimps [refl]) 
+		       (snd(Thm.dest_comb(snd(Thm.dest_comb (cprop_of th))))))
+		      RS meta_eq_to_obj_eq
+    in [th,Pth] MRS trans
+    end;
+
+
+    (* Normalization of arithmetical expressions *)
+val rzero = Const("0",rT);
+val rone = Const("1",rT);
+fun mk_real i = 
+    case i of 
+	0 => rzero
+      | 1 => rone
+      | _ => (HOLogic.number_of_const rT)$(HOLogic.mk_binum i); 
+
+fun dest_real (Const("0",_)) = 0
+  | dest_real (Const("1",_)) = 1
+  | dest_real (Const("Numeral.number_of",_)$b) = HOLogic.dest_binum b;
+
+	(* Normal form for terms is: 
+	 (c0*x0 + ... + cn*xn + k) / c , where ci!=0 and x0<..<xn ordered according to vs*)
+	(* functions to prove trivial properties about numbers *)
+fun proveq thy n m = prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(mk_real n,mk_real m));
+fun provenz thy n = 
+    prove_bysimp thy (simpset_of thy) (HOLogic.Not$(HOLogic.mk_eq(mk_real n,rzero)));
+
+fun proveprod thy m n = 
+    prove_bysimp thy (simpset_of thy) 
+		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.times" (mk_real m,mk_real n),mk_real (m*n)));
+fun proveadd thy m n = 
+    prove_bysimp thy (simpset_of thy) 
+		 (HOLogic.mk_eq(HOLogic.mk_binop "HOL.plus" (mk_real m,mk_real n),mk_real (m+n)));
+fun provediv thy m n = 
+    let val g = gcd (m,n) 
+	val m' = m div g
+	val n'= n div g
+    in
+	(prove_bysimp thy (simpset_of thy) 
+		     (HOLogic.mk_eq(HOLogic.mk_binop "HOL.divide" (mk_real m,mk_real n),
+				    HOLogic.mk_binop "HOL.divide" 
+						     (mk_real m',mk_real n'))),m')
+    end;
+		 (* Multiplication of a normal term by a constant *)
+val ncmul_congh = thm "ncmul_congh";
+val ncmul_cong = thm "ncmul_cong";
+fun decomp_ncmulh thy c t = 
+    if c = 0 then ([],fn _ => instantiate' [SOME crT] [SOME (cterm_of thy t)] mult_zero_left) else 
+    case t of 
+	Const("HOL.plus",_)$(Const("HOL.times",_)$c'$v)$b => 
+	([b],FWD (instantiate' [] [NONE, NONE, SOME (cterm_of thy v)] 
+			       ((proveprod thy c (dest_real c')) RS ncmul_congh)))
+      | _ => ([],fn _ => proveprod thy c (dest_real t));
+
+fun prove_ncmulh thy c = divide_and_conquer (decomp_ncmulh thy c);
+
+    (* prove_ncmul thy n t n = a theorem : "c*(t/n) = (t'/n')*)
+fun prove_ncmul thy c (t,m) = 
+    let val (eq1,c') = provediv thy c m
+	val tt' = prove_ncmulh thy c' t
+    in [eq1,tt'] MRS ncmul_cong
+    end;
+
+    (* prove_nneg returns "-(t/n) = t'/n'" ; normally t'=t and n' = -n*)
+val nneg_cong = thm "nneg_cong";
+fun prove_nneg thy (t,m) = (prove_ncmul thy ~1 (t, m)) RS nneg_cong;
+
+(* Addition of 2 expressions in normal form*)
+val naddh_cong_same = thm "naddh_cong_same";
+val naddh_cong_same0 = thm "naddh_cong_same0";
+val naddh_cong_ts = thm "naddh_cong_ts";
+val naddh_cong_st = thm "naddh_cong_st";
+
+fun earlier [] x y = false 
+  | earlier (h::t) x y =
+    if h = y then false 
+    else if h = x then true 
+    else earlier t x y ; 
+
+fun decomp_naddh thy vs (t,s) = 
+    case (t,s) of 
+	(Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr, 
+	 Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) =>
+	if tv = sv then 
+	    let val ntc = dest_real tc
+		val nsc = dest_real sc
+		val addth = proveadd thy ntc nsc
+	    in if ntc + nsc = 0 
+	       then ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
+						  (addth RS naddh_cong_same0)))
+	       else ([(tr,sr)], FWD (instantiate' [] [NONE,NONE,NONE,SOME (cterm_of thy tv)] 
+						  (addth RS naddh_cong_same)))
+	    end
+	else if earlier vs tv sv 
+	then ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
+	else ([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
+      | (Const("HOL.plus",_)$(ctv as Const("HOL.times",_)$tc$tv)$tr,_) => 
+	([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts))
+      | (_,Const("HOL.plus",_)$(csv as Const("HOL.times",_)$sc$sv)$sr) => 
+	([(t,sr)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy csv)] naddh_cong_st))
+      | (_,_) => ([], fn _ => proveadd thy (dest_real t) (dest_real s));
+
+    (* prove_naddh returns "t + s = t'*) 
+fun prove_naddh thy vs = divide_and_conquer (decomp_naddh thy vs);
+
+val nadd_cong_same = thm "nadd_cong_same";
+val nadd_cong = thm "nadd_cong";
+val plus_cong = thm "plus_cong";
+    (* prove_nadd resturns: "t/m + s/n = t'/m'"*)
+fun prove_nadd thy vs (t,m) (s,n) = 
+    if n=m then 
+	let val nm = proveq thy n m
+	    val ts = prove_naddh thy vs (t,s)
+	in [nm,ts] MRS nadd_cong_same
+	end
+    else let val l = lcm (m,n)
+	     val m' = l div m
+	     val n' = l div n
+	     val mml = proveprod thy m' m
+	     val nnl = proveprod thy n' n
+	     val mnz = provenz thy m
+	     val nnz = provenz thy n
+	     val lnz = provenz thy l
+	     val mt = prove_ncmulh thy m' t
+	     val ns = prove_ncmulh thy n' s
+	     val _$(_$_$t') = prop_of mt
+	     val _$(_$_$s') = prop_of ns
+	 in [mml,nnl,mnz,nnz,lnz,[mt,ns,prove_naddh thy vs (t',s')] MRS plus_cong] 
+		MRS nadd_cong
+	 end;
+
+    (* prove_nsub returns: "t/m - s/n = t'/m'"*)
+val nsub_cong = thm "nsub_cong";
+fun prove_nsub thy vs (t,m) (s,n) = 
+    let val nsm = prove_nneg thy (s,n)
+	val _$(_$_$(_$s'$n')) = prop_of nsm
+	val ts = prove_nadd thy vs (t,m) (s',dest_real n')
+    in [nsm,ts] MRS nsub_cong
+    end;
+
+val ndivide_cong = thm "ndivide_cong";
+fun prove_ndivide thy (t,m) n = instantiate' [] [SOME(cterm_of thy t)] 
+					     ((proveprod thy m n) RS ndivide_cong);
+
+exception FAILURE of string;
+
+val divide_cong = thm"divide_cong";
+val diff_cong = thm"diff_cong";
+val uminus_cong = thm"uminus_cong";
+val mult_cong = thm"mult_cong";
+val mult_cong2 = thm"mult_cong2";
+val normalizeh_var = thm "normalizeh_var";
+val nrefl = thm "nrefl";
+
+fun decomp_normalizeh thy vs t =
+    case t of
+	Free _ => ([], fn _ => instantiate' [] [SOME(cterm_of thy t)] normalizeh_var)
+      | Const("HOL.uminus",_)$a => 
+	([a], 
+	 fn [tha] => let val _$(_$_$(_$a'$n')) = prop_of tha
+			 in [tha,prove_nneg thy (a',dest_real n')] 
+				MRS uminus_cong
+			 end )
+      | Const("HOL.plus",_)$a$b => 
+	([a,b], 
+	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
+			     val _$(_$_$(_$b'$m')) = prop_of thb
+			 in [tha,thb,prove_nadd thy vs (a',dest_real n') (b',dest_real m')] 
+				MRS plus_cong
+			 end )
+      | Const("HOL.minus",_)$a$b => 
+	([a,b], 
+	 fn [tha,thb] => let val _$(_$_$(_$a'$n')) = prop_of tha
+			     val _$(_$_$(_$b'$m')) = prop_of thb
+			 in [tha,thb,prove_nsub thy vs (a',dest_real n') (b',dest_real m')] 
+				MRS diff_cong
+			 end )
+      | Const("HOL.times",_)$a$b => 
+	if can dest_real a 
+	then ([b], fn [thb] => 
+		      let val _$(_$_$(_$b'$m')) = prop_of thb
+		      in [thb, prove_ncmul thy (dest_real a) (b',dest_real m')] MRS mult_cong
+		      end )
+	else if can dest_real b
+	then ([a], fn [tha] => 
+		      let val _$(_$_$(_$a'$m')) = prop_of tha
+		      in [tha, prove_ncmul thy (dest_real b) (a',dest_real m')] MRS mult_cong2
+		      end )
+	else raise FAILURE "decomp_normalizeh: non linear term"
+      | Const("HOL.divide",_)$a$b => 
+	if can dest_real b
+	then ([a], fn [tha] => 
+		      let val _$(_$_$(_$a'$m')) = prop_of tha
+		      in [tha, prove_ndivide thy (a',dest_real m') (dest_real b)] MRS divide_cong
+		      end )
+	else raise FAILURE "decomp_normalizeh: non linear term"
+      | _ => ([], fn _ => instantiate' [] [SOME (cterm_of thy t)] nrefl);
+fun prove_normalizeh thy vs = divide_and_conquer (decomp_normalizeh thy vs);
+fun dest_xth vs th = 
+    let val _$(_$_$(_$t$n)) = prop_of th
+    in (case t of 
+	    Const("HOL.plus",_)$(Const("HOL.times",_)$c$y)$r => 
+	    if vs = [] then (0,t,dest_real n)
+	    else if hd vs = y then (dest_real c, r,dest_real n)
+	    else (0,t,dest_real n)
+	  | _ => (0,t,dest_real n))
+    end;
+
+fun prove_strictsign thy n = 
+    prove_bysimp thy (simpset_of thy) 
+		 (HOLogic.mk_binrel "Orderings.less" 
+				    (if n > 0 then (rzero, mk_real n) else (mk_real n, rzero))); 
+fun prove_fracsign thy (m,n) = 
+    let val mn = HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n)
+    in prove_bysimp thy (simpset_of thy) 
+		 (HOLogic.mk_binrel "Orderings.less" 
+				    (if m*n > 0 then (rzero, mn) else (mn, rzero)))
+    end; 
+
+fun holbool_of true = HOLogic.true_const
+  | holbool_of false = HOLogic.false_const;
+
+fun prove_fracsign_eq thy s (m,n) = 
+    let fun f s = the (AList.lookup (op =) [("Orderings.less", op <),("Orderings.less_eq", op <=),("op =", op =)] s)
+    in 
+    prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq
+		 (HOLogic.mk_binrel s 
+				    (HOLogic.mk_binop "HOL.divide" (mk_real m, mk_real n),rzero), 
+				    holbool_of (f s (m*n,0))))
+    end;
+
+fun proveq_eq thy n m = 
+    prove_bysimp thy (simpset_of thy) 
+		 (HOLogic.mk_eq 
+		      (HOLogic.mk_eq(mk_real n, mk_real m),holbool_of (n = m)));
+
+val sum_of_same_denoms = thm "sum_of_same_denoms";
+val sum_of_opposite_denoms = thm "sum_of_opposite_denoms";
+val trivial_sum_of_opposites = thm "trivial_sum_of_opposites";
+val normalize_ltground_cong = thm "normalize_ltground_cong";
+val normalize_ltnoxpos_cong = thm "normalize_ltnoxpos_cong";
+val normalize_ltnoxneg_cong = thm "normalize_ltnoxneg_cong";
+val normalize_ltxpos_cong = thm "normalize_ltxpos_cong";
+val normalize_ltxneg_cong = thm "normalize_ltxneg_cong";
+
+val normalize_leground_cong = thm "normalize_leground_cong";
+val normalize_lenoxpos_cong = thm "normalize_lenoxpos_cong";
+val normalize_lenoxneg_cong = thm "normalize_lenoxneg_cong";
+val normalize_lexpos_cong = thm "normalize_lexpos_cong";
+val normalize_lexneg_cong = thm "normalize_lexneg_cong";
+
+val normalize_eqground_cong = thm "normalize_eqground_cong";
+val normalize_eqnox_cong = thm "normalize_eqnox_cong";
+val normalize_eqxpos_cong = thm "normalize_eqxpos_cong";
+val normalize_eqxneg_cong = thm "normalize_eqxneg_cong";
+
+val normalize_not_lt = thm "normalize_not_lt";
+val normalize_not_le = thm "normalize_not_le";
+val normalize_not_eq = thm "normalize_not_eq";
+
+fun prove_normalize thy vs at = 
+    case at of 
+	Const("Orderings.less",_)$s$t => 
+	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+	    val (cx,r,n) = dest_xth vs smtth
+	in if cx = 0 then if can dest_real r 
+			  then [smtth, prove_fracsign_eq thy "Orderings.less" (dest_real r, n)]
+				   MRS normalize_ltground_cong
+			  else [smtth, prove_strictsign thy n] 
+				   MRS (if n > 0 then normalize_ltnoxpos_cong 
+					else normalize_ltnoxneg_cong)
+	   else let val srn = prove_fracsign thy (n,cx)
+		    val rr' = if cx < 0 
+			      then instantiate' [] [SOME (cterm_of thy r)]
+						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
+			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
+						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
+							   RS sum_of_same_denoms)
+		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_ltxneg_cong 
+					else normalize_ltxpos_cong)
+		end
+	end
+      | Const("Orderings.less_eq",_)$s$t => 
+	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+	    val (cx,r,n) = dest_xth vs smtth
+	in if cx = 0 then if can dest_real r 
+			  then [smtth, prove_fracsign_eq thy "Orderings.less_eq" (dest_real r, n)]
+				   MRS normalize_leground_cong
+			  else [smtth, prove_strictsign thy n] 
+				   MRS (if n > 0 then normalize_lenoxpos_cong 
+					else normalize_lenoxneg_cong)
+	   else let val srn = prove_fracsign thy (n,cx)
+		    val rr' = if cx < 0 
+			      then instantiate' [] [SOME (cterm_of thy r)]
+						((proveadd thy cx (~cx)) RS sum_of_opposite_denoms)
+			      else instantiate' [] [SOME (cterm_of thy (mk_real cx))] 
+						(((prove_ncmulh thy ~1 r) RS nneg_cong) 
+							   RS sum_of_same_denoms)
+		in [smtth,srn,rr'] MRS (if n*cx < 0 then normalize_lexneg_cong 
+					else normalize_lexpos_cong)
+		end
+	end
+      | Const("op =",_)$s$t => 
+	let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop "HOL.minus" (s,t))
+	    val (cx,r,n) = dest_xth vs smtth
+	in if cx = 0 then if can dest_real r 
+			  then [smtth, provenz thy n, 
+				proveq_eq thy (dest_real r) 0]
+				   MRS normalize_eqground_cong
+			  else [smtth, provenz thy n] 
+				   MRS normalize_eqnox_cong
+	   else let val scx = prove_strictsign thy cx
+		    val nnz = provenz thy n
+		    val rr' = if cx < 0 
+			      then proveadd thy cx (~cx)
+			      else ((prove_ncmulh thy ~1 r) RS nneg_cong) 
+				       RS trivial_sum_of_opposites
+		in [smtth,scx,nnz,rr'] MRS (if cx < 0 then normalize_eqxneg_cong 
+					else normalize_eqxpos_cong)
+		end
+	end
+      | Const("Not",_)$(Const("Orderings.less",T)$s$t) => 
+	(prove_normalize thy vs (Const("Orderings.less_eq",T)$t$s)) RS normalize_not_lt
+      | Const("Not",_)$(Const("Orderings.less_eq",T)$s$t) => 
+	(prove_normalize thy vs (Const("Orderings.less",T)$t$s)) RS normalize_not_le
+      | (nt as Const("Not",_))$(Const("op =",T)$s$t) => 
+	(prove_normalize thy vs (Const("op =",T)$s$t)) RS qe_Not
+      | _ => instantiate' [SOME cbT] [SOME (cterm_of thy at)] refl;
+
+     (* Generic quantifier elimination *)
+
+
+val qe_ex_conj = thm "qe_ex_conj";
+val qe_ex_nconj = thm "qe_ex_nconj";
+val qe_ALL = thm "qe_ALL";
+val ex_eq_cong = thm "ex_eq_cong";
+
+fun decomp_genqelim thy afnp nfnp qfnp (P,vs) = 
+    case P of
+	(Const("op &",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_conjI)
+      | (Const("op |",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_disjI)
+      | (Const("op -->",_)$A$B) => ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_impI)
+      | (Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => 
+	([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
+      | (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
+      | (Const("Ex",_)$Abs(xn,xT,p)) => 
+	let val (xn1,p1) = variant_abs(xn,xT,p)
+	    val x= Free(xn1,xT)
+	in ([(p1,x::vs)],
+            fn [th1_1] => 
+               let val th2 = [th1_1,nfnp (x::vs) (snd (CooperProof.qe_get_terms th1_1))] MRS trans
+		   val eth1 = (forall_intr (cterm_of thy (Free(xn1,xT))) th2) COMP  ex_eq_cong
+		   val th3 = qfnp (snd(CooperProof.qe_get_terms eth1))
+               in [eth1,th3] MRS trans
+               end )
+	end
+      | (Const("All",_)$Abs(xn,xT,p)) => 
+	([((HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p),vs)], fn [th] => th RS qe_ALL)
+      | _ => ([], fn [] => afnp vs P);
+
+val fr_prepqelim = thms "fr_prepqelim";
+val prepare_qelim_ss = HOL_basic_ss 
+			   addsimps simp_thms 
+			   addsimps (List.take(ex_simps,4))
+			   addsimps fr_prepqelim
+			   addsimps [not_all,ex_disj_distrib];
+
+fun prove_genqelim thy afnp nfnp qfnp P = 
+    let val thP = (Simplifier.rewrite prepare_qelim_ss P) RS meta_eq_to_obj_eq
+	val _$(_$_$P') = prop_of thP
+	val vs = term_frees P'
+	val qeth = divide_and_conquer (decomp_genqelim thy afnp nfnp qfnp) (Pattern.eta_long [] P',vs)
+	val _$(_$_$p'') = prop_of qeth
+	val thp' = nfnp vs p''
+    in [[thP, qeth] MRS trans, thp'] MRS trans
+    end;
+
+fun qelim P =
+  let val {thy, ...} = Thm.rep_cterm P
+  in prove_genqelim thy (prove_normalize thy) (nnfp (prove_normalize thy)) (ferrack_eq thy) P end;
+
+
+    (* Just for testing!! *)
+(*
+val thy = the_context();
+fun parseb s = term_of (read_cterm thy (s,HOLogic.boolT));
+fun parser s = term_of (read_cterm thy (s,rT));
+val fm = parseb "(x::real) < y + t & (y - 5 < x | 34 < y + t) & (x = s + 3*y) | (x ~= y - s)";
+
+provediv thy 4 2;
+provediv thy ~4 2;
+provediv thy 4 ~2;
+provediv thy 44 32;
+provediv thy ~34 20000;
+provediv thy ~4000000 ~27676;
+
+val vs = [Free("x",rT),Free("y",rT),Free("z",rT)] ;
+prove_nsub thy vs
+		    (parser "4*(x::real) + (3*y + 5)" ,54) (parser "3*(y::real) + (4*z + 5)",9);
+
+prove_ndivide thy (parser "4*(x::real) + (3*y + 5)" ,5) 4;
+prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
+		    (parser "4*(x::real) + 3* ((3*y + 5) + x)");
+prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
+		    (parser "4*(x::real) - 3* ((3*y + 5)*9 + x)");
+prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
+		    (parser "- x");
+prove_normalizeh thy [Free("x",rT),Free("y",rT),Free("z",rT)] 
+		    (parser "4*(x::real) +3* ((3*y + 5) / 3 - (- x))");
+
+
+
+
+
+
+fun test xn s = ferrack_eq thy (parseb ("EX (" ^ xn ^ "::real)." ^ s));
+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)";
+test "x" "(x::real) < y + t & y - 5 < x & (x ~= y - s)";
+test "x" "(x::real) < y + t";
+test "x" "(x::real) > y + t";
+test "x" "(x::real) = y + t";
+test "x" "(x::real) ~= y + t";
+test "x" "34 < y + (t::real)";
+test "x" "(x::real) ~= y + t & 34 < y + (t::real)";
+test "x" "(x::real) ~= y + t & (x::real) < y + t";
+
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= 3*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 "); 
+
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < 3*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < (-1)*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 "); 
+
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = 3*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = (-1)*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 = x + 3 + 4* (y - 15*z) / 3 "); 
+
+prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + y)"); 
+prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= 3*x + y)"); 
+prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= (-1)*x + y)"); 
+prove_normalize thy vs (parseb "~ ((x::real) + 4* (y - 15*z) / 3 <= x + 3 + 4* (y - 15*z) / 3 )"); 
+
+prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + y)"); 
+prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < 3*x + y)"); 
+prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < (-1)*x + y)"); 
+prove_normalize thy vs (parseb "~((x::real) + 4* (y - 15*z) / 3 < x + 3 + 4* (y - 15*z) / 3 )"); 
+
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= 3*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= (-1)*x + y"); 
+prove_normalize thy vs (parseb "(x::real) + 4* (y - 15*z) / 3 ~= x + 3 + 4* (y - 15*z) / 3 "); 
+
+
+nnfp (prove_normalize thy) vs
+     (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)))");
+nnfp (prove_normalize thy) vs
+     (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)))");
+
+fun frtest s = frqelim thy (read_cterm thy (s,HOLogic.boolT));
+frtest "~ (ALL (x::real) y. x < y --> 10*x < 11*y)";
+frtest "ALL (x::real) y. x < y --> (10*(x + 5*y + -1) < 60*y)";
+frtest "EX (x::real) y. x ~= y --> x < y";
+frtest "EX (x::real) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y";
+frtest "ALL (x::real) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y";
+*)
+  (* 1 Alternations *)
+(*
+frtest "ALL (x::real). (EX (y::real). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)";
+frtest "ALL (x::real) < 0. (EX (y::real) > 0. 7*x + y > 0 & x - y <= 9)";
+frtest "EX (x::real). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)";
+frtest "EX (x::real). 0 < x & x < 1 & (ALL y. (1 < y & y < 2) --> (1 < 2*(y - x) & 2*(y - x) <3))";
+frtest "ALL (x::real). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)";
+*)
+    (* Formulae with 3 quantifiers *)
+  (* 0 Alternations *)
+(*
+frtest "ALL (x::real) y z. x + y < z --> y >= z --> x < 0";
+frtest "EX (x::real) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0";
+frtest "ALL (x::real) y z. abs (x + y) <= z --> (abs z = z)";
+frtest "EX (x::real) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0";
+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))";
+*)
+  (* 1 Alternations *)
+(*
+frtest "ALL (x::real) y. x < y --> (EX z>0. x+z = y)";
+frtest "ALL (x::real) y. (EX z>0. abs (x - y) <= z )";
+frtest "EX (x::real) y. (ALL z>0. (z < x --> z <= 5) & (z > y --> z >= x))";
+frtest "EX (x::real) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))";
+frtest "EX (x::real) y. (ALL z>0. abs (3*x - 7*y) >= 5 & abs (3*x+7*y) <= 2*z + 1)";
+*)
+  (* 2 Alternations *)
+(*
+frtest "EX (x::real)>0. (ALL y >0. (EX z>7. 5*x - 3*y <= 7*z))";
+frtest "EX (x::real). abs x < 4 & (ALL y > 0. (EX z. 5*x - 3*y <= 7*z))";
+frtest "ALL (x::real). (EX y > x. (ALL z < y. x+z < 2*y))" ;
+frtest "ALL (x::real). (EX y<(3*x - 1). (ALL z >= (3*x - 1). x - y + z > x ))" ;
+frtest "EX (x::real). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))";
+*)
+    (* Formulae with 4 quantifiers *)
+    (* 0 Alternations *)
+(*
+frtest "ALL (x::real) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y";
+frtest "ALL (x::real) y. ALL z >x. ALL w > y. abs (z-x) + abs (y-w + x) <= z - x + w-y+abs x";
+frtest "EX (x::real) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89";
+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)";
+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)";
+*)
+    (* 1 Alternations *)
+(*
+frtest "ALL (x::real) y z. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z)";
+frtest "ALL (x::real). (EX y z w. x< y & x < z & x> w & 3*x < w + y)";
+frtest "ALL (x::real) y. (EX z w. abs (x-y) = abs (z-w) & z < x & w ~= y)";
+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))";
+frtest "EX (x::real) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)";
+*)
+    (* 2 Alternations *)
+(*
+frtest "EX z. (ALL (x::real) y. (EX w >= abs (x+y+z). w <= abs x + abs y + abs z))";
+frtest "EX z. (ALL (x::real) < z. (EX y w. x< y & x < z & x> w & 3*x < w + y))";
+frtest "ALL (x::real) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))";
+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)))";
+frtest "EX (x::real) z. (ALL w >= abs (x+z). (EX y. w >= abs x + abs y + abs z))";
+*)
+    (* 3 Alternations *)
+(*
+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)))";
+frtest "EX (x::real). (ALL y < 3*x. (EX z > max x y. 
+  (ALL w . abs w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))";
+frtest "ALL (x::real). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))";
+frtest "ALL (x::real). (EX y. (ALL z>19. abs (y) <= abs (x + z) & (EX w. abs (x + z) < w - y)))";
+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)))";
+*)
+end