|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"rsquarefree" > "rsquarefree_def"
|
|
|
7 |
"poly_order" > "poly_order_def"
|
|
|
8 |
"poly_neg" > "poly_neg_primdef"
|
|
|
9 |
"poly_mul" > "poly_mul_primdef"
|
|
|
10 |
"poly_exp" > "poly_exp_primdef"
|
|
|
11 |
"poly_divides" > "poly_divides_def"
|
|
|
12 |
"poly_diff_aux" > "poly_diff_aux_primdef"
|
|
|
13 |
"poly_add" > "poly_add_primdef"
|
|
|
14 |
"poly" > "poly_primdef"
|
|
|
15 |
"normalize" > "normalize_def"
|
|
|
16 |
"diff" > "diff_def"
|
|
|
17 |
"degree" > "degree_def"
|
|
|
18 |
"##" > "##_def"
|
|
|
19 |
|
|
|
20 |
const_maps
|
|
|
21 |
"rsquarefree" > "HOL4Real.poly.rsquarefree"
|
|
|
22 |
"poly_order" > "HOL4Real.poly.poly_order"
|
|
|
23 |
"poly_neg" > "HOL4Real.poly.poly_neg"
|
|
|
24 |
"poly_divides" > "HOL4Real.poly.poly_divides"
|
|
|
25 |
"diff" > "HOL4Real.poly.diff"
|
|
|
26 |
"degree" > "HOL4Real.poly.degree"
|
|
|
27 |
|
|
|
28 |
thm_maps
|
|
|
29 |
"rsquarefree_def" > "HOL4Real.poly.rsquarefree_def"
|
|
|
30 |
"rsquarefree" > "HOL4Real.poly.rsquarefree"
|
|
|
31 |
"poly_order_def" > "HOL4Real.poly.poly_order_def"
|
|
|
32 |
"poly_order" > "HOL4Real.poly.poly_order"
|
|
|
33 |
"poly_neg_primdef" > "HOL4Real.poly.poly_neg_primdef"
|
|
|
34 |
"poly_neg_def" > "HOL4Real.poly.poly_neg_def"
|
|
|
35 |
"poly_mul_def" > "HOL4Real.poly.poly_mul_def"
|
|
|
36 |
"poly_exp_def" > "HOL4Real.poly.poly_exp_def"
|
|
|
37 |
"poly_divides_def" > "HOL4Real.poly.poly_divides_def"
|
|
|
38 |
"poly_divides" > "HOL4Real.poly.poly_divides"
|
|
|
39 |
"poly_diff_def" > "HOL4Real.poly.poly_diff_def"
|
|
|
40 |
"poly_diff_aux_def" > "HOL4Real.poly.poly_diff_aux_def"
|
|
|
41 |
"poly_def" > "HOL4Real.poly.poly_def"
|
|
|
42 |
"poly_cmul_def" > "HOL4Real.poly.poly_cmul_def"
|
|
|
43 |
"poly_add_def" > "HOL4Real.poly.poly_add_def"
|
|
|
44 |
"normalize" > "HOL4Real.poly.normalize"
|
|
|
45 |
"diff_def" > "HOL4Real.poly.diff_def"
|
|
|
46 |
"degree_def" > "HOL4Real.poly.degree_def"
|
|
|
47 |
"degree" > "HOL4Real.poly.degree"
|
|
|
48 |
"RSQUAREFREE_ROOTS" > "HOL4Real.poly.RSQUAREFREE_ROOTS"
|
|
|
49 |
"RSQUAREFREE_DECOMP" > "HOL4Real.poly.RSQUAREFREE_DECOMP"
|
|
|
50 |
"POLY_ZERO_LEMMA" > "HOL4Real.poly.POLY_ZERO_LEMMA"
|
|
|
51 |
"POLY_ZERO" > "HOL4Real.poly.POLY_ZERO"
|
|
|
52 |
"POLY_SQUAREFREE_DECOMP_ORDER" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP_ORDER"
|
|
|
53 |
"POLY_SQUAREFREE_DECOMP" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP"
|
|
|
54 |
"POLY_ROOTS_INDEX_LENGTH" > "HOL4Real.poly.POLY_ROOTS_INDEX_LENGTH"
|
|
|
55 |
"POLY_ROOTS_INDEX_LEMMA" > "HOL4Real.poly.POLY_ROOTS_INDEX_LEMMA"
|
|
|
56 |
"POLY_ROOTS_FINITE_SET" > "HOL4Real.poly.POLY_ROOTS_FINITE_SET"
|
|
|
57 |
"POLY_ROOTS_FINITE_LEMMA" > "HOL4Real.poly.POLY_ROOTS_FINITE_LEMMA"
|
|
|
58 |
"POLY_ROOTS_FINITE" > "HOL4Real.poly.POLY_ROOTS_FINITE"
|
|
|
59 |
"POLY_PRIME_EQ_0" > "HOL4Real.poly.POLY_PRIME_EQ_0"
|
|
|
60 |
"POLY_PRIMES" > "HOL4Real.poly.POLY_PRIMES"
|
|
|
61 |
"POLY_ORDER_EXISTS" > "HOL4Real.poly.POLY_ORDER_EXISTS"
|
|
|
62 |
"POLY_ORDER" > "HOL4Real.poly.POLY_ORDER"
|
|
|
63 |
"POLY_NORMALIZE" > "HOL4Real.poly.POLY_NORMALIZE"
|
|
|
64 |
"POLY_NEG_CLAUSES" > "HOL4Real.poly.POLY_NEG_CLAUSES"
|
|
|
65 |
"POLY_NEG" > "HOL4Real.poly.POLY_NEG"
|
|
|
66 |
"POLY_MVT" > "HOL4Real.poly.POLY_MVT"
|
|
|
67 |
"POLY_MUL_LCANCEL" > "HOL4Real.poly.POLY_MUL_LCANCEL"
|
|
|
68 |
"POLY_MUL_CLAUSES" > "HOL4Real.poly.POLY_MUL_CLAUSES"
|
|
|
69 |
"POLY_MUL_ASSOC" > "HOL4Real.poly.POLY_MUL_ASSOC"
|
|
|
70 |
"POLY_MUL" > "HOL4Real.poly.POLY_MUL"
|
|
|
71 |
"POLY_MONO" > "HOL4Real.poly.POLY_MONO"
|
|
|
72 |
"POLY_LINEAR_REM" > "HOL4Real.poly.POLY_LINEAR_REM"
|
|
|
73 |
"POLY_LINEAR_DIVIDES" > "HOL4Real.poly.POLY_LINEAR_DIVIDES"
|
|
|
74 |
"POLY_LENGTH_MUL" > "HOL4Real.poly.POLY_LENGTH_MUL"
|
|
|
75 |
"POLY_IVT_POS" > "HOL4Real.poly.POLY_IVT_POS"
|
|
|
76 |
"POLY_IVT_NEG" > "HOL4Real.poly.POLY_IVT_NEG"
|
|
|
77 |
"POLY_EXP_PRIME_EQ_0" > "HOL4Real.poly.POLY_EXP_PRIME_EQ_0"
|
|
|
78 |
"POLY_EXP_EQ_0" > "HOL4Real.poly.POLY_EXP_EQ_0"
|
|
|
79 |
"POLY_EXP_DIVIDES" > "HOL4Real.poly.POLY_EXP_DIVIDES"
|
|
|
80 |
"POLY_EXP_ADD" > "HOL4Real.poly.POLY_EXP_ADD"
|
|
|
81 |
"POLY_EXP" > "HOL4Real.poly.POLY_EXP"
|
|
|
82 |
"POLY_ENTIRE_LEMMA" > "HOL4Real.poly.POLY_ENTIRE_LEMMA"
|
|
|
83 |
"POLY_ENTIRE" > "HOL4Real.poly.POLY_ENTIRE"
|
|
|
84 |
"POLY_DIVIDES_ZERO" > "HOL4Real.poly.POLY_DIVIDES_ZERO"
|
|
|
85 |
"POLY_DIVIDES_TRANS" > "HOL4Real.poly.POLY_DIVIDES_TRANS"
|
|
|
86 |
"POLY_DIVIDES_SUB2" > "HOL4Real.poly.POLY_DIVIDES_SUB2"
|
|
|
87 |
"POLY_DIVIDES_SUB" > "HOL4Real.poly.POLY_DIVIDES_SUB"
|
|
|
88 |
"POLY_DIVIDES_REFL" > "HOL4Real.poly.POLY_DIVIDES_REFL"
|
|
|
89 |
"POLY_DIVIDES_EXP" > "HOL4Real.poly.POLY_DIVIDES_EXP"
|
|
|
90 |
"POLY_DIVIDES_ADD" > "HOL4Real.poly.POLY_DIVIDES_ADD"
|
|
|
91 |
"POLY_DIFF_ZERO" > "HOL4Real.poly.POLY_DIFF_ZERO"
|
|
|
92 |
"POLY_DIFF_WELLDEF" > "HOL4Real.poly.POLY_DIFF_WELLDEF"
|
|
|
93 |
"POLY_DIFF_NEG" > "HOL4Real.poly.POLY_DIFF_NEG"
|
|
|
94 |
"POLY_DIFF_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_MUL_LEMMA"
|
|
|
95 |
"POLY_DIFF_MUL" > "HOL4Real.poly.POLY_DIFF_MUL"
|
|
|
96 |
"POLY_DIFF_LEMMA" > "HOL4Real.poly.POLY_DIFF_LEMMA"
|
|
|
97 |
"POLY_DIFF_ISZERO" > "HOL4Real.poly.POLY_DIFF_ISZERO"
|
|
|
98 |
"POLY_DIFF_EXP_PRIME" > "HOL4Real.poly.POLY_DIFF_EXP_PRIME"
|
|
|
99 |
"POLY_DIFF_EXP" > "HOL4Real.poly.POLY_DIFF_EXP"
|
|
|
100 |
"POLY_DIFF_CMUL" > "HOL4Real.poly.POLY_DIFF_CMUL"
|
|
|
101 |
"POLY_DIFF_CLAUSES" > "HOL4Real.poly.POLY_DIFF_CLAUSES"
|
|
|
102 |
"POLY_DIFF_AUX_NEG" > "HOL4Real.poly.POLY_DIFF_AUX_NEG"
|
|
|
103 |
"POLY_DIFF_AUX_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_AUX_MUL_LEMMA"
|
|
|
104 |
"POLY_DIFF_AUX_ISZERO" > "HOL4Real.poly.POLY_DIFF_AUX_ISZERO"
|
|
|
105 |
"POLY_DIFF_AUX_CMUL" > "HOL4Real.poly.POLY_DIFF_AUX_CMUL"
|
|
|
106 |
"POLY_DIFF_AUX_ADD" > "HOL4Real.poly.POLY_DIFF_AUX_ADD"
|
|
|
107 |
"POLY_DIFF_ADD" > "HOL4Real.poly.POLY_DIFF_ADD"
|
|
|
108 |
"POLY_DIFFERENTIABLE" > "HOL4Real.poly.POLY_DIFFERENTIABLE"
|
|
|
109 |
"POLY_DIFF" > "HOL4Real.poly.POLY_DIFF"
|
|
|
110 |
"POLY_CONT" > "HOL4Real.poly.POLY_CONT"
|
|
|
111 |
"POLY_CMUL_CLAUSES" > "HOL4Real.poly.POLY_CMUL_CLAUSES"
|
|
|
112 |
"POLY_CMUL" > "HOL4Real.poly.POLY_CMUL"
|
|
|
113 |
"POLY_ADD_RZERO" > "HOL4Real.poly.POLY_ADD_RZERO"
|
|
|
114 |
"POLY_ADD_CLAUSES" > "HOL4Real.poly.POLY_ADD_CLAUSES"
|
|
|
115 |
"POLY_ADD" > "HOL4Real.poly.POLY_ADD"
|
|
|
116 |
"ORDER_UNIQUE" > "HOL4Real.poly.ORDER_UNIQUE"
|
|
|
117 |
"ORDER_THM" > "HOL4Real.poly.ORDER_THM"
|
|
|
118 |
"ORDER_ROOT" > "HOL4Real.poly.ORDER_ROOT"
|
|
|
119 |
"ORDER_POLY" > "HOL4Real.poly.ORDER_POLY"
|
|
|
120 |
"ORDER_MUL" > "HOL4Real.poly.ORDER_MUL"
|
|
|
121 |
"ORDER_DIVIDES" > "HOL4Real.poly.ORDER_DIVIDES"
|
|
|
122 |
"ORDER_DIFF" > "HOL4Real.poly.ORDER_DIFF"
|
|
|
123 |
"ORDER_DECOMP" > "HOL4Real.poly.ORDER_DECOMP"
|
|
|
124 |
"ORDER" > "HOL4Real.poly.ORDER"
|
|
|
125 |
"FINITE_LEMMA" > "HOL4Real.poly.FINITE_LEMMA"
|
|
|
126 |
"DEGREE_ZERO" > "HOL4Real.poly.DEGREE_ZERO"
|
|
|
127 |
|
|
|
128 |
end
|