(* tools for arithmetic

   author: Walther Neuper 010308

remove_thy"Atools";

use_thy"IsacKnowledge/Atools";

use_thy"IsacKnowledge/Isac";

use_thy_only"IsacKnowledge/Atools";

use_thy"IsacKnowledge/Isac";

*)

Atools = ComplexI + Descript +

(*-------------------- consts------------------------------------------------*)

consts

  Arbfix, Undef    :: real

  dummy            :: real

  some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")

  occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")

 "pow"   :: [real, real] => real    (infixr "^^^" 80)

(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)

                           ~~~~     ~~~~    ~~~~     ~~~*)

(*WN0603 at FE-interface encoded strings to '^', 

	see 'fun encode', fun 'decode'*)

  "abs"   :: real => real            ("(|| _ ||)")

(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)

  "absset":: real set => real        ("(||| _ |||)")

  (*is numeral constant ?*)

  "is'_const" :: real => bool        ("_ is'_const" 10)

  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)

  "is'_atom"  :: real => bool        ("_ is'_atom" 10)

  "is'_even"  :: real => bool        ("_ is'_even" 10)

  (* identity on term level*)

  "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)

  "argument'_in"  :: real => real ("argument'_in _" 10)

  "sameFunId"     :: [real, bool] => bool (**"same'_funid _ _" 10

	WN0609 changed the id, because ".. _ _" inhibits currying**)

(*-------------------- rules -------------------------------------*)

rules (*for evaluating the assumptions of conditional rules*)

  last_thmI	"lastI (x#xs) = (if xs =!= [] then x else lastI xs)"

  real_unari_minus           "- a = (-1) * a"

  rle_refl                  "(n::real) <= n"

(*reflI                     "(t = t) = True"*)

  radd_left_cancel_le       "((k::real) + m <= k + n) = (m <= n)"

  not_true                  "(~ True) = False"

  not_false                 "(~ False) = True"

  and_true                  "(a & True) = a"

  and_false                 "(a & False) = False"

  or_true                   "(a | True) = True"

  or_false                  "(a | False) = a"

  and_commute               "(a & b) = (b & a)"

  or_commute                "(a | b) = (b | a)"

  (*.should be in Rational.thy, but: 

   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)

  rat_leq1	          "[| b ~= 0; d ~= 0 |] ==> \

			  \((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)

  rat_leq2	          "d ~= 0 ==> \

			  \( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*)

  rat_leq3	          "b ~= 0 ==> \

			  \((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)

end