# HG changeset patch
# User nipkow
# Date 916069849 -3600
# Node ID 4f7975c74cdfa56c62a840018736892264e9803e
# Parent  e01e2328d0f0a1b15e20420ffbf691fb731476fb
More arith simplifications.

diff -r e01e2328d0f0 -r 4f7975c74cdf src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Arith.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -855,12 +855,11 @@
 val not_lessD = leI;
 val sym = sym;
 
-fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
+val mk_Eq = mk_eq;
 val mk_Trueprop = HOLogic.mk_Trueprop;
 
-fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
-  | neg_prop(TP$t) =
-      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
+fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
+  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
 
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
diff -r e01e2328d0f0 -r 4f7975c74cdf src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -412,7 +412,7 @@
 
 val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
 val neg_prop = Nat_LA_Data.neg_prop;
-val mkEqTrue = Nat_LA_Data.mkEqTrue;
+val mk_Eq = Nat_LA_Data.mk_Eq;
 
 val intT = Type("IntDef.int",[]);
 
diff -r e01e2328d0f0 -r 4f7975c74cdf src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Integ/IntDef.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -149,7 +149,6 @@
 
 Goalw [neg_def, int_def] "~ neg(int n)";
 by (Simp_tac 1);
-by Safe_tac;
 qed "not_neg_nat";
 
 Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
diff -r e01e2328d0f0 -r 4f7975c74cdf src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Lambda/Eta.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -28,9 +28,8 @@
 
 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
 by (induct_tac "t" 1);
-by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
-by(Auto_tac);
-by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
+  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
+ by(nat_arith_tac 1);
 by(Auto_tac);
 qed "free_lift";
 Addsimps [free_lift];
@@ -170,7 +169,6 @@
   by (etac thin_rl 1);
   by (exhaust_tac "t" 1);
     by (Asm_simp_tac 1);
-    by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    by (Asm_simp_tac 1);
   by (Asm_simp_tac 1);
  by (Asm_simp_tac 1);
diff -r e01e2328d0f0 -r 4f7975c74cdf src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -27,9 +27,9 @@
   val sym:		thm (* x = y ==> y = x *)
   val decomp: term ->
              ((term * int)list * int * string * (term * int)list * int)option
-  val mkEqTrue: thm -> thm
+  val mk_Eq: thm -> thm
   val mk_Trueprop: term -> term
-  val neg_prop: term -> term * bool
+  val neg_prop: term -> term
   val simp: thm -> thm
   val is_False: thm -> bool
   val is_nat: typ list * term -> bool
@@ -41,12 +41,13 @@
          p/q is the decomposition of the sum terms x/y into a list
          of summand * multiplicity pairs and a constant summand.
 
-mkEqTrue(P) = `P == True'
+mk_Eq(~in) = `in == False'
+mk_Eq(in) = `in == True'
+where `in' is an (in)equality.
 
-neg_prop(t) = (nt,neg) if t is wrapped up in Trueprop and
+neg_prop(t) = neg if t is wrapped up in Trueprop and
   nt is the (logically) negated version of t, where the negation
   of a negative term is the term itself (no double negation!);
-  neg = `t is already negated'.
 
 simp must reduce contradictory <= to False.
    It should also cancel common summands to keep <= reduced;
@@ -360,17 +361,17 @@
 
 fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i;
 
-fun prover1(just,sg,thms,concl) =
-let val (nconcl,neg) = LA_Data.neg_prop concl
+fun prover1(just,sg,thms,concl,pos) =
+let val nconcl = LA_Data.neg_prop concl
     val cnconcl = cterm_of sg nconcl
     val Fthm = mkthm sg (thms @ [assume cnconcl]) just
-    val contr = if neg then LA_Data.notI else LA_Data.ccontr
-in Some(LA_Data.mkEqTrue ((implies_intr cnconcl Fthm) COMP contr)) end
+    val contr = if pos then LA_Data.ccontr else LA_Data.notI
+in Some(LA_Data.mk_Eq ((implies_intr cnconcl Fthm) COMP contr)) end
 handle _ => None;
 
 (* handle thm with equality conclusion *)
 fun prover2(just1,just2,sg,thms,concl) =
-let val (nconcl,_) = LA_Data.neg_prop concl (* m ~= n *)
+let val nconcl = LA_Data.neg_prop concl (* m ~= n *)
     val cnconcl = cterm_of sg nconcl
     val neqthm = assume cnconcl
     val casethm = neqthm COMP LA_Data.neqE (* [|m<n ==> R; n<m ==> R|] ==> R *)
@@ -382,17 +383,22 @@
     and thm2 = mkthm sg (thms @ [assume cless2]) just2
     val dthm1 = implies_intr cless1 thm1 and dthm2 = implies_intr cless2 thm2
     val thm = dthm2 COMP (dthm1 COMP casethm)
-in Some(LA_Data.mkEqTrue ((implies_intr cnconcl thm) COMP LA_Data.ccontr)) end
+in Some(LA_Data.mk_Eq ((implies_intr cnconcl thm) COMP LA_Data.ccontr)) end
 handle _ => None;
 
-(* FIXME: forward proof of equalities missing! *)
+(* PRE: concl is not negated! *)
 fun lin_arith_prover sg thms concl =
 let val Hs = map (#prop o rep_thm) thms
     val Tconcl = LA_Data.mk_Trueprop concl
 in case prove([],Hs,Tconcl) of
-     [j] => prover1(j,sg,thms,Tconcl)
+     [j] => prover1(j,sg,thms,Tconcl,true)
    | [j1,j2] => prover2(j1,j2,sg,thms,Tconcl)
-   | _ => None
+   | _ => let val nTconcl = LA_Data.neg_prop Tconcl
+          in case prove([],Hs,nTconcl) of
+               [j] => prover1(j,sg,thms,nTconcl,false)
+               (* [_,_] impossible because of negation *)
+             | _ => None
+          end
 end;
 
 end;