| author | Walther Neuper <neuper@ist.tugraz.at> |
| Wed, 25 Aug 2010 16:20:07 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 37947 | 22235e4dbe5f |
| parent 37906 | src/Tools/isac/IsacKnowledge/LogExp.thy@e2b23ba9df13 |
| child 37954 | 4022d670753c |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
(* all outcommented in order to demonstrate authoring: |
| neuper@37906 | 2 |
WN071203 |
| neuper@37906 | 3 |
remove_thy"LogExp"; |
| neuper@37947 | 4 |
use_thy_only"Knowledge/LogExp"; |
| neuper@37947 | 5 |
use_thy_only"Knowledge/Isac"; |
| neuper@37906 | 6 |
*) |
| neuper@37906 | 7 |
LogExp = PolyEq + |
| neuper@37906 | 8 |
|
| neuper@37906 | 9 |
consts |
| neuper@37906 | 10 |
|
| neuper@37906 | 11 |
ln :: "real => real" |
| neuper@37906 | 12 |
exp :: "real => real" ("E'_ ^^^ _" 80)
|
| neuper@37906 | 13 |
|
| neuper@37906 | 14 |
(*--------------------------------------------------*) |
| neuper@37906 | 15 |
alog :: "[real, real] => real" ("_ log _" 90)
|
| neuper@37906 | 16 |
|
| neuper@37906 | 17 |
(*Script-names*) |
| neuper@37906 | 18 |
Solve'_log :: "[bool,real, bool list] \ |
| neuper@37906 | 19 |
\=> bool list" |
| neuper@37906 | 20 |
("((Script Solve'_log (_ _=))//(_))" 9)
|
| neuper@37906 | 21 |
|
| neuper@37906 | 22 |
rules |
| neuper@37906 | 23 |
|
| neuper@37906 | 24 |
equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)" |
| neuper@37906 | 25 |
(* this is what students ^^^^^^^... are told to do *) |
| neuper@37906 | 26 |
equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)" |
| neuper@37906 | 27 |
exp_invers_log "a^^^(a log b) = b" |
| neuper@37906 | 28 |
(*---------------------------------------------------*) |
| neuper@37906 | 29 |
|
| neuper@37906 | 30 |
end |