|
1 (* tools for arithmetic |
|
2 author: Walther Neuper 010308 |
|
3 |
|
4 remove_thy"Atools"; |
|
5 use_thy"IsacKnowledge/Atools"; |
|
6 use_thy"IsacKnowledge/Isac"; |
|
7 |
|
8 use_thy_only"IsacKnowledge/Atools"; |
|
9 use_thy"IsacKnowledge/Isac"; |
|
10 *) |
|
11 |
|
12 |
|
13 Atools = ComplexI + Descript + |
|
14 |
|
15 (*-------------------- consts------------------------------------------------*) |
|
16 consts |
|
17 |
|
18 Arbfix, Undef :: real |
|
19 dummy :: real |
|
20 |
|
21 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _") |
|
22 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _") |
|
23 |
|
24 "pow" :: [real, real] => real (infixr "^^^" 80) |
|
25 (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat) |
|
26 ~~~~ ~~~~ ~~~~ ~~~*) |
|
27 (*WN0603 at FE-interface encoded strings to '^', |
|
28 see 'fun encode', fun 'decode'*) |
|
29 |
|
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) |
|
38 |
|
39 (* identity on term level*) |
|
40 "ident" :: ['a, 'a] => bool ("(_ =!=/ _)" [51, 51] 50) |
|
41 |
|
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 |
|
48 |
|
49 (*-------------------- rules -------------------------------------*) |
|
50 rules (*for evaluating the assumptions of conditional rules*) |
|
51 |
|
52 last_thmI "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" |
|
53 real_unari_minus "- a = (-1) * a" |
|
54 |
|
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)" |
|
66 |
|
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?*) |
|
75 |
|
76 end |