1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sun May 02 13:13:44 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Sun May 02 15:55:37 2021 +0200
1.3 @@ -10,14 +10,16 @@
1.4 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
1.5
1.6 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
1.7 -lemma radd_left_cancel_le: "((k::real) + m <= k + n) = (m <= n)" by auto
1.8 +lemma radd_left_cancel_le: "((k::real) + m \<le> k + n) = (m \<le> n)" by auto
1.9 (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
1.10
1.11 +thm "Fields.linordered_field_class.mult_imp_le_div_pos" (*0 < ?y \<Longrightarrow> ?z * ?y \<le> ?x \<Longrightarrow> ?z \<le> ?x / ?y*)
1.12 +
1.13 axiomatization where (*for evaluating the assumptions of conditional rules*)
1.14 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
1.15 - rat_leq1: "[| 0 \<noteq> b; 0 \<noteq> d |] ==> (a / b <= c / d) = (a * d <= b * c)"(*Quickcheck found a counterexample*) and
1.16 - rat_leq2: "0 \<noteq> d ==> (a <= c / d) = (a * d <= c)" (*Quickcheck found a counterexample*) and
1.17 - rat_leq3: "0 \<noteq> b ==> (a / b <= c ) = (a <= b * c)" (*Quickcheck found a counterexample*)
1.18 + rat_leq1: "0 \<noteq> b \<Longrightarrow> 0 \<noteq> d \<Longrightarrow> (a / b \<le> c / d) = (a * d \<le> b * c)"(*Quickcheck found a counterexample*) and
1.19 + rat_leq2: "0 \<noteq> d \<Longrightarrow> (a \<le> c / d) = (a * d \<le> c)"(*Quickcheck found a counterexample*) and
1.20 + rat_leq3: "0 \<noteq> b \<Longrightarrow> (a / b \<le> c ) = (a \<le> b * c)"(*Quickcheck found a counterexample*)
1.21
1.22
1.23 subsection \<open>setup for ML-functions\<close>