1 (* tools for arithmetic
2 author: Walther Neuper 010308
5 use_thy"IsacKnowledge/Atools";
6 use_thy"IsacKnowledge/Isac";
8 use_thy_only"IsacKnowledge/Atools";
9 use_thy"IsacKnowledge/Isac";
13 Atools = ComplexI + Descript +
15 (*-------------------- consts------------------------------------------------*)
21 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
22 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
24 "pow" :: [real, real] => real (infixr "^^^" 80)
25 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
27 (*WN0603 at FE-interface encoded strings to '^',
28 see 'fun encode', fun 'decode'*)
30 "abs" :: real => real ("(|| _ ||)")
31 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
32 "absset":: real set => real ("(||| _ |||)")
33 (*is numeral constant ?*)
34 "is'_const" :: real => bool ("_ is'_const" 10)
35 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
36 "is'_atom" :: real => bool ("_ is'_atom" 10)
37 "is'_even" :: real => bool ("_ is'_even" 10)
39 (* identity on term level*)
40 "ident" :: ['a, 'a] => bool ("(_ =!=/ _)" [51, 51] 50)
42 "argument'_in" :: real => real ("argument'_in _" 10)
43 "sameFunId" :: [real, bool] => bool (**"same'_funid _ _" 10
44 WN0609 changed the id, because ".. _ _" inhibits currying**)
45 "filter'_sameFunId":: [real, bool list] => bool list
46 ("filter'_sameFunId _ _" 10)
47 "boollist2sum" :: bool list => real
49 (*-------------------- rules -------------------------------------*)
50 rules (*for evaluating the assumptions of conditional rules*)
52 last_thmI "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
53 real_unari_minus "- a = (-1) * a"
55 rle_refl "(n::real) <= n"
56 (*reflI "(t = t) = True"*)
57 radd_left_cancel_le "((k::real) + m <= k + n) = (m <= n)"
58 not_true "(~ True) = False"
59 not_false "(~ False) = True"
60 and_true "(a & True) = a"
61 and_false "(a & False) = False"
62 or_true "(a | True) = True"
63 or_false "(a | False) = a"
64 and_commute "(a & b) = (b & a)"
65 or_commute "(a | b) = (b | a)"
67 (*.should be in Rational.thy, but:
68 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
69 rat_leq1 "[| b ~= 0; d ~= 0 |] ==> \
70 \((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
71 rat_leq2 "d ~= 0 ==> \
72 \( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
73 rat_leq3 "b ~= 0 ==> \
74 \((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)