3 (** )"../BridgeJEdit/BridgeJEdit" ( *activate after devel.of BridgeJEdit*) |
3 (** )"../BridgeJEdit/BridgeJEdit" ( *activate after devel.of BridgeJEdit*) |
4 (**) "../BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*) |
4 (**) "../BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*) |
5 (* ^^^ for KEStore_Elems.add_thes *) |
5 (* ^^^ for KEStore_Elems.add_thes *) |
6 begin |
6 begin |
7 subsection \<open>theorems for Base_Tools\<close> |
7 subsection \<open>theorems for Base_Tools\<close> |
|
8 |
|
9 lemma real_unari_minus: "- a = (-1) * (a::real)" by auto |
|
10 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*) |
|
11 |
|
12 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *) |
|
13 lemma radd_left_cancel_le: "((k::real) + m <= k + n) = (m <= n)" by auto |
|
14 (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*) |
|
15 |
8 axiomatization where (*for evaluating the assumptions of conditional rules*) |
16 axiomatization where (*for evaluating the assumptions of conditional rules*) |
|
17 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *) |
|
18 rat_leq1: "[| 0 \<noteq> b; 0 \<noteq> d |] ==> (a / b <= c / d) = (a * d <= b * c)"(*Quickcheck found a counterexample*) and |
|
19 rat_leq2: "0 \<noteq> d ==> (a <= c / d) = (a * d <= c)" (*Quickcheck found a counterexample*) and |
|
20 rat_leq3: "0 \<noteq> b ==> (a / b <= c ) = (a <= b * c)" (*Quickcheck found a counterexample*) |
9 |
21 |
10 (*last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*) |
|
11 real_unari_minus: "- a = (-1) * a" and |
|
12 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and |
|
13 (* should be in Rational.thy, but: |
|
14 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*) |
|
15 rat_leq1: "[| b ~= 0; d ~= 0 |] ==> |
|
16 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and |
|
17 rat_leq2: "d ~= 0 ==> |
|
18 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and |
|
19 rat_leq3: "b ~= 0 ==> |
|
20 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*) |
|
21 |
22 |
22 subsection \<open>setup for ML-functions\<close> |
23 subsection \<open>setup for ML-functions\<close> |
23 text \<open>required by "eval_binop" below\<close> |
24 text \<open>required by "eval_binop" below\<close> |
24 setup \<open>KEStore_Elems.add_calcs |
25 setup \<open>KEStore_Elems.add_calcs |
25 [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")), |
26 [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")), |