1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/isac/IsacKnowledge/Atools.thy	Wed Jul 21 13:53:39 2010 +0200
     1.3 @@ -0,0 +1,76 @@
     1.4 +(* tools for arithmetic
     1.5 +   author: Walther Neuper 010308
     1.6 +
     1.7 +remove_thy"Atools";
     1.8 +use_thy"IsacKnowledge/Atools";
     1.9 +use_thy"IsacKnowledge/Isac";
    1.10 +
    1.11 +use_thy_only"IsacKnowledge/Atools";
    1.12 +use_thy"IsacKnowledge/Isac";
    1.13 +*)
    1.14 +
    1.15 +
    1.16 +Atools = ComplexI + Descript +
    1.17 +
    1.18 +(*-------------------- consts------------------------------------------------*)
    1.19 +consts
    1.20 +
    1.21 +  Arbfix, Undef    :: real
    1.22 +  dummy            :: real
    1.23 +
    1.24 +  some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
    1.25 +  occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
    1.26 +
    1.27 + "pow"   :: [real, real] => real    (infixr "^^^" 80)
    1.28 +(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
    1.29 +                           ~~~~     ~~~~    ~~~~     ~~~*)
    1.30 +(*WN0603 at FE-interface encoded strings to '^', 
    1.31 +	see 'fun encode', fun 'decode'*)
    1.32 +
    1.33 +  "abs"   :: real => real            ("(|| _ ||)")
    1.34 +(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    1.35 +  "absset":: real set => real        ("(||| _ |||)")
    1.36 +  (*is numeral constant ?*)
    1.37 +  "is'_const" :: real => bool        ("_ is'_const" 10)
    1.38 +  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
    1.39 +  "is'_atom"  :: real => bool        ("_ is'_atom" 10)
    1.40 +  "is'_even"  :: real => bool        ("_ is'_even" 10)
    1.41 +		
    1.42 +  (* identity on term level*)
    1.43 +  "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)
    1.44 +
    1.45 +  "argument'_in"    :: real => real ("argument'_in _" 10)
    1.46 +  "sameFunId"       :: [real, bool] => bool (**"same'_funid _ _" 10
    1.47 +	WN0609 changed the id, because ".. _ _" inhibits currying**)
    1.48 +  "filter'_sameFunId":: [real, bool list] => bool list 
    1.49 +					("filter'_sameFunId _ _" 10)
    1.50 +  "boollist2sum"    :: bool list => real
    1.51 +
    1.52 +(*-------------------- rules -------------------------------------*)
    1.53 +rules (*for evaluating the assumptions of conditional rules*)
    1.54 +
    1.55 +  last_thmI	"lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
    1.56 +  real_unari_minus           "- a = (-1) * a"
    1.57 +
    1.58 +  rle_refl                  "(n::real) <= n"
    1.59 +(*reflI                     "(t = t) = True"*)
    1.60 +  radd_left_cancel_le       "((k::real) + m <= k + n) = (m <= n)"
    1.61 +  not_true                  "(~ True) = False"
    1.62 +  not_false                 "(~ False) = True"
    1.63 +  and_true                  "(a & True) = a"
    1.64 +  and_false                 "(a & False) = False"
    1.65 +  or_true                   "(a | True) = True"
    1.66 +  or_false                  "(a | False) = a"
    1.67 +  and_commute               "(a & b) = (b & a)"
    1.68 +  or_commute                "(a | b) = (b | a)"
    1.69 +
    1.70 +  (*.should be in Rational.thy, but: 
    1.71 +   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
    1.72 +  rat_leq1	          "[| b ~= 0; d ~= 0 |] ==> \
    1.73 +			  \((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
    1.74 +  rat_leq2	          "d ~= 0 ==> \
    1.75 +			  \( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*)
    1.76 +  rat_leq3	          "b ~= 0 ==> \
    1.77 +			  \((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
    1.78 +
    1.79 +end