1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Aug 30 15:18:09 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Aug 31 10:19:02 2010 +0200
1.3 @@ -59,8 +59,7 @@
1.4 (*use_thy "Knowledge/Typefix" FIXXXMEWN100827*)
1.5 use_thy "Knowledge/Descript"
1.6
1.7 -ML {* @{thm sym} *}
1.8 -ML {* @{thm } RS @{thm } *}
1.9 +ML {* @{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)} *}
1.10
1.11 ML {*"--------------------------------------------"*}
1.12
2.1 --- a/test/Tools/isac/Knowledge/Isac.thy Mon Aug 30 15:18:09 2010 +0200
2.2 +++ b/test/Tools/isac/Knowledge/Isac.thy Tue Aug 31 10:19:02 2010 +0200
2.3 @@ -41,7 +41,10 @@
2.4 lemma "z + - z = (0::real)" by (rule Groups.group_add_class.right_minus)
2.5 lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
2.6 lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule Rings.division_ring_class.minus_divide_left)
2.7 +
2.8 lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
2.9 +lemma "x * (y / z) = x * y / (z::real)" by (rule Rings.division_ring_class.times_divide_eq_right) (*without (1)*)
2.10 +
2.11 lemma "y / z * x = y * x / (z::real)" by (rule Fields.field_class.times_divide_eq_left)
2.12 lemma "x / y / z = x / (y * (z::real))" by (rule Fields.field_inverse_zero_class.divide_divide_eq_left)
2.13 lemma "x / (y / z) = x * z / (y::real)" by (rule Fields.field_inverse_zero_class.divide_divide_eq_right)
2.14 @@ -50,9 +53,57 @@
2.15 lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule Rings.ring_class.right_diff_distrib)
2.16 lemma "(x + y) / z = x / z + y / (z::real)" by (rule Rings.division_ring_class.add_divide_distrib)
2.17
2.18 -
2.19 -text {* these are twice:
2.20 +section {* comments on the above *}
2.21 +subsection {* these are twice: *}
2.22 +text {*
2.23 (*lemma "m1 + (n1 + k1) = m1 + n1 + k1" + see sym_real_add_assoc *)
2.24 (*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_real_mult_assoc*)
2.25 *}
2.26 +
2.27 +subsection {* leading parts of long.names can be omitted, except *_class.*(n)*}
2.28 +lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule take_Cons)
2.29 +lemma "t = (t::real)" by (rule refl)
2.30 +lemma "take n [] = []" by (rule take_Nil)
2.31 +lemma "(f o g) x = f (g x)" by (rule o_apply)
2.32 +lemma "(if True then x else y) = x" by (rule if_True)
2.33 +lemma "(if False then x else y) = y" by (rule if_False)
2.34 +(*lemma "- z1 = -1 * z1" by (rule \*)
2.35 +lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule left_distrib)
2.36 +lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule right_distrib)
2.37 +lemma "r1 * r1 = (r1::real) ^ 2" by (rule comm_semiring_1_class.normalizing_semiring_rules(29))
2.38 +lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule comm_semiring_1_class.normalizing_semiring_rules(26))
2.39 +lemma "z * 1 = (z::real)" by (rule mult_1_right)
2.40 +(*lemma "z1 + z1 = 2 * z1::real)" by (rule !!!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4)): m + m = ((1::'a) + (1::'a)) * m*)
2.41 +lemma "1 * z = (z::real)" by (rule mult_1_left)
2.42 +lemma "0 * z = (0::real)" by (rule mult_zero_left)
2.43 +lemma "z * 0 = (0::real)" by (rule mult_zero_right)
2.44 +lemma "0 + z = (z::real)" by (rule add_0_left)
2.45 +lemma "z + 0 = (z::real)" by (rule add_0_right)
2.46 +lemma "0 / x = (0::real)" by (rule divide_zero_left)
2.47 +lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
2.48 +lemma "n <= (n::real)" by (rule real_le_refl)
2.49 +lemma "- (- z) = (z::real)" by (rule minus_minus)
2.50 +lemma "z * w = w * (z::real)" by (rule real_mult_commute)
2.51 +lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
2.52 +lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule real_mult_assoc)
2.53 +lemma "z + w = w + (z::real)" by (rule add_commute)
2.54 +lemma "x + (y + z) = y + (x + (z::real))" by (rule add_left_commute)
2.55 +lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule add_assoc)
2.56 +lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule minus_mult_left)
2.57 +lemma "z + - z = (0::real)" by (rule right_minus)
2.58 +lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
2.59 +lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule minus_divide_left)
2.60 +
2.61 +lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
2.62 +lemma "x * (y / z) = x * y / (z::real)" by (rule times_divide_eq_right)
2.63 +
2.64 +lemma "y / z * x = y * x / (z::real)" by (rule times_divide_eq_left)
2.65 +lemma "x / y / z = x / (y * (z::real))" by (rule divide_divide_eq_left)
2.66 +lemma "x / (y / z) = x * z / (y::real)" by (rule divide_divide_eq_right)
2.67 +lemma "x / 1 = (x::real)" by (rule divide_1)
2.68 +lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule left_diff_distrib)
2.69 +lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule right_diff_distrib)
2.70 +lemma "(x + y) / z = x / z + y / (z::real)" by (rule add_divide_distrib)
2.71 +
2.72 +
2.73 end
2.74 \ No newline at end of file