|
neuper@42385
|
1 |
WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
|
|
neuper@42390
|
2 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42390
|
3 |
find_theorems: in emacs
|
|
neuper@42390
|
4 |
(999) name :
|
|
neuper@42390
|
5 |
(999) simp : "?a * (?b + ?c)"
|
|
neuper@42390
|
6 |
Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
|
|
neuper@42390
|
7 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42399
|
8 |
"?r1 * ?r1 = ?r1 ^^^ 2" ... "_ * _ = _ ^^^ _ "
|
|
neuper@42399
|
9 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42390
|
10 |
|
|
neuper@42390
|
11 |
(1) ======================================================================= + ===========
|
|
neuper@42385
|
12 |
Isabelle2002-isac Isabelle2009-2
|
|
neuper@42385
|
13 |
ok
|
|
neuper@42385
|
14 |
\ to be checked
|
|
neuper@42385
|
15 |
\? still misterious
|
|
neuper@42385
|
16 |
# better would be the *_class.*(n)
|
|
neuper@42385
|
17 |
// no rule outside *_class.*(n)
|
|
neuper@42385
|
18 |
> rlsthmsNOTisac;
|
|
neuper@42385
|
19 |
val it =
|
|
neuper@42385
|
20 |
[("refl", "?t = ?t"), HOL.refl
|
|
neuper@42385
|
21 |
("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply
|
|
neuper@42385
|
22 |
("take_Nil", "take ?n [] = []"), List.take_Nil
|
|
neuper@42385
|
23 |
("take_Cons", List.take_Cons
|
|
neuper@42385
|
24 |
"take ?n (?x # ?xs) =
|
|
neuper@42385
|
25 |
(case ?n of 0 => [] | Suc m => ?x # take m ?xs)"),
|
|
neuper@42385
|
26 |
("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True
|
|
neuper@42385
|
27 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
28 |
("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
|
|
neuper@42385
|
29 |
("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
|
|
neuper@52062
|
30 |
("real_add_mult_distrib", Rings.semiring_class.distrib_right
|
|
neuper@42385
|
31 |
"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
|
|
neuper@52062
|
32 |
("real_add_mult_distrib2", Rings.semiring_class.distrib_left
|
|
neuper@42385
|
33 |
"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
|
|
neuper@42385
|
34 |
("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
|
|
neuper@42399
|
35 |
Poly.realpow_two_atom: ?r is_atom \<Longrightarrow> ?r * ?r = ?r ^^^ 2
|
|
neuper@42385
|
36 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
37 |
("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)
|
|
neuper@42399
|
38 |
"?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]),
|
|
neuper@42399
|
39 |
Poly.realpow_addI_atom: ?r is_atom \<Longrightarrow> ?r ^^^ ?n * ?r ^^^ ?m = ?r ^^^ (?n + ?m)
|
|
neuper@42385
|
40 |
("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right
|
|
neuper@42385
|
41 |
("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1" [.]), #!^! Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4): ?m + ?m = ((1::?'a) + (1::?'a)) * ?m
|
|
neuper@42399
|
42 |
Test.rtwo_of_the_same -''- //
|
|
neuper@42385
|
43 |
("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left
|
|
neuper@42385
|
44 |
("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left
|
|
neuper@42385
|
45 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
46 |
("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right
|
|
neuper@42385
|
47 |
("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
|
|
neuper@42385
|
48 |
("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
|
|
neuper@42385
|
49 |
("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
|
|
neuper@48763
|
50 |
("sym_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
|
|
neuper@42385
|
51 |
"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
|
|
neuper@42399
|
52 |
PolyEq.real_assoc_2: c -''- //
|
|
neuper@42385
|
53 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
54 |
("le_refl", "?n <= ?n"), RealDef.real_le_refl
|
|
neuper@48764
|
55 |
2012: ?.order_refl
|
|
neuper@42385
|
56 |
("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
|
|
neuper@48764
|
57 |
("mult_commute", "?z * ?w = ?w * ?z"), 2011: RealDef.real_mult_commute
|
|
neuper@48764
|
58 |
2012 ?.mult_commute
|
|
neuper@42385
|
59 |
("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
|
|
neuper@42399
|
60 |
"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
|
|
neuper@42399
|
61 |
PolyEq.real_assoc_2 -''- //
|
|
neuper@48764
|
62 |
("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), 2011:RealDef.real_mult_assoc
|
|
neuper@48764
|
63 |
2012: ?.mult_assoc
|
|
neuper@42385
|
64 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
65 |
("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
|
|
neuper@42385
|
66 |
("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
|
|
neuper@42385
|
67 |
("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc
|
|
neuper@42385
|
68 |
("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left
|
|
neuper@42385
|
69 |
("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus
|
|
neuper@42385
|
70 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
71 |
("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc
|
|
neuper@42385
|
72 |
"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]),
|
|
neuper@42385
|
73 |
-''- //
|
|
neuper@42385
|
74 |
("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left
|
|
neuper@42385
|
75 |
("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1)
|
|
neuper@42385
|
76 |
-''- ! Rings.division_ring_class.times_divide_eq_right
|
|
neuper@42385
|
77 |
("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left
|
|
neuper@42385
|
78 |
("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left
|
|
neuper@42385
|
79 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
80 |
("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right
|
|
neuper@42385
|
81 |
("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1
|
|
neuper@42385
|
82 |
("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib
|
|
neuper@42385
|
83 |
"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"),
|
|
neuper@42385
|
84 |
("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib
|
|
neuper@42385
|
85 |
"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"),
|
|
neuper@42385
|
86 |
("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
|
|
neuper@42385
|
87 |
-----------------------------------------------------------------------------------------------------------------
|
|
neuper@42385
|
88 |
("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
|
|
neuper@48763
|
89 |
("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_mult_assoc
|
|
neuper@42385
|
90 |
: (thmID * Thm.thm) list
|
|
neuper@42390
|
91 |
|
|
neuper@42390
|
92 |
|
|
neuper@42390
|
93 |
(2) ===== thms in Scripts: ================================================ + ===========
|
|
neuper@42385
|
94 |
"real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
|
|
neuper@42387
|
95 |
"real_minus_eq_cancel", "(- ?a = - ?b) = (?a = ?b)" Groups.group_add_class.neg_equal_iff_equal:
|
|
neuper@42385
|
96 |
|
|
neuper@42385
|
97 |
"_ + (_ + (_::nat)) = _ + _ + _"
|
|
neuper@42385
|
98 |
|
|
neuper@42390
|
99 |
(3) ===== list funs: ====================================================== + ===========
|
|
neuper@42399
|
100 |
nth_Nil_ ListC.NTH_NIL
|
|
neuper@42399
|
101 |
nth_Cons_ ListC.NTH_CONS
|
|
neuper@42385
|
102 |
|
|
neuper@42399
|
103 |
length_Nil_ ListC.LENGTH_NIL
|
|
neuper@42399
|
104 |
length_Cons_ ListC.LENGTH_CONS
|
|
neuper@42390
|
105 |
|
|
neuper@42399
|
106 |
tl_Nil_ ListC.tl_Nil_
|
|
neuper@42399
|
107 |
tl_Cons_ ListC.tl_Cons_
|