1.1 --- a/test/Tools/isac/Knowledge/Isac.thy Mon Jul 15 08:28:50 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,116 +0,0 @@
1.4 -(* Title: test/Tools/isac/Isac.thy
1.5 - Author: Walther Neuper, TU Graz, 2010
1.6 - (c) due to copyright terms
1.7 -
1.8 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.9 - 10 20 30 40 50 60 70 80
1.10 -*)
1.11 -
1.12 -(*WN110319 theory Isac imports Complex_Main (*TODO Build_Isac*) begin*)
1.13 -theory isac imports Isac
1.14 -imports "Frontend/Frontend"
1.15 - PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) DiophantEq Test
1.16 -begin
1.17 -
1.18 -
1.19 -text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
1.20 - the leading parts of longnames can be dropped with some exceptions. *}
1.21 -
1.22 -lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule List.take_Cons)
1.23 -lemma "t = (t::real)" by (rule HOL.refl)
1.24 -lemma "take n [] = []" by (rule List.take_Nil)
1.25 -lemma "(f o g) x = f (g x)" by (rule Fun.o_apply)
1.26 -lemma "(if True then x else y) = x" by (rule HOL.if_True)
1.27 -lemma "(if False then x else y) = y" by (rule HOL.if_False)
1.28 -(*lemma "- z1 = -1 * z1" by (rule \*)
1.29 -lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule Rings.semiring_class.left_distrib)
1.30 -lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule Rings.semiring_class.right_distrib)
1.31 -lemma "r1 * r1 = (r1::real) ^ 2" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29))
1.32 -lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26))
1.33 -lemma "z * 1 = (z::real)" by (rule Groups.monoid_mult_class.mult_1_right)
1.34 -(*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.35 -lemma "1 * z = (z::real)" by (rule Groups.monoid_mult_class.mult_1_left)
1.36 -lemma "0 * z = (0::real)" by (rule Rings.mult_zero_class.mult_zero_left)
1.37 -lemma "z * 0 = (0::real)" by (rule Rings.mult_zero_class.mult_zero_right)
1.38 -lemma "0 + z = (z::real)" by (rule Groups.monoid_add_class.add_0_left)
1.39 -lemma "z + 0 = (z::real)" by (rule Groups.monoid_add_class.add_0_right)
1.40 -lemma "0 / x = (0::real)" by (rule Rings.division_ring_class.divide_zero_left)
1.41 -lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
1.42 -lemma "n <= (n::real)" by (rule RealDef.order_refl)
1.43 -lemma "- (- z) = (z::real)" by (rule Groups.group_add_class.minus_minus)
1.44 -lemma "z * w = w * (z::real)" by (rule RealDef.mult_commute)
1.45 -lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
1.46 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule RealDef.mult_assoc)
1.47 -lemma "z + w = w + (z::real)" by (rule Groups.ab_semigroup_add_class.add_commute)
1.48 -lemma "x + (y + z) = y + (x + (z::real))" by (rule Groups.ab_semigroup_add_class.add_left_commute)
1.49 -lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule Groups.semigroup_add_class.add_assoc)
1.50 -lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule Rings.ring_class.minus_mult_left)
1.51 -lemma "z + - z = (0::real)" by (rule Groups.group_add_class.right_minus)
1.52 -lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
1.53 -lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule Rings.division_ring_class.minus_divide_left)
1.54 -
1.55 -lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
1.56 -lemma "x * (y / z) = x * y / (z::real)" by (rule Rings.division_ring_class.times_divide_eq_right) (*without (1)*)
1.57 -
1.58 -lemma "y / z * x = y * x / (z::real)" by (rule Fields.field_class.times_divide_eq_left)
1.59 -lemma "x / y / z = x / (y * (z::real))" by (rule Fields.field_inverse_zero_class.divide_divide_eq_left)
1.60 -lemma "x / (y / z) = x * z / (y::real)" by (rule Fields.field_inverse_zero_class.divide_divide_eq_right)
1.61 -lemma "x / 1 = (x::real)" by (rule Rings.division_ring_class.divide_1)
1.62 -lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule Rings.ring_class.left_diff_distrib)
1.63 -lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule Rings.ring_class.right_diff_distrib)
1.64 -lemma "(x + y) / z = x / z + y / (z::real)" by (rule Rings.division_ring_class.add_divide_distrib)
1.65 -
1.66 -section {* comments on the above *}
1.67 -subsection {* these are twice: *}
1.68 -text {*
1.69 -(*lemma "m1 + (n1 + k1) = m1 + n1 + k1" + see sym_real_add_assoc *)
1.70 -(*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_mult_assoc*)
1.71 -*}
1.72 -
1.73 -subsection {* leading parts of long.names can be omitted, except *_class.*(n)*}
1.74 -lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)" by (rule take_Cons)
1.75 -lemma "t = (t::real)" by (rule refl)
1.76 -lemma "take n [] = []" by (rule take_Nil)
1.77 -lemma "(f o g) x = f (g x)" by (rule o_apply)
1.78 -lemma "(if True then x else y) = x" by (rule if_True)
1.79 -lemma "(if False then x else y) = y" by (rule if_False)
1.80 -(*lemma "- z1 = -1 * z1" by (rule \*)
1.81 -lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)" by (rule left_distrib)
1.82 -lemma "w * (z1 + z2) = w * z1 + w * (z2::real)" by (rule right_distrib)
1.83 -lemma "r1 * r1 = (r1::real) ^ 2" by (rule comm_semiring_1_class.normalizing_semiring_rules(29))
1.84 -lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)" by (rule comm_semiring_1_class.normalizing_semiring_rules(26))
1.85 -lemma "z * 1 = (z::real)" by (rule mult_1_right)
1.86 -(*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.87 -lemma "1 * z = (z::real)" by (rule mult_1_left)
1.88 -lemma "0 * z = (0::real)" by (rule mult_zero_left)
1.89 -lemma "z * 0 = (0::real)" by (rule mult_zero_right)
1.90 -lemma "0 + z = (z::real)" by (rule add_0_left)
1.91 -lemma "z + 0 = (z::real)" by (rule add_0_right)
1.92 -lemma "0 / x = (0::real)" by (rule divide_zero_left)
1.93 -lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
1.94 -lemma "n <= (n::real)" by (rule order_refl)
1.95 -lemma "- (- z) = (z::real)" by (rule minus_minus)
1.96 -lemma "z * w = w * (z::real)" by (rule mult_commute)
1.97 -lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
1.98 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule mult_assoc)
1.99 -lemma "z + w = w + (z::real)" by (rule add_commute)
1.100 -lemma "x + (y + z) = y + (x + (z::real))" by (rule add_left_commute)
1.101 -lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule add_assoc)
1.102 -lemma "- (x1 * y1) = - x1 * (y1::real)" by (rule minus_mult_left)
1.103 -lemma "z + - z = (0::real)" by (rule right_minus)
1.104 -lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))
1.105 -lemma "- (x1 / y1) = - x1 / (y1::real)" by (rule minus_divide_left)
1.106 -
1.107 -lemma "x * (y / z) = x * y / (z::real)" by (rule Fields.field_class.times_divide_eq(1))
1.108 -lemma "x * (y / z) = x * y / (z::real)" by (rule times_divide_eq_right)
1.109 -
1.110 -lemma "y / z * x = y * x / (z::real)" by (rule times_divide_eq_left)
1.111 -lemma "x / y / z = x / (y * (z::real))" by (rule divide_divide_eq_left)
1.112 -lemma "x / (y / z) = x * z / (y::real)" by (rule divide_divide_eq_right)
1.113 -lemma "x / 1 = (x::real)" by (rule divide_1)
1.114 -lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)" by (rule left_diff_distrib)
1.115 -lemma "w * (z1 - z2) = w * z1 - w * (z2::real)" by (rule right_diff_distrib)
1.116 -lemma "(x + y) / z = x / z + y / (z::real)" by (rule add_divide_distrib)
1.117 -
1.118 -
1.119 -end
1.120 \ No newline at end of file