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>

     2.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Apr 29 17:08:38 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Sun May 02 13:13:44 2021 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4    exception Bind raised 
     2.5    (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):
     2.6      'val (Form f, tac, asms) = pt_extract (pt, p);' *)
     2.7 -d2_pqformula1:         "[|0<=p \<up> 2 - 4*q|] ==> (q+p*bdv+   bdv \<up> 2=0) =
     2.8 +  d2_pqformula1:         "[|0<=p \<up> 2 - 4*q|] ==> (q+p*bdv+   bdv \<up> 2=0) =
     2.9                             ((bdv= (-1)*(p/2) + sqrt(p \<up> 2 - 4*q)/2) 
    2.10                            | (bdv= (-1)*(p/2) - sqrt(p \<up> 2 - 4*q)/2))" and
    2.11    d2_pqformula1_neg:     "[|p \<up> 2 - 4*q<0|] ==> (q+p*bdv+   bdv \<up> 2=0) = False" and