More arith simplifications.
authornipkow
Mon Jan 11 16:50:49 1999 +0100 (1999-01-11)
changeset 60794f7975c74cdf
parent 6078 e01e2328d0f0
child 6080 0a2798ea600c
More arith simplifications.
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/IntDef.ML
src/HOL/Lambda/Eta.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Jan 11 12:52:53 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Jan 11 16:50:49 1999 +0100
     1.3 @@ -855,12 +855,11 @@
     1.4  val not_lessD = leI;
     1.5  val sym = sym;
     1.6  
     1.7 -fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
     1.8 +val mk_Eq = mk_eq;
     1.9  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.10  
    1.11 -fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
    1.12 -  | neg_prop(TP$t) =
    1.13 -      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
    1.14 +fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
    1.15 +  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
    1.16  
    1.17  (* Turn term into list of summand * multiplicity plus a constant *)
    1.18  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
     2.1 --- a/src/HOL/Integ/Bin.ML	Mon Jan 11 12:52:53 1999 +0100
     2.2 +++ b/src/HOL/Integ/Bin.ML	Mon Jan 11 16:50:49 1999 +0100
     2.3 @@ -412,7 +412,7 @@
     2.4  
     2.5  val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
     2.6  val neg_prop = Nat_LA_Data.neg_prop;
     2.7 -val mkEqTrue = Nat_LA_Data.mkEqTrue;
     2.8 +val mk_Eq = Nat_LA_Data.mk_Eq;
     2.9  
    2.10  val intT = Type("IntDef.int",[]);
    2.11  
     3.1 --- a/src/HOL/Integ/IntDef.ML	Mon Jan 11 12:52:53 1999 +0100
     3.2 +++ b/src/HOL/Integ/IntDef.ML	Mon Jan 11 16:50:49 1999 +0100
     3.3 @@ -149,7 +149,6 @@
     3.4  
     3.5  Goalw [neg_def, int_def] "~ neg(int n)";
     3.6  by (Simp_tac 1);
     3.7 -by Safe_tac;
     3.8  qed "not_neg_nat";
     3.9  
    3.10  Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
     4.1 --- a/src/HOL/Lambda/Eta.ML	Mon Jan 11 12:52:53 1999 +0100
     4.2 +++ b/src/HOL/Lambda/Eta.ML	Mon Jan 11 16:50:49 1999 +0100
     4.3 @@ -28,9 +28,8 @@
     4.4  
     4.5  Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
     4.6  by (induct_tac "t" 1);
     4.7 -by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
     4.8 -by(Auto_tac);
     4.9 -by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
    4.10 +  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
    4.11 + by(nat_arith_tac 1);
    4.12  by(Auto_tac);
    4.13  qed "free_lift";
    4.14  Addsimps [free_lift];
    4.15 @@ -170,7 +169,6 @@
    4.16    by (etac thin_rl 1);
    4.17    by (exhaust_tac "t" 1);
    4.18      by (Asm_simp_tac 1);
    4.19 -    by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    4.20     by (Asm_simp_tac 1);
    4.21    by (Asm_simp_tac 1);
    4.22   by (Asm_simp_tac 1);
     5.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 11 12:52:53 1999 +0100
     5.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 11 16:50:49 1999 +0100
     5.3 @@ -27,9 +27,9 @@
     5.4    val sym:		thm (* x = y ==> y = x *)
     5.5    val decomp: term ->
     5.6               ((term * int)list * int * string * (term * int)list * int)option
     5.7 -  val mkEqTrue: thm -> thm
     5.8 +  val mk_Eq: thm -> thm
     5.9    val mk_Trueprop: term -> term
    5.10 -  val neg_prop: term -> term * bool
    5.11 +  val neg_prop: term -> term
    5.12    val simp: thm -> thm
    5.13    val is_False: thm -> bool
    5.14    val is_nat: typ list * term -> bool
    5.15 @@ -41,12 +41,13 @@
    5.16           p/q is the decomposition of the sum terms x/y into a list
    5.17           of summand * multiplicity pairs and a constant summand.
    5.18  
    5.19 -mkEqTrue(P) = `P == True'
    5.20 +mk_Eq(~in) = `in == False'
    5.21 +mk_Eq(in) = `in == True'
    5.22 +where `in' is an (in)equality.
    5.23  
    5.24 -neg_prop(t) = (nt,neg) if t is wrapped up in Trueprop and
    5.25 +neg_prop(t) = neg if t is wrapped up in Trueprop and
    5.26    nt is the (logically) negated version of t, where the negation
    5.27    of a negative term is the term itself (no double negation!);
    5.28 -  neg = `t is already negated'.
    5.29  
    5.30  simp must reduce contradictory <= to False.
    5.31     It should also cancel common summands to keep <= reduced;
    5.32 @@ -360,17 +361,17 @@
    5.33  
    5.34  fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i;
    5.35  
    5.36 -fun prover1(just,sg,thms,concl) =
    5.37 -let val (nconcl,neg) = LA_Data.neg_prop concl
    5.38 +fun prover1(just,sg,thms,concl,pos) =
    5.39 +let val nconcl = LA_Data.neg_prop concl
    5.40      val cnconcl = cterm_of sg nconcl
    5.41      val Fthm = mkthm sg (thms @ [assume cnconcl]) just
    5.42 -    val contr = if neg then LA_Data.notI else LA_Data.ccontr
    5.43 -in Some(LA_Data.mkEqTrue ((implies_intr cnconcl Fthm) COMP contr)) end
    5.44 +    val contr = if pos then LA_Data.ccontr else LA_Data.notI
    5.45 +in Some(LA_Data.mk_Eq ((implies_intr cnconcl Fthm) COMP contr)) end
    5.46  handle _ => None;
    5.47  
    5.48  (* handle thm with equality conclusion *)
    5.49  fun prover2(just1,just2,sg,thms,concl) =
    5.50 -let val (nconcl,_) = LA_Data.neg_prop concl (* m ~= n *)
    5.51 +let val nconcl = LA_Data.neg_prop concl (* m ~= n *)
    5.52      val cnconcl = cterm_of sg nconcl
    5.53      val neqthm = assume cnconcl
    5.54      val casethm = neqthm COMP LA_Data.neqE (* [|m<n ==> R; n<m ==> R|] ==> R *)
    5.55 @@ -382,17 +383,22 @@
    5.56      and thm2 = mkthm sg (thms @ [assume cless2]) just2
    5.57      val dthm1 = implies_intr cless1 thm1 and dthm2 = implies_intr cless2 thm2
    5.58      val thm = dthm2 COMP (dthm1 COMP casethm)
    5.59 -in Some(LA_Data.mkEqTrue ((implies_intr cnconcl thm) COMP LA_Data.ccontr)) end
    5.60 +in Some(LA_Data.mk_Eq ((implies_intr cnconcl thm) COMP LA_Data.ccontr)) end
    5.61  handle _ => None;
    5.62  
    5.63 -(* FIXME: forward proof of equalities missing! *)
    5.64 +(* PRE: concl is not negated! *)
    5.65  fun lin_arith_prover sg thms concl =
    5.66  let val Hs = map (#prop o rep_thm) thms
    5.67      val Tconcl = LA_Data.mk_Trueprop concl
    5.68  in case prove([],Hs,Tconcl) of
    5.69 -     [j] => prover1(j,sg,thms,Tconcl)
    5.70 +     [j] => prover1(j,sg,thms,Tconcl,true)
    5.71     | [j1,j2] => prover2(j1,j2,sg,thms,Tconcl)
    5.72 -   | _ => None
    5.73 +   | _ => let val nTconcl = LA_Data.neg_prop Tconcl
    5.74 +          in case prove([],Hs,nTconcl) of
    5.75 +               [j] => prover1(j,sg,thms,nTconcl,false)
    5.76 +               (* [_,_] impossible because of negation *)
    5.77 +             | _ => None
    5.78 +          end
    5.79  end;
    5.80  
    5.81  end;