Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bug in plusinf and mininf for the oracle fixed.
authorchaieb
Wed, 27 Apr 2005 11:49:20 +0200
changeset 15859 7bc8b9683224
parent 15858 d9f0c8580c0c
child 15860 a344c4284972
bug in plusinf and mininf for the oracle fixed.
src/HOL/Integ/cooper_dec.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/cooper_dec.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
@@ -323,8 +323,11 @@
 	 				 else fm 
  
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
-  )) => 
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	          else error "minusinf : term not in normal form!!!"
+	else fm
 	 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
@@ -341,8 +344,11 @@
 	 				 else fm
 
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
-  )) =>
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else error "plusinf : term not in normal form!!!"
+	else fm 
 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
@@ -323,8 +323,11 @@
 	 				 else fm 
  
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
-  )) => 
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	          else error "minusinf : term not in normal form!!!"
+	else fm
 	 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
@@ -341,8 +344,11 @@
 	 				 else fm
 
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
-  )) =>
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else error "plusinf : term not in normal form!!!"
+	else fm 
 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)
isabelle