(*  Title:  test/Tools/isac/Isac.thy

    Author: Walther Neuper, TU Graz, 2010

    (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

theory Isac imports Complex_Main (*TODO Build_Isac*) begin

text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;

        the leading parts of longnames can be dropped with some exceptions. *}

lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)"          by (rule List.take_Cons)

lemma "t = (t::real)"                                                           by (rule HOL.refl)

lemma "take n [] = []"                                                          by (rule List.take_Nil)

lemma "(f o g) x = f (g x)"                                                     by (rule Fun.o_apply)

lemma "(if True then x else y) = x"                                             by (rule HOL.if_True)

lemma "(if False then x else y) = y"                                            by (rule HOL.if_False)

(*lemma "- z1 = -1 * z1"                                                        by (rule \*)

lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)"                                 by (rule Rings.semiring_class.left_distrib)

lemma "w * (z1 + z2) = w * z1 + w * (z2::real)"                                 by (rule Rings.semiring_class.right_distrib)

lemma "r1 * r1 = (r1::real) ^ 2"                                                by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29))

lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)"                              by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26))

lemma "z * 1 = (z::real)"                                                       by (rule Groups.monoid_mult_class.mult_1_right)

(*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*)

lemma "1 * z = (z::real)"                                                       by (rule Groups.monoid_mult_class.mult_1_left)

lemma "0 * z = (0::real)"                                                       by (rule Rings.mult_zero_class.mult_zero_left)

lemma "z * 0 = (0::real)"                                                       by (rule Rings.mult_zero_class.mult_zero_right)

lemma "0 + z = (z::real)"                                                       by (rule Groups.monoid_add_class.add_0_left)

lemma "z + 0 = (z::real)"                                                       by (rule Groups.monoid_add_class.add_0_right)

lemma "0 / x = (0::real)"                                                       by (rule Rings.division_ring_class.divide_zero_left)

lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)"                                   by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))

lemma "n <= (n::real)"                                                          by (rule RealDef.real_le_refl)

lemma "- (- z) = (z::real)"                                                     by (rule Groups.group_add_class.minus_minus)

lemma "z * w = w * (z::real)"                                                   by (rule RealDef.real_mult_commute)

lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))"                                 by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))

lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))"                                   by (rule RealDef.real_mult_assoc)

lemma "z + w = w + (z::real)"                                                   by (rule Groups.ab_semigroup_add_class.add_commute)

lemma "x + (y + z) = y + (x + (z::real))"                                       by (rule Groups.ab_semigroup_add_class.add_left_commute)

lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))"                                   by (rule Groups.semigroup_add_class.add_assoc)

lemma "- (x1 * y1) = - x1 * (y1::real)"                                         by (rule Rings.ring_class.minus_mult_left)

lemma "z + - z = (0::real)"                                                     by (rule Groups.group_add_class.right_minus)

lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)"                                   by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))

lemma "- (x1 / y1) = - x1 / (y1::real)"                                         by (rule Rings.division_ring_class.minus_divide_left)

lemma "x * (y / z) = x * y / (z::real)"                                         by (rule Fields.field_class.times_divide_eq(1))

lemma "x * (y / z) = x * y / (z::real)"                                         by (rule Rings.division_ring_class.times_divide_eq_right) (*without (1)*)

lemma "y / z * x = y * x / (z::real)"                                           by (rule Fields.field_class.times_divide_eq_left)

lemma "x / y / z = x / (y * (z::real))"                                         by (rule Fields.field_inverse_zero_class.divide_divide_eq_left)

lemma "x / (y / z) = x * z / (y::real)"                                         by (rule Fields.field_inverse_zero_class.divide_divide_eq_right)

lemma "x / 1 = (x::real)"                                                       by (rule Rings.division_ring_class.divide_1)

lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)"                                 by (rule Rings.ring_class.left_diff_distrib)

lemma "w * (z1 - z2) = w * z1 - w * (z2::real)"                                 by (rule Rings.ring_class.right_diff_distrib)

lemma "(x + y) / z = x / z + y / (z::real)"                                     by (rule Rings.division_ring_class.add_divide_distrib)

section {* comments on the above *}

subsection {* these are twice: *}

text {*

(*lemma "m1 + (n1 + k1) = m1 + n1 + k1"              + see sym_real_add_assoc *)

(*lemma "m1 * (n1 * k1) = m1 * n1 * k1"  )]          + see sym_real_mult_assoc*)

*}

subsection {* leading parts of long.names can be omitted, except *_class.*(n)*}

lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)"          by (rule take_Cons)

lemma "t = (t::real)"                                                           by (rule refl)

lemma "take n [] = []"                                                          by (rule take_Nil)

lemma "(f o g) x = f (g x)"                                                     by (rule o_apply)

lemma "(if True then x else y) = x"                                             by (rule if_True)

lemma "(if False then x else y) = y"                                            by (rule if_False)

(*lemma "- z1 = -1 * z1"                                                        by (rule \*)

lemma "(z1 + z2) * w = z1 * w + z2 * (w::real)"                                 by (rule left_distrib)

lemma "w * (z1 + z2) = w * z1 + w * (z2::real)"                                 by (rule right_distrib)

lemma "r1 * r1 = (r1::real) ^ 2"                                                by (rule comm_semiring_1_class.normalizing_semiring_rules(29))

lemma "r1 ^ n1 * r1 ^ m1 = (r1::real) ^ (n1 + m1)"                              by (rule comm_semiring_1_class.normalizing_semiring_rules(26))

lemma "z * 1 = (z::real)"                                                       by (rule mult_1_right)

(*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*)

lemma "1 * z = (z::real)"                                                       by (rule mult_1_left)

lemma "0 * z = (0::real)"                                                       by (rule mult_zero_left)

lemma "z * 0 = (0::real)"                                                       by (rule mult_zero_right)

lemma "0 + z = (z::real)"                                                       by (rule add_0_left)

lemma "z + 0 = (z::real)"                                                       by (rule add_0_right)

lemma "0 / x = (0::real)"                                                       by (rule divide_zero_left)

lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)"                                   by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))

lemma "n <= (n::real)"                                                          by (rule real_le_refl)

lemma "- (- z) = (z::real)"                                                     by (rule minus_minus)

lemma "z * w = w * (z::real)"                                                   by (rule real_mult_commute)

lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))"                                 by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))

lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))"                                   by (rule real_mult_assoc)

lemma "z + w = w + (z::real)"                                                   by (rule add_commute)

lemma "x + (y + z) = y + (x + (z::real))"                                       by (rule add_left_commute)

lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))"                                   by (rule add_assoc)

lemma "- (x1 * y1) = - x1 * (y1::real)"                                         by (rule minus_mult_left)

lemma "z + - z = (0::real)"                                                     by (rule right_minus)

lemma "z1 + (z2 + z3) = z1 + z2 + (z3::real)"                                   by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25))

lemma "- (x1 / y1) = - x1 / (y1::real)"                                         by (rule minus_divide_left)

lemma "x * (y / z) = x * y / (z::real)"                                         by (rule Fields.field_class.times_divide_eq(1))

lemma "x * (y / z) = x * y / (z::real)"                                         by (rule times_divide_eq_right)

lemma "y / z * x = y * x / (z::real)"                                           by (rule times_divide_eq_left)

lemma "x / y / z = x / (y * (z::real))"                                         by (rule divide_divide_eq_left)

lemma "x / (y / z) = x * z / (y::real)"                                         by (rule divide_divide_eq_right)

lemma "x / 1 = (x::real)"                                                       by (rule divide_1)

lemma "(z1 - z2) * w = z1 * w - z2 * (w::real)"                                 by (rule left_diff_distrib)

lemma "w * (z1 - z2) = w * z1 - w * (z2::real)"                                 by (rule right_diff_distrib)

lemma "(x + y) / z = x / z + y / (z::real)"                                     by (rule add_divide_distrib)

end