1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Apr 29 17:08:38 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun May 02 13:13:44 2021 +0200
     1.3 @@ -5,19 +5,20 @@
     1.4                        (*  ^^^ for KEStore_Elems.add_thes *)
     1.5  begin
     1.6  subsection \<open>theorems for Base_Tools\<close>
     1.7 +
     1.8 +lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto
     1.9 +(*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
    1.10 +
    1.11 +(* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
    1.12 +lemma radd_left_cancel_le: "((k::real) + m <= k + n) = (m <= n)" by auto
    1.13 +(*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
    1.14 +
    1.15  axiomatization where (*for evaluating the assumptions of conditional rules*)
    1.16 +  (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
    1.17 +  rat_leq1: "[| 0 \<noteq> b; 0 \<noteq> d |] ==> (a / b <= c / d) = (a * d <= b * c)"(*Quickcheck found a counterexample*) and
    1.18 +  rat_leq2:	          "0 \<noteq> d    ==> (a     <= c / d) = (a * d <=     c)" (*Quickcheck found a counterexample*) and
    1.19 +  rat_leq3:	   "0 \<noteq> b           ==> (a / b <= c    ) = (a     <= b * c)" (*Quickcheck found a counterexample*)
    1.20  
    1.21 -(*last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
    1.22 -  real_unari_minus:   "- a = (-1) * a" and
    1.23 -  radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
    1.24 -  (* should be in Rational.thy, but: 
    1.25 -   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
    1.26 -  rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
    1.27 -		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
    1.28 -  rat_leq2:	      "d ~= 0 ==>
    1.29 -		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
    1.30 -  rat_leq3:	      "b ~= 0 ==>
    1.31 -		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
    1.32  
    1.33  subsection \<open>setup for ML-functions\<close>
    1.34  text \<open>required by "eval_binop" below\<close>