| author | boehmes |
| Tue, 27 Mar 2012 17:11:02 +0200 | |
| changeset 47155 | ade3fc826af3 |
| parent 46787 | 3d3d8f8929a7 |
| permissions | -rw-r--r-- |
| 14516 | 1 |
import |
2 |
||
3 |
import_segment "hol4" |
|
4 |
||
5 |
def_maps |
|
6 |
"sup" > "sup_def" |
|
7 |
"sumc" > "sumc_def" |
|
8 |
"sum" > "sum_def" |
|
9 |
||
10 |
const_maps |
|
11 |
"sup" > "HOL4Real.real.sup" |
|
12 |
"sum" > "HOL4Real.real.sum" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
13 |
"real_sub" > "Groups.minus_class.minus" :: "real => real => real" |
| 14516 | 14 |
"real_of_num" > "RealDef.real" :: "nat => real" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
15 |
"real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
16 |
"real_gt" > "Compatibility.real_gt" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
17 |
"real_ge" > "Compatibility.real_ge" |
| 24996 | 18 |
"pow" > "Power.power_class.power" :: "real => nat => real" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
19 |
"abs" > "Groups.abs_class.abs" :: "real => real" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
20 |
"/" > "Fields.inverse_class.divide" :: "real => real => real" |
| 14516 | 21 |
|
22 |
thm_maps |
|
23 |
"sup_def" > "HOL4Real.real.sup_def" |
|
24 |
"sup" > "HOL4Real.real.sup" |
|
25 |
"sumc" > "HOL4Real.real.sumc" |
|
26 |
"sum_def" > "HOL4Real.real.sum_def" |
|
27 |
"sum" > "HOL4Real.real.sum" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
28 |
"real_sub" > "Fields.linordered_field_class.sign_simps_16" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
29 |
"real_of_num" > "Compatibility.real_of_num" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
30 |
"real_lte" > "Compatibility.real_lte" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
31 |
"real_lt" > "Orderings.linorder_class.not_le" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
32 |
"real_gt" > "Compatibility.GREATER_DEF" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
33 |
"real_ge" > "Compatibility.real_ge" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
34 |
"real_div" > "Fields.division_ring_class.divide_inverse" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
35 |
"pow" > "Compatibility.pow" |
|
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
36 |
"abs" > "Compatibility.abs" |
| 14516 | 37 |
"SUP_LEMMA3" > "HOL4Real.real.SUP_LEMMA3" |
38 |
"SUP_LEMMA2" > "HOL4Real.real.SUP_LEMMA2" |
|
39 |
"SUP_LEMMA1" > "HOL4Real.real.SUP_LEMMA1" |
|
40 |
"SUM_ZERO" > "HOL4Real.real.SUM_ZERO" |
|
41 |
"SUM_TWO" > "HOL4Real.real.SUM_TWO" |
|
42 |
"SUM_SUBST" > "HOL4Real.real.SUM_SUBST" |
|
43 |
"SUM_SUB" > "HOL4Real.real.SUM_SUB" |
|
44 |
"SUM_REINDEX" > "HOL4Real.real.SUM_REINDEX" |
|
45 |
"SUM_POS_GEN" > "HOL4Real.real.SUM_POS_GEN" |
|
46 |
"SUM_POS" > "HOL4Real.real.SUM_POS" |
|
47 |
"SUM_PERMUTE_0" > "HOL4Real.real.SUM_PERMUTE_0" |
|
48 |
"SUM_OFFSET" > "HOL4Real.real.SUM_OFFSET" |
|
49 |
"SUM_NSUB" > "HOL4Real.real.SUM_NSUB" |
|
50 |
"SUM_NEG" > "HOL4Real.real.SUM_NEG" |
|
51 |
"SUM_LE" > "HOL4Real.real.SUM_LE" |
|
52 |
"SUM_GROUP" > "HOL4Real.real.SUM_GROUP" |
|
53 |
"SUM_EQ" > "HOL4Real.real.SUM_EQ" |
|
54 |
"SUM_DIFF" > "HOL4Real.real.SUM_DIFF" |
|
55 |
"SUM_DEF" > "HOL4Real.real.SUM_DEF" |
|
56 |
"SUM_CMUL" > "HOL4Real.real.SUM_CMUL" |
|
57 |
"SUM_CANCEL" > "HOL4Real.real.SUM_CANCEL" |
|
58 |
"SUM_BOUND" > "HOL4Real.real.SUM_BOUND" |
|
59 |
"SUM_ADD" > "HOL4Real.real.SUM_ADD" |
|
60 |
"SUM_ABS_LE" > "HOL4Real.real.SUM_ABS_LE" |
|
61 |
"SUM_ABS" > "HOL4Real.real.SUM_ABS" |
|
62 |
"SUM_2" > "HOL4Real.real.SUM_2" |
|
63 |
"SUM_1" > "HOL4Real.real.SUM_1" |
|
64 |
"SUM_0" > "HOL4Real.real.SUM_0" |
|
65 |
"SETOK_LE_LT" > "HOL4Real.real.SETOK_LE_LT" |
|
66 |
"REAL_SUP_UBOUND_LE" > "HOL4Real.real.REAL_SUP_UBOUND_LE" |
|
67 |
"REAL_SUP_UBOUND" > "HOL4Real.real.REAL_SUP_UBOUND" |
|
68 |
"REAL_SUP_SOMEPOS" > "HOL4Real.real.REAL_SUP_SOMEPOS" |
|
69 |
"REAL_SUP_LE" > "HOL4Real.real.REAL_SUP_LE" |
|
70 |
"REAL_SUP_EXISTS" > "HOL4Real.real.REAL_SUP_EXISTS" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
71 |
"REAL_SUP_ALLPOS" > "Compatibility.REAL_SUP_ALLPOS" |
| 14516 | 72 |
"REAL_SUP" > "HOL4Real.real.REAL_SUP" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
73 |
"REAL_SUMSQ" > "Nat_Numeral.linordered_ring_strict_class.sum_squares_eq_zero_iff" |
| 14516 | 74 |
"REAL_SUB_TRIANGLE" > "HOL4Real.real.REAL_SUB_TRIANGLE" |
75 |
"REAL_SUB_SUB2" > "HOL4Real.real.REAL_SUB_SUB2" |
|
76 |
"REAL_SUB_SUB" > "HOL4Real.real.REAL_SUB_SUB" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
77 |
"REAL_SUB_RZERO" > "Groups.group_add_class.diff_0_right" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
78 |
"REAL_SUB_RNEG" > "Groups.group_add_class.diff_minus_eq_add" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
79 |
"REAL_SUB_REFL" > "Groups.group_add_class.diff_self" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
80 |
"REAL_SUB_RDISTRIB" > "Fields.linordered_field_class.sign_simps_5" |
| 14516 | 81 |
"REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
82 |
"REAL_SUB_LZERO" > "Groups.group_add_class.diff_0" |
| 15647 | 83 |
"REAL_SUB_LT" > "HOL4Real.real.REAL_SUB_LT" |
| 14516 | 84 |
"REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG" |
| 15647 | 85 |
"REAL_SUB_LE" > "HOL4Real.real.REAL_SUB_LE" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
86 |
"REAL_SUB_LDISTRIB" > "Fields.linordered_field_class.sign_simps_6" |
| 14516 | 87 |
"REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2" |
| 14796 | 88 |
"REAL_SUB_ADD2" > "HOL4Real.real.REAL_SUB_ADD2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
89 |
"REAL_SUB_ADD" > "Groups.group_add_class.diff_add_cancel" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
90 |
"REAL_SUB_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq2" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
91 |
"REAL_SUB_0" > "Groups.ab_group_add_class.diff_eq_0_iff_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
92 |
"REAL_RNEG_UNIQ" > "Groups.group_add_class.add_eq_0_iff" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
93 |
"REAL_RINV_UNIQ" > "Fields.division_ring_class.inverse_unique" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
94 |
"REAL_RDISTRIB" > "Fields.linordered_field_class.sign_simps_8" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
95 |
"REAL_POW_POW" > "Power.monoid_mult_class.power_mult" |
| 17188 | 96 |
"REAL_POW_MONO_LT" > "HOL4Real.real.REAL_POW_MONO_LT" |
| 14516 | 97 |
"REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
98 |
"REAL_POW_LT" > "Power.linordered_semidom_class.zero_less_power" |
| 14516 | 99 |
"REAL_POW_INV" > "Power.power_inverse" |
100 |
"REAL_POW_DIV" > "Power.power_divide" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
101 |
"REAL_POW_ADD" > "Power.monoid_mult_class.power_add" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
102 |
"REAL_POW2_ABS" > "Nat_Numeral.linordered_idom_class.power2_abs" |
| 14516 | 103 |
"REAL_POS_NZ" > "HOL4Real.real.REAL_POS_NZ" |
104 |
"REAL_POS" > "RealDef.real_of_nat_ge_zero" |
|
105 |
"REAL_POASQ" > "HOL4Real.real.REAL_POASQ" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
106 |
"REAL_OVER1" > "Fields.division_ring_class.divide_1" |
| 14516 | 107 |
"REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc" |
|
35344
e0b46cd72414
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents:
35267
diff
changeset
|
108 |
"REAL_OF_NUM_POW" > "RealDef.power_real_of_nat" |
| 14516 | 109 |
"REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult" |
110 |
"REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff" |
|
111 |
"REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject" |
|
112 |
"REAL_OF_NUM_ADD" > "RealDef.real_of_nat_add" |
|
113 |
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT" |
|
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
114 |
"REAL_NOT_LT" > "Compatibility.real_lte" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
115 |
"REAL_NOT_LE" > "Orderings.linorder_class.not_le" |
|
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
44763
diff
changeset
|
116 |
"REAL_NEG_SUB" > "Groups.group_add_class.minus_diff_eq" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
117 |
"REAL_NEG_RMUL" > "Int.int_arith_rules_14" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
118 |
"REAL_NEG_NEG" > "Groups.group_add_class.minus_minus" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
119 |
"REAL_NEG_MUL2" > "Rings.ring_class.minus_mult_minus" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
120 |
"REAL_NEG_MINUS1" > "Semiring_Normalization.comm_ring_1_class.normalizing_ring_rules_1" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
121 |
"REAL_NEG_LT0" > "Groups.ordered_ab_group_add_class.neg_less_0_iff_less" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
122 |
"REAL_NEG_LMUL" > "Int.int_arith_rules_13" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
123 |
"REAL_NEG_LE0" > "Groups.ordered_ab_group_add_class.neg_le_0_iff_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
124 |
"REAL_NEG_INV" > "Fields.division_ring_class.nonzero_inverse_minus_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
125 |
"REAL_NEG_GT0" > "Groups.ordered_ab_group_add_class.neg_0_less_iff_less" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
126 |
"REAL_NEG_GE0" > "Groups.ordered_ab_group_add_class.neg_0_le_iff_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
127 |
"REAL_NEG_EQ0" > "Groups.group_add_class.neg_equal_0_iff_equal" |
| 14516 | 128 |
"REAL_NEG_EQ" > "HOL4Real.real.REAL_NEG_EQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
129 |
"REAL_NEG_ADD" > "Groups.ab_group_add_class.minus_add_distrib" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
130 |
"REAL_NEG_0" > "Groups.group_add_class.minus_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
131 |
"REAL_NEGNEG" > "Groups.group_add_class.minus_minus" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
132 |
"REAL_MUL_SYM" > "Fields.linordered_field_class.sign_simps_21" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
133 |
"REAL_MUL_RZERO" > "Divides.arithmetic_simps_41" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
134 |
"REAL_MUL_RNEG" > "Int.int_arith_rules_14" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
135 |
"REAL_MUL_RINV" > "Fields.division_ring_class.right_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
136 |
"REAL_MUL_RID" > "Divides.arithmetic_simps_43" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
137 |
"REAL_MUL_LZERO" > "Divides.arithmetic_simps_40" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
138 |
"REAL_MUL_LNEG" > "Int.int_arith_rules_13" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
139 |
"REAL_MUL_LINV" > "Fields.division_ring_class.left_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
140 |
"REAL_MUL_LID" > "Divides.arithmetic_simps_42" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
141 |
"REAL_MUL_ASSOC" > "Fields.linordered_field_class.sign_simps_22" |
| 14516 | 142 |
"REAL_MUL" > "RealDef.real_of_nat_mult" |
143 |
"REAL_MIDDLE2" > "HOL4Real.real.REAL_MIDDLE2" |
|
144 |
"REAL_MIDDLE1" > "HOL4Real.real.REAL_MIDDLE1" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
145 |
"REAL_MEAN" > "Orderings.dense_linorder_class.dense" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
146 |
"REAL_LT_TRANS" > "Orderings.order_less_trans" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
147 |
"REAL_LT_TOTAL" > "Compatibility.REAL_LT_TOTAL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
148 |
"REAL_LT_SUB_RADD" > "Fields.linordered_field_class.sign_simps_4" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
149 |
"REAL_LT_SUB_LADD" > "Fields.linordered_field_class.sign_simps_3" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
150 |
"REAL_LT_RMUL_IMP" > "Rings.linordered_semiring_strict_class.mult_strict_right_mono" |
| 14516 | 151 |
"REAL_LT_RMUL_0" > "HOL4Real.real.REAL_LT_RMUL_0" |
152 |
"REAL_LT_RMUL" > "RealDef.real_mult_less_iff1" |
|
| 15647 | 153 |
"REAL_LT_REFL" > "Orderings.order_less_irrefl" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
154 |
"REAL_LT_RDIV_EQ" > "Fields.linordered_field_class.pos_less_divide_eq" |
| 14516 | 155 |
"REAL_LT_RDIV_0" > "HOL4Real.real.REAL_LT_RDIV_0" |
156 |
"REAL_LT_RDIV" > "HOL4Real.real.REAL_LT_RDIV" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
157 |
"REAL_LT_RADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right" |
| 14516 | 158 |
"REAL_LT_NZ" > "HOL4Real.real.REAL_LT_NZ" |
159 |
"REAL_LT_NEGTOTAL" > "HOL4Real.real.REAL_LT_NEGTOTAL" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
160 |
"REAL_LT_NEG" > "Groups.ordered_ab_group_add_class.neg_less_iff_less" |
| 14516 | 161 |
"REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
162 |
"REAL_LT_MUL2" > "Rings.linordered_semiring_strict_class.mult_strict_mono'" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
163 |
"REAL_LT_MUL" > "RealDef.real_mult_order" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
164 |
"REAL_LT_LMUL_IMP" > "RealDef.real_mult_less_mono2" |
| 14516 | 165 |
"REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
166 |
"REAL_LT_LMUL" > "Rings.linordered_ring_strict_class.mult_less_cancel_left_pos" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
167 |
"REAL_LT_LE" > "Orderings.order_class.less_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
168 |
"REAL_LT_LDIV_EQ" > "Fields.linordered_field_class.pos_divide_less_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
169 |
"REAL_LT_LADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_left" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
170 |
"REAL_LT_INV_EQ" > "Fields.linordered_field_inverse_zero_class.inverse_positive_iff_positive" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
171 |
"REAL_LT_INV" > "Fields.linordered_field_class.less_imp_inverse_less" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
172 |
"REAL_LT_IMP_NE" > "Orderings.order_class.less_imp_neq" |
| 15647 | 173 |
"REAL_LT_IMP_LE" > "Orderings.order_less_imp_le" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
174 |
"REAL_LT_IADD" > "Groups.ordered_cancel_ab_semigroup_add_class.add_strict_left_mono" |
| 14516 | 175 |
"REAL_LT_HALF2" > "HOL4Real.real.REAL_LT_HALF2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
176 |
"REAL_LT_HALF1" > "Int.half_gt_zero_iff" |
| 15647 | 177 |
"REAL_LT_GT" > "Orderings.order_less_not_sym" |
| 14516 | 178 |
"REAL_LT_FRACTION_0" > "HOL4Real.real.REAL_LT_FRACTION_0" |
179 |
"REAL_LT_FRACTION" > "HOL4Real.real.REAL_LT_FRACTION" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
180 |
"REAL_LT_DIV" > "Fields.linordered_field_class.divide_pos_pos" |
| 14516 | 181 |
"REAL_LT_ANTISYM" > "HOL4Real.real.REAL_LT_ANTISYM" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
182 |
"REAL_LT_ADD_SUB" > "Fields.linordered_field_class.sign_simps_3" |
| 14516 | 183 |
"REAL_LT_ADDR" > "HOL4Real.real.REAL_LT_ADDR" |
184 |
"REAL_LT_ADDNEG2" > "HOL4Real.real.REAL_LT_ADDNEG2" |
|
185 |
"REAL_LT_ADDNEG" > "HOL4Real.real.REAL_LT_ADDNEG" |
|
186 |
"REAL_LT_ADDL" > "HOL4Real.real.REAL_LT_ADDL" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
187 |
"REAL_LT_ADD2" > "Groups.add_mono_thms_linordered_field_5" |
| 14516 | 188 |
"REAL_LT_ADD1" > "HOL4Real.real.REAL_LT_ADD1" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
189 |
"REAL_LT_ADD" > "Groups.ordered_comm_monoid_add_class.add_pos_pos" |
| 14516 | 190 |
"REAL_LT_1" > "HOL4Real.real.REAL_LT_1" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
191 |
"REAL_LT_01" > "Rings.linordered_semidom_class.zero_less_one" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
192 |
"REAL_LTE_TRANS" > "Orderings.order_less_le_trans" |
| 14516 | 193 |
"REAL_LTE_TOTAL" > "HOL4Real.real.REAL_LTE_TOTAL" |
194 |
"REAL_LTE_ANTSYM" > "HOL4Real.real.REAL_LTE_ANTSYM" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
195 |
"REAL_LTE_ADD2" > "Groups.add_mono_thms_linordered_field_3" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
196 |
"REAL_LTE_ADD" > "Groups.ordered_comm_monoid_add_class.add_pos_nonneg" |
| 14516 | 197 |
"REAL_LT1_POW2" > "HOL4Real.real.REAL_LT1_POW2" |
198 |
"REAL_LT" > "RealDef.real_of_nat_less_iff" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
199 |
"REAL_LNEG_UNIQ" > "Groups.group_add_class.eq_neg_iff_add_eq_0" |
| 14516 | 200 |
"REAL_LINV_UNIQ" > "HOL4Real.real.REAL_LINV_UNIQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
201 |
"REAL_LE_TRANS" > "Orderings.order_trans_rules_23" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
202 |
"REAL_LE_TOTAL" > "Orderings.linorder_class.linear" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
203 |
"REAL_LE_SUB_RADD" > "Fields.linordered_field_class.sign_simps_2" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
204 |
"REAL_LE_SUB_LADD" > "Fields.linordered_field_class.sign_simps_1" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
205 |
"REAL_LE_SQUARE" > "Rings.linordered_ring_class.zero_le_square" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
206 |
"REAL_LE_RNEG" > "HOL4Real.real.REAL_LE_RNEG" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
207 |
"REAL_LE_RMUL_IMP" > "Rings.ordered_semiring_class.mult_right_mono" |
| 14516 | 208 |
"REAL_LE_RMUL" > "RealDef.real_mult_le_cancel_iff1" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
209 |
"REAL_LE_REFL" > "Orderings.preorder_class.order_refl" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
210 |
"REAL_LE_RDIV_EQ" > "Fields.linordered_field_class.pos_le_divide_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
211 |
"REAL_LE_RDIV" > "Fields.linordered_field_class.mult_imp_le_div_pos" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
212 |
"REAL_LE_RADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
213 |
"REAL_LE_POW2" > "Nat_Numeral.linordered_idom_class.zero_le_power2" |
| 14516 | 214 |
"REAL_LE_NEGTOTAL" > "HOL4Real.real.REAL_LE_NEGTOTAL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
215 |
"REAL_LE_NEGR" > "Groups.linordered_ab_group_add_class.le_minus_self_iff" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
216 |
"REAL_LE_NEGL" > "Groups.linordered_ab_group_add_class.minus_le_self_iff" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
217 |
"REAL_LE_NEG2" > "Groups.ordered_ab_group_add_class.neg_le_iff_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
218 |
"REAL_LE_NEG" > "Groups.ordered_ab_group_add_class.neg_le_iff_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
219 |
"REAL_LE_MUL2" > "Rings.ordered_semiring_class.mult_mono'" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
220 |
"REAL_LE_MUL" > "Rings.mult_sign_intros_1" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
221 |
"REAL_LE_LT" > "Orderings.order_class.le_less" |
| 14516 | 222 |
"REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
223 |
"REAL_LE_LMUL_IMP" > "Rings.ordered_comm_semiring_class.comm_mult_left_mono" |
| 14516 | 224 |
"REAL_LE_LMUL" > "RealDef.real_mult_le_cancel_iff2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
225 |
"REAL_LE_LDIV_EQ" > "Fields.linordered_field_class.pos_divide_le_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
226 |
"REAL_LE_LDIV" > "Fields.linordered_field_class.mult_imp_div_pos_le" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
227 |
"REAL_LE_LADD_IMP" > "Groups.ordered_ab_semigroup_add_class.add_left_mono" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
228 |
"REAL_LE_LADD" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
229 |
"REAL_LE_INV_EQ" > "Fields.linordered_field_inverse_zero_class.inverse_nonnegative_iff_nonnegative" |
| 14516 | 230 |
"REAL_LE_INV" > "HOL4Real.real.REAL_LE_INV" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
231 |
"REAL_LE_DOUBLE" > "Groups.linordered_ab_group_add_class.zero_le_double_add_iff_zero_le_single_add" |
| 14516 | 232 |
"REAL_LE_DIV" > "HOL4Real.real.REAL_LE_DIV" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
233 |
"REAL_LE_ANTISYM" > "Orderings.order_class.eq_iff" |
| 14516 | 234 |
"REAL_LE_ADDR" > "HOL4Real.real.REAL_LE_ADDR" |
235 |
"REAL_LE_ADDL" > "HOL4Real.real.REAL_LE_ADDL" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
236 |
"REAL_LE_ADD2" > "Groups.add_mono_thms_linordered_semiring_1" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
237 |
"REAL_LE_ADD" > "Groups.ordered_comm_monoid_add_class.add_nonneg_nonneg" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
238 |
"REAL_LE_01" > "Rings.linordered_semidom_class.zero_le_one" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
239 |
"REAL_LET_TRANS" > "Orderings.order_le_less_trans" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
240 |
"REAL_LET_TOTAL" > "Orderings.linorder_class.le_less_linear" |
| 14516 | 241 |
"REAL_LET_ANTISYM" > "HOL4Real.real.REAL_LET_ANTISYM" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
242 |
"REAL_LET_ADD2" > "Groups.add_mono_thms_linordered_field_4" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
243 |
"REAL_LET_ADD" > "Groups.ordered_comm_monoid_add_class.add_nonneg_pos" |
| 14516 | 244 |
"REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2" |
245 |
"REAL_LE" > "RealDef.real_of_nat_le_iff" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
246 |
"REAL_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
247 |
"REAL_INV_POS" > "Fields.linordered_field_class.positive_imp_inverse_positive" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
248 |
"REAL_INV_NZ" > "Fields.division_ring_class.nonzero_imp_inverse_nonzero" |
| 14516 | 249 |
"REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
250 |
"REAL_INV_LT1" > "Fields.linordered_field_class.one_less_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
251 |
"REAL_INV_INV" > "Fields.division_ring_inverse_zero_class.inverse_inverse_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
252 |
"REAL_INV_EQ_0" > "Fields.division_ring_inverse_zero_class.inverse_nonzero_iff_nonzero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
253 |
"REAL_INV_1OVER" > "Fields.division_ring_class.inverse_eq_divide" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
254 |
"REAL_INV_0" > "Fields.division_ring_inverse_zero_class.inverse_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
255 |
"REAL_INVINV" > "Fields.division_ring_class.nonzero_inverse_inverse_eq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
256 |
"REAL_INV1" > "Fields.division_ring_class.inverse_1" |
| 14516 | 257 |
"REAL_INJ" > "RealDef.real_of_nat_inject" |
258 |
"REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves" |
|
259 |
"REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
260 |
"REAL_EQ_SUB_RADD" > "Fields.linordered_field_class.sign_simps_12" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
261 |
"REAL_EQ_SUB_LADD" > "Fields.linordered_field_class.sign_simps_11" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
262 |
"REAL_EQ_RMUL_IMP" > "HOL4Real.real.REAL_EQ_RMUL_IMP" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
263 |
"REAL_EQ_RMUL" > "Rings.mult_compare_simps_13" |
| 14516 | 264 |
"REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
265 |
"REAL_EQ_RADD" > "Groups.cancel_semigroup_add_class.add_right_cancel" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
266 |
"REAL_EQ_NEG" > "Groups.group_add_class.neg_equal_iff_equal" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
267 |
"REAL_EQ_MUL_LCANCEL" > "Rings.mult_compare_simps_14" |
| 14516 | 268 |
"REAL_EQ_LMUL_IMP" > "HOL4Real.real.REAL_EQ_LMUL_IMP" |
269 |
"REAL_EQ_LMUL2" > "RealDef.real_mult_left_cancel" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
270 |
"REAL_EQ_LMUL" > "Rings.mult_compare_simps_14" |
| 14516 | 271 |
"REAL_EQ_LDIV_EQ" > "HOL4Real.real.REAL_EQ_LDIV_EQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
272 |
"REAL_EQ_LADD" > "Groups.cancel_semigroup_add_class.add_left_cancel" |
| 15647 | 273 |
"REAL_EQ_IMP_LE" > "Orderings.order_eq_refl" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
274 |
"REAL_ENTIRE" > "Rings.ring_no_zero_divisors_class.mult_eq_0_iff" |
| 14516 | 275 |
"REAL_DOWN2" > "RealDef.real_lbound_gt_zero" |
276 |
"REAL_DOWN" > "HOL4Real.real.REAL_DOWN" |
|
| 25930 | 277 |
"REAL_DOUBLE" > "Int.mult_2" |
| 14516 | 278 |
"REAL_DIV_RMUL" > "HOL4Real.real.REAL_DIV_RMUL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
279 |
"REAL_DIV_REFL" > "Fields.division_ring_class.divide_self" |
| 17188 | 280 |
"REAL_DIV_MUL2" > "HOL4Real.real.REAL_DIV_MUL2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
281 |
"REAL_DIV_LZERO" > "Fields.division_ring_class.divide_zero_left" |
| 14516 | 282 |
"REAL_DIV_LMUL" > "HOL4Real.real.REAL_DIV_LMUL" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
283 |
"REAL_DIFFSQ" > "Rings.comm_ring_class.square_diff_square_factored" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
284 |
"REAL_ARCH_LEAST" > "Transcendental.reals_Archimedean4" |
| 14516 | 285 |
"REAL_ARCH" > "RComplete.reals_Archimedean3" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
286 |
"REAL_ADD_SYM" > "Fields.linordered_field_class.sign_simps_18" |
| 14516 | 287 |
"REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2" |
| 14796 | 288 |
"REAL_ADD_SUB" > "HOL4Real.real.REAL_ADD_SUB" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
289 |
"REAL_ADD_RINV" > "Groups.group_add_class.right_minus" |
| 14516 | 290 |
"REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
291 |
"REAL_ADD_RID" > "Divides.arithmetic_simps_39" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
292 |
"REAL_ADD_RDISTRIB" > "Fields.linordered_field_class.sign_simps_8" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
293 |
"REAL_ADD_LINV" > "Groups.ab_group_add_class.ab_left_minus" |
| 14516 | 294 |
"REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
295 |
"REAL_ADD_LID" > "Divides.arithmetic_simps_38" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
296 |
"REAL_ADD_LDISTRIB" > "Fields.linordered_field_class.sign_simps_7" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
297 |
"REAL_ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_19" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
298 |
"REAL_ADD2_SUB2" > "RealDef.add_diff_add" |
| 14516 | 299 |
"REAL_ADD" > "RealDef.real_of_nat_add" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
300 |
"REAL_ABS_TRIANGLE" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
301 |
"REAL_ABS_POS" > "Groups.ordered_ab_group_add_abs_class.abs_ge_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
302 |
"REAL_ABS_MUL" > "Rings.linordered_idom_class.abs_mult" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
303 |
"REAL_ABS_0" > "Divides.arithmetic_simps_27" |
|
46787
3d3d8f8929a7
file system structure separating HOL4 and HOL Light concerns
haftmann
parents:
45548
diff
changeset
|
304 |
"REAL_10" > "Compatibility.REAL_10" |
| 14516 | 305 |
"REAL_1" > "HOL4Real.real.REAL_1" |
306 |
"REAL_0" > "HOL4Real.real.REAL_0" |
|
307 |
"REAL" > "RealDef.real_of_nat_Suc" |
|
308 |
"POW_ZERO_EQ" > "HOL4Real.real.POW_ZERO_EQ" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
309 |
"POW_ZERO" > "HOL4Real.real.POW_ZERO" |
| 14516 | 310 |
"POW_POS_LT" > "HOL4Real.real.POW_POS_LT" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
311 |
"POW_POS" > "Power.linordered_semidom_class.zero_le_power" |
| 14516 | 312 |
"POW_PLUS1" > "HOL4Real.real.POW_PLUS1" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
313 |
"POW_ONE" > "Power.monoid_mult_class.power_one" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
314 |
"POW_NZ" > "Power.ring_1_no_zero_divisors_class.field_power_not_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
315 |
"POW_MUL" > "Power.comm_monoid_mult_class.power_mult_distrib" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
316 |
"POW_MINUS1" > "Nat_Numeral.ring_1_class.power_minus1_even" |
| 14516 | 317 |
"POW_M1" > "HOL4Real.real.POW_M1" |
318 |
"POW_LT" > "HOL4Real.real.POW_LT" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
319 |
"POW_LE" > "Power.linordered_semidom_class.power_mono" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
320 |
"POW_INV" > "Power.division_ring_class.nonzero_power_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
321 |
"POW_EQ" > "Power.linordered_semidom_class.power_inject_base" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
322 |
"POW_ADD" > "Power.monoid_mult_class.power_add" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
323 |
"POW_ABS" > "Power.linordered_idom_class.power_abs" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
324 |
"POW_2_LT" > "RealDef.two_realpow_gt" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
325 |
"POW_2_LE1" > "RealDef.two_realpow_ge_one" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
326 |
"POW_2" > "Nat_Numeral.monoid_mult_class.power2_eq_square" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
327 |
"POW_1" > "Power.monoid_mult_class.power_one_right" |
| 14516 | 328 |
"POW_0" > "Power.power_0_Suc" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
329 |
"ABS_ZERO" > "Groups.ordered_ab_group_add_abs_class.abs_eq_0" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
330 |
"ABS_TRIANGLE" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq" |
| 14516 | 331 |
"ABS_SUM" > "HOL4Real.real.ABS_SUM" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
332 |
"ABS_SUB_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_triangle_ineq3" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
333 |
"ABS_SUB" > "Groups.ordered_ab_group_add_abs_class.abs_minus_commute" |
| 14516 | 334 |
"ABS_STILLNZ" > "HOL4Real.real.ABS_STILLNZ" |
335 |
"ABS_SIGN2" > "HOL4Real.real.ABS_SIGN2" |
|
336 |
"ABS_SIGN" > "HOL4Real.real.ABS_SIGN" |
|
337 |
"ABS_REFL" > "HOL4Real.real.ABS_REFL" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
338 |
"ABS_POW2" > "Nat_Numeral.linordered_idom_class.abs_power2" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
339 |
"ABS_POS" > "Groups.ordered_ab_group_add_abs_class.abs_ge_zero" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
340 |
"ABS_NZ" > "Groups.ordered_ab_group_add_abs_class.zero_less_abs_iff" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
341 |
"ABS_NEG" > "Groups.ordered_ab_group_add_abs_class.abs_minus_cancel" |
| 14516 | 342 |
"ABS_N" > "RealDef.abs_real_of_nat_cancel" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
343 |
"ABS_MUL" > "Rings.linordered_idom_class.abs_mult" |
| 14516 | 344 |
"ABS_LT_MUL2" > "HOL4Real.real.ABS_LT_MUL2" |
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
345 |
"ABS_LE" > "Groups.ordered_ab_group_add_abs_class.abs_ge_self" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
346 |
"ABS_INV" > "Fields.linordered_field_class.nonzero_abs_inverse" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
347 |
"ABS_DIV" > "Fields.linordered_field_class.nonzero_abs_divide" |
| 14516 | 348 |
"ABS_CIRCLE" > "HOL4Real.real.ABS_CIRCLE" |
349 |
"ABS_CASES" > "HOL4Real.real.ABS_CASES" |
|
350 |
"ABS_BOUNDS" > "RealDef.abs_le_interval_iff" |
|
351 |
"ABS_BOUND" > "HOL4Real.real.ABS_BOUND" |
|
352 |
"ABS_BETWEEN2" > "HOL4Real.real.ABS_BETWEEN2" |
|
353 |
"ABS_BETWEEN1" > "HOL4Real.real.ABS_BETWEEN1" |
|
354 |
"ABS_BETWEEN" > "HOL4Real.real.ABS_BETWEEN" |
|
|
44763
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
355 |
"ABS_ABS" > "Groups.ordered_ab_group_add_abs_class.abs_idempotent" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
356 |
"ABS_1" > "Divides.arithmetic_simps_28" |
|
b50d5d694838
HOL/Import: Update HOL4 generated files to current Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37887
diff
changeset
|
357 |
"ABS_0" > "Divides.arithmetic_simps_27" |
| 14516 | 358 |
|
359 |
end |