| author | wenzelm |
| Thu, 21 Jun 2007 15:42:07 +0200 | |
| changeset 23454 | c54975167be9 |
| parent 23453 | bf46f5cbdd64 |
| child 23455 | e18a371624b5 |
| src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy | file | annotate | diff | comparison | revisions | |
| src/HOL/Complex/ex/ROOT.ML | file | annotate | diff | comparison | revisions | |
| src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions | |
| src/HOL/Real/Ferrante_Rackoff.thy | file | annotate | diff | comparison | revisions | |
| src/HOL/Real/Real.thy | file | annotate | diff | comparison | revisions | |
| src/HOL/Real/ferrante_rackoff.ML | file | annotate | diff | comparison | revisions | |
| src/HOL/Real/ferrante_rackoff_proof.ML | file | annotate | diff | comparison | revisions | |
| src/HOL/ex/Dense_Linear_Order_Ex.thy | file | annotate | diff | comparison | revisions | |
| src/HOL/ex/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Complex/ex/Ferrante_Rackoff_Ex.thy Thu Jun 21 15:42:06 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,169 +0,0 @@ -(* - 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 Thu Jun 21 15:42:06 2007 +0200 +++ b/src/HOL/Complex/ex/ROOT.ML Thu Jun 21 15:42:07 2007 +0200 @@ -21,8 +21,6 @@ no_document use_thy "NatPair"; use_thy "DenumRat"; -use_thy "Ferrante_Rackoff_Ex"; - if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *) else use_thy "MIR";
--- a/src/HOL/IsaMakefile Thu Jun 21 15:42:06 2007 +0200 +++ b/src/HOL/IsaMakefile Thu Jun 21 15:42:07 2007 +0200 @@ -82,31 +82,32 @@ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML \ - $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML \ - ATP_Linkup.thy Accessible_Part.thy Datatype.thy \ - Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy \ - FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \ - Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy \ - List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy \ - Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ - Predicate.thy Presburger.thy Product_Type.thy ROOT.ML Recdef.thy \ + $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ + Accessible_Part.thy Datatype.thy Dense_Linear_Order.thy Divides.thy \ + Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy \ + Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy \ + IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy Main.thy \ + Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy \ + OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy \ + Presburger.thy Product_Type.thy ROOT.ML Recdef.thy \ Record.thy Refute.thy Relation.thy Relation_Power.thy \ Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \ Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \ + Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML \ + Tools/Ferrante_Rackoff/ferrante_rackoff.ML \ Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer.ML Groebner_Basis.thy \ Tools/Groebner_Basis/normalizer_data.ML \ Tools/Presburger/cooper.ML Tools/Presburger/presburger.ML \ - Tools/Presburger/qelim.ML Tools/Presburger/generated_cooper.ML \ - Tools/Presburger/cooper_data.ML Tools/TFL/dcterm.ML \ - Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML \ - Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML \ - Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \ - Tools/datatype_aux.ML Tools/datatype_case.ML \ - Tools/datatype_codegen.ML Tools/datatype_hooks.ML \ - Tools/datatype_package.ML Tools/datatype_prop.ML \ - Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \ - Tools/function_package/auto_term.ML \ + Tools/Presburger/generated_cooper.ML Tools/Presburger/cooper_data.ML \ + Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML \ + Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML \ + Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML \ + Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ + Tools/datatype_case.ML Tools/datatype_codegen.ML \ + Tools/datatype_hooks.ML Tools/datatype_package.ML \ + Tools/datatype_prop.ML Tools/datatype_realizer.ML \ + Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \ Tools/function_package/context_tree.ML \ Tools/function_package/fundef_common.ML \ Tools/function_package/fundef_core.ML \ @@ -121,11 +122,12 @@ Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \ Tools/metis_tools.ML Tools/numeral_syntax.ML \ Tools/old_inductive_package.ML Tools/polyhash.ML \ - Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML \ - Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML \ - Tools/refute_isar.ML Tools/res_atp.ML Tools/res_atp_methods.ML \ - Tools/res_atp_provers.ML Tools/res_atpset.ML Tools/res_axioms.ML \ - Tools/res_clause.ML Tools/res_hol_clause.ML Tools/res_reconstruct.ML \ + Tools/primrec_package.ML Tools/prop_logic.ML Tools/qelim.ML \ + Tools/recdef_package.ML Tools/recfun_codegen.ML \ + Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \ + Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \ + Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \ + Tools/res_hol_clause.ML Tools/res_reconstruct.ML \ Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \ Tools/specification_package.ML Tools/split_rule.ML \ Tools/string_syntax.ML Tools/typecopy_package.ML \ @@ -159,11 +161,10 @@ $(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \ Library/Zorn.thy \ - Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/float_arith.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/RealVector.thy Real/ferrante_rackoff_proof.ML \ - Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML \ + Real/ContNotDenum.thy Real/float_arith.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/RealVector.thy 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 \ @@ -190,7 +191,6 @@ $(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/Ferrante_Rackoff_Ex.thy \ Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \ Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \ Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML @@ -400,7 +400,7 @@ MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \ MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \ MetisExamples/set.thy - @$(ISATOOL) usedir -g true $(OUT)/HOL MetisExamples + @$(ISATOOL) usedir $(OUT)/HOL MetisExamples ## HOL-Algebra @@ -649,7 +649,7 @@ $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ ex/BT.thy ex/BinEx.thy ex/CTL.thy \ - ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \ + ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \ ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \ ex/Codegenerator.thy ex/Codegenerator_Rat.thy \ ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
--- a/src/HOL/Real/Ferrante_Rackoff.thy Thu Jun 21 15:42:06 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,544 +0,0 @@ -(* - ID: $Id$ - Author: Amine Chaieb, TU Muenchen -*) - -header {* 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 - -lemma qe_Not: "P = Q ==> (~P) = (~Q)" -by blast - -lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)" -by blast - -lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)" -by blast - -lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)" -by blast - -lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)" -by blast - -lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)" -by blast -lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" - by iprover - -lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))" - by iprover - -lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))" -by blast - -lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))" -by blast - -lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)" - by blast -lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))" -by blast - -lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))" -by blast -lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))" -by blast -lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))" -by blast -lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))" -by blast -lemma qe_ex_conj: "(EX (x::int). A x) = R - ==> (EX (x::int). P x) = (Q & (EX x::int. A x)) - ==> (EX (x::int). P x) = (Q & R)" -by blast - -lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q) - ==> (EX (x::int). P x) = Q" -by blast - - - -use "ferrante_rackoff_proof.ML" -use "ferrante_rackoff.ML" -setup "Ferrante_Rackoff.setup" - -end
--- a/src/HOL/Real/Real.thy Thu Jun 21 15:42:06 2007 +0200 +++ b/src/HOL/Real/Real.thy Thu Jun 21 15:42:07 2007 +0200 @@ -2,6 +2,6 @@ (* $Id$ *) theory Real -imports ContNotDenum Ferrante_Rackoff RealVector +imports ContNotDenum RealVector begin end
--- a/src/HOL/Real/ferrante_rackoff.ML Thu Jun 21 15:42:06 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,100 +0,0 @@ -(* - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Ferrante and Rackoff Algorithm. -*) - -signature FERRANTE_RACKOFF = -sig - val ferrack_tac: bool -> int -> tactic - val setup: theory -> theory - val trace: bool ref -end; - -structure Ferrante_Rackoff : FERRANTE_RACKOFF = -struct - -val trace = ref false; -fun trace_msg s = if !trace then tracing s else (); - -val binarith = map thm ["Pls_0_eq", "Min_1_eq", "pred_Pls", "pred_Min","pred_1","pred_0", - "succ_Pls", "succ_Min", "succ_1", "succ_0", - "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10", "add_BIT_11", - "minus_Pls", "minus_Min", "minus_1", "minus_0", - "mult_Pls", "mult_Min", "mult_1", "mult_0", - "add_Pls_right", "add_Min_right"]; - -val comp_arith = binarith @ arith_simps @ simp_thms - -fun prepare_for_linr 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 np = length ps; - val (fm', np) = Library.foldr mk_all (ps, (Library.foldr HOLogic.mk_imp (rhs, c), np)); - val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT) - (term_frees fm' @ term_vars fm'); - val fm2 = Library.foldr mk_all2 (vs, fm'); - in (fm2, np + length vs, length rhs) end; - -fun spec_step n th = if n = 0 then th else spec_step (n - 1) th RS spec ; -fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp; - -val context_ss = simpset_of (the_context ()); - -fun ferrack_tac q i = ObjectLogic.atomize_tac i - THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i) - THEN (fn st => - let - val g = nth (prems_of st) (i - 1) - val thy = Thm.theory_of_thm st - (* Transform the term*) - val (t,np,nh) = prepare_for_linr q g - (* Some simpsets for dealing with mod div abs and nat*) - val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}] - (* simp rules for elimination of abs *) - val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}] - val ct = cterm_of thy (HOLogic.mk_Trueprop t) - (* Theorem for the nat --> int transformation *) - val pre_thm = Seq.hd (EVERY - [simp_tac simpset0 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 thy (Pattern.eta_long [] t1)) - in - (trace_msg ("calling procedure with term:\n" ^ - Sign.string_of_term thy 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); - -val ferrack_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 => K (Method.SIMPLE_METHOD' (ferrack_tac q))) - end; - -val setup = - Method.add_method ("ferrack", ferrack_meth, - "LCF-proof-producing decision procedure for linear real arithmetic"); - -end;
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Thu Jun 21 15:42:06 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,824 +0,0 @@ -(* - 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 bool}; -val rT = @{typ RealDef.real}; -val crT = @{ctyp RealDef.real}; - -(* Normalization*) - - - (* Computation of uset *) -fun uset x fm = - case fm of - Const("op &",_)$p$q => fold (insert (op =)) (uset x p) (uset x q) - | Const("op |",_)$p$q => fold (insert (op =)) (uset x p) (uset x q) - | Const(@{const_name Orderings.less},_)$s$t => if s=x then [t] - else if t = x then [s] - else [] - | Const(@{const_name 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 = @{typ "RealDef.real set"}; - -fun holrealset [] = @{term "{} :: RealDef.real set"} - | holrealset (x::xs) = @{term "insert :: RealDef.real => RealDef.real set => RealDef.real set"} - $ x $ holrealset xs; -fun prove_bysimp thy ss t = Goal.prove (ProofContext.init 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 (Const ("Finite_Set.finite", rsT --> HOLogic.boolT) $ hU) - 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(@{const_name 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(@{const_name 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) = Syntax.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 negate (Const ("Not",_) $ p) = p - |negate p = (HOLogic.Not $ p); - -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 = 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 = HOLogic.mk_number rT 0; -val rone = HOLogic.mk_number rT 1; -fun mk_real i = HOLogic.mk_number rT i; -val dest_real = snd o HOLogic.dest_number; - - (* 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 @{const_name 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 @{const_name HOL.plus} (mk_real m,mk_real n),mk_real (m+n))); -fun provediv thy m n = - let val g = Integer.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 @{const_name HOL.divide} (mk_real m,mk_real n), - HOLogic.mk_binop @{const_name 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)] @{thm mult_zero_left}) else - case t of - Const(@{const_name HOL.plus},_)$(Const(@{const_name 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(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr, - Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name 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(@{const_name HOL.plus},_)$(ctv as Const(@{const_name HOL.times},_)$tc$tv)$tr,_) => - ([(tr,s)],FWD (instantiate' [] [NONE,NONE,NONE,SOME(cterm_of thy ctv)] naddh_cong_ts)) - | (_,Const(@{const_name HOL.plus},_)$(csv as Const(@{const_name 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 = Integer.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(@{const_name 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(@{const_name 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(@{const_name 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(@{const_name 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(@{const_name 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(@{const_name HOL.plus},_)$(Const(@{const_name 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 @{const_name 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 @{const_name HOL.divide} (mk_real m, mk_real n) - in prove_bysimp thy (simpset_of thy) - (HOLogic.mk_binrel @{const_name 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 =) [(@{const_name Orderings.less}, op <),(@{const_name Orderings.less_eq}, op <=),("op =", op =)] s) - in - prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq - (HOLogic.mk_binrel s - (HOLogic.mk_binop @{const_name 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(@{const_name Orderings.less},_)$s$t => - let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name 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 @{const_name 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(@{const_name Orderings.less_eq},_)$s$t => - let val smtth = prove_normalizeh thy vs (HOLogic.mk_binop @{const_name 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 @{const_name 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 @{const_name 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(@{const_name Orderings.less},T)$s$t) => - (prove_normalize thy vs (Const(@{const_name Orderings.less_eq},T)$t$s)) RS normalize_not_lt - | Const("Not",_)$(Const(@{const_name Orderings.less_eq},T)$s$t) => - (prove_normalize thy vs (Const(@{const_name 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 get_terms th = -let - val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = - prop_of th -in (A,B) end; - -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) = Syntax.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 (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(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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Dense_Linear_Order_Ex.thy Thu Jun 21 15:42:07 2007 +0200 @@ -0,0 +1,156 @@ +(* + ID: $Id$ + Author: Amine Chaieb, TU Muenchen +*) + +header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} + +theory Dense_Linear_Order_Ex +imports Main +begin + +lemma + "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> x - y >0" + by dlo + +lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" + by dlo + +lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \<le> 0 )" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) 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))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \<noteq> abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). 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))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" + by dlo + +lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" + by dlo + +lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" + by dlo + +lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" + by dlo + +lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). + (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y. + (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" + by dlo + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" + by dlo + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" + by dlo + +end
--- a/src/HOL/ex/ROOT.ML Thu Jun 21 15:42:06 2007 +0200 +++ b/src/HOL/ex/ROOT.ML Thu Jun 21 15:42:07 2007 +0200 @@ -48,6 +48,7 @@ time_use_thy "CTL"; time_use_thy "mesontest2"; time_use_thy "Arith_Examples"; +time_use_thy "Dense_Linear_Order_Ex"; time_use_thy "PresburgerEx"; if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *) else time_use_thy "Reflected_Presburger";