1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/Isac.thy Mon Aug 30 15:18:09 2010 +0200
1.3 @@ -0,0 +1,58 @@
1.4 +(* Title: test/Tools/isac/Isac.thy
1.5 + Author: Walther Neuper, TU Graz
1.6 +
1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 + 10 20 30 40 50 60 70 80
1.9 +*)
1.10 +
1.11 +theory Isac imports Complex_Main (*TODO Build_Isac*) begin
1.12 +
1.13 +section {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals *}
1.14 +
1.15 +lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule List.take_Cons)
1.16 +lemma "t = (t::real)" by (rule HOL.refl)
1.17 +lemma "take n [] = []" by (rule List.take_Nil)
1.18 +lemma "(f o g) x = f (g x)" by (rule Fun.o_apply)
1.19 +lemma "(if True then x else y) = x" by (rule HOL.if_True)
1.20 +lemma "(if False then x else y) = y" by (rule HOL.if_False)
1.21 +(*lemma "- z1 = -1 * z1" by (rule \*)
1.22 +lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule Rings.semiring_class.left_distrib)
1.23 +lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule Rings.semiring_class.right_distrib)
1.24 +lemma "r1 * r1 = (r1::real) ^ 2" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29))
1.25 +lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26))
1.26 +lemma "z * 1 = (z::real)" by (rule Groups.monoid_mult_class.mult_1_right)
1.27 +(*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*)
1.28 +lemma "1 * z = (z::real)" by (rule Groups.monoid_mult_class.mult_1_left)
1.29 +lemma "0 * z = (0::real)" by (rule Rings.mult_zero_class.mult_zero_left)
1.30 +lemma "z * 0 = (0::real)" by (rule Rings.mult_zero_class.mult_zero_right)
1.31 +lemma "0 + z = (z::real)" by (rule Groups.monoid_add_class.add_0_left)
1.32 +lemma "z + 0 = (z::real)" by (rule Groups.monoid_add_class.add_0_right)
1.33 +lemma "0 / x = (0::real)" by (rule Rings.division_ring_class.divide_zero_left)
1.34 +lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
1.35 +lemma "n <= (n::real)" by (rule RealDef.real_le_refl)
1.36 +lemma "- (- z) = (z::real)" by (rule Groups.group_add_class.minus_minus)
1.37 +lemma "z * w = w * (z::real)" by (rule RealDef.real_mult_commute)
1.38 +lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
1.39 +lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule RealDef.real_mult_assoc)
1.40 +lemma "z + w = w + (z::real)" by (rule Groups.ab_semigroup_add_class.add_commute)
1.41 +lemma "x + (y + z) = y + (x + (z::real))" by (rule Groups.ab_semigroup_add_class.add_left_commute)
1.42 +lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule Groups.semigroup_add_class.add_assoc)
1.43 +lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule Rings.ring_class.minus_mult_left)
1.44 +lemma "z + - z = (0::real)" by (rule Groups.group_add_class.right_minus)
1.45 +lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
1.46 +lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule Rings.division_ring_class.minus_divide_left)
1.47 +lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
1.48 +lemma "y / z * x = y * x / (z::real)" by (rule Fields.field_class.times_divide_eq_left)
1.49 +lemma "x / y / z = x / (y * (z::real))" by (rule Fields.field_inverse_zero_class.divide_divide_eq_left)
1.50 +lemma "x / (y / z) = x * z / (y::real)" by (rule Fields.field_inverse_zero_class.divide_divide_eq_right)
1.51 +lemma "x / 1 = (x::real)" by (rule Rings.division_ring_class.divide_1)
1.52 +lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule Rings.ring_class.left_diff_distrib)
1.53 +lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule Rings.ring_class.right_diff_distrib)
1.54 +lemma "(x + y) / z = x / z + y / (z::real)" by (rule Rings.division_ring_class.add_divide_distrib)
1.55 +
1.56 +
1.57 +text {* these are twice:
1.58 +(*lemma "m1 + (n1 + k1) = m1 + n1 + k1" + see sym_real_add_assoc *)
1.59 +(*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_real_mult_assoc*)
1.60 +*}
1.61 +end
1.62 \ No newline at end of file