|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"bit" > "bit_def"
|
|
|
7 |
"TIMES_2EXP" > "TIMES_2EXP_primdef"
|
|
|
8 |
"SLICE" > "SLICE_primdef"
|
|
|
9 |
"SBIT" > "SBIT_primdef"
|
|
|
10 |
"MOD_2EXP" > "MOD_2EXP_primdef"
|
|
|
11 |
"LSBn" > "LSBn_primdef"
|
|
|
12 |
"DIV_2EXP" > "DIV_2EXP_primdef"
|
|
|
13 |
"DIVMOD_2EXP" > "DIVMOD_2EXP_primdef"
|
|
|
14 |
"DIV2" > "DIV2_primdef"
|
|
|
15 |
"BITWISE" > "BITWISE_primdef"
|
|
|
16 |
"BITS" > "BITS_primdef"
|
|
|
17 |
|
|
|
18 |
const_maps
|
|
|
19 |
"bit" > "HOL4Word32.bits.bit"
|
|
|
20 |
"TIMES_2EXP" > "HOL4Word32.bits.TIMES_2EXP"
|
|
|
21 |
"SLICE" > "HOL4Word32.bits.SLICE"
|
|
|
22 |
"SBIT" > "HOL4Word32.bits.SBIT"
|
|
|
23 |
"MOD_2EXP" > "HOL4Word32.bits.MOD_2EXP"
|
|
|
24 |
"LSBn" > "HOL4Word32.bits.LSBn"
|
|
|
25 |
"DIV_2EXP" > "HOL4Word32.bits.DIV_2EXP"
|
|
|
26 |
"DIVMOD_2EXP" > "HOL4Word32.bits.DIVMOD_2EXP"
|
|
|
27 |
"DIV2" > "HOL4Word32.bits.DIV2"
|
|
|
28 |
"BITS" > "HOL4Word32.bits.BITS"
|
|
|
29 |
|
|
|
30 |
const_renames
|
|
|
31 |
"BIT" > "bit"
|
|
|
32 |
|
|
|
33 |
thm_maps
|
|
|
34 |
"bit_def" > "HOL4Word32.bits.bit_def"
|
|
|
35 |
"ZERO_LT_TWOEXP" > "HOL4Word32.bits.ZERO_LT_TWOEXP"
|
|
|
36 |
"TWOEXP_MONO2" > "HOL4Word32.bits.TWOEXP_MONO2"
|
|
|
37 |
"TWOEXP_MONO" > "HOL4Word32.bits.TWOEXP_MONO"
|
|
|
38 |
"TWOEXP_DIVISION" > "HOL4Word32.bits.TWOEXP_DIVISION"
|
|
|
39 |
"TIMES_2EXP_primdef" > "HOL4Word32.bits.TIMES_2EXP_primdef"
|
|
|
40 |
"TIMES_2EXP_def" > "HOL4Word32.bits.TIMES_2EXP_def"
|
|
|
41 |
"SUC_SUB" > "HOL4Word32.bits.SUC_SUB"
|
|
|
42 |
"SLICE_primdef" > "HOL4Word32.bits.SLICE_primdef"
|
|
|
43 |
"SLICE_def" > "HOL4Word32.bits.SLICE_def"
|
|
|
44 |
"SLICE_ZERO" > "HOL4Word32.bits.SLICE_ZERO"
|
|
|
45 |
"SLICE_THM" > "HOL4Word32.bits.SLICE_THM"
|
|
|
46 |
"SLICE_LEM3" > "HOL4Word32.bits.SLICE_LEM3"
|
|
|
47 |
"SLICE_LEM2" > "HOL4Word32.bits.SLICE_LEM2"
|
|
|
48 |
"SLICE_LEM1" > "HOL4Word32.bits.SLICE_LEM1"
|
|
|
49 |
"SLICE_COMP_THM" > "HOL4Word32.bits.SLICE_COMP_THM"
|
|
|
50 |
"SLICELT_THM" > "HOL4Word32.bits.SLICELT_THM"
|
|
|
51 |
"SBIT_primdef" > "HOL4Word32.bits.SBIT_primdef"
|
|
|
52 |
"SBIT_def" > "HOL4Word32.bits.SBIT_def"
|
|
|
53 |
"SBIT_DIV" > "HOL4Word32.bits.SBIT_DIV"
|
|
|
54 |
"ODD_MOD2_LEM" > "HOL4Word32.bits.ODD_MOD2_LEM"
|
|
|
55 |
"NOT_ZERO_ADD1" > "Nat.not0_implies_Suc"
|
|
|
56 |
"NOT_MOD2_LEM2" > "HOL4Word32.bits.NOT_MOD2_LEM2"
|
|
|
57 |
"NOT_MOD2_LEM" > "HOL4Word32.bits.NOT_MOD2_LEM"
|
|
|
58 |
"NOT_BITS2" > "HOL4Word32.bits.NOT_BITS2"
|
|
|
59 |
"NOT_BITS" > "HOL4Word32.bits.NOT_BITS"
|
|
|
60 |
"NOT_BIT" > "HOL4Word32.bits.NOT_BIT"
|
|
|
61 |
"MOD_PLUS_RIGHT" > "HOL4Word32.bits.MOD_PLUS_RIGHT"
|
|
|
62 |
"MOD_PLUS_1" > "HOL4Word32.bits.MOD_PLUS_1"
|
|
|
63 |
"MOD_ADD_1" > "HOL4Word32.bits.MOD_ADD_1"
|
|
|
64 |
"MOD_2EXP_primdef" > "HOL4Word32.bits.MOD_2EXP_primdef"
|
|
|
65 |
"MOD_2EXP_def" > "HOL4Word32.bits.MOD_2EXP_def"
|
|
|
66 |
"MOD_2EXP_MONO" > "HOL4Word32.bits.MOD_2EXP_MONO"
|
|
|
67 |
"MOD_2EXP_LT" > "HOL4Word32.bits.MOD_2EXP_LT"
|
|
|
68 |
"MOD_2EXP_LEM" > "HOL4Word32.bits.MOD_2EXP_LEM"
|
|
|
69 |
"LSBn_primdef" > "HOL4Word32.bits.LSBn_primdef"
|
|
|
70 |
"LSBn_def" > "HOL4Word32.bits.LSBn_def"
|
|
|
71 |
"LSB_ODD" > "HOL4Word32.bits.LSB_ODD"
|
|
|
72 |
"LESS_EXP_MULT2" > "HOL4Word32.bits.LESS_EXP_MULT2"
|
|
|
73 |
"LESS_EQ_EXP_MULT" > "HOL4Word32.bits.LESS_EQ_EXP_MULT"
|
|
|
74 |
"EXP_SUB_LESS_EQ" > "HOL4Word32.bits.EXP_SUB_LESS_EQ"
|
|
|
75 |
"EVEN_MOD2_LEM" > "HOL4Word32.bits.EVEN_MOD2_LEM"
|
|
|
76 |
"DIV_MULT_THM2" > "HOL4Word32.bits.DIV_MULT_THM2"
|
|
|
77 |
"DIV_MULT_THM" > "HOL4Word32.bits.DIV_MULT_THM"
|
|
|
78 |
"DIV_MULT_LEM" > "HOL4Word32.bits.DIV_MULT_LEM"
|
|
|
79 |
"DIV_MULT_1" > "HOL4Word32.bits.DIV_MULT_1"
|
|
|
80 |
"DIV_2EXP_primdef" > "HOL4Word32.bits.DIV_2EXP_primdef"
|
|
|
81 |
"DIV_2EXP_def" > "HOL4Word32.bits.DIV_2EXP_def"
|
|
|
82 |
"DIVMOD_2EXP_primdef" > "HOL4Word32.bits.DIVMOD_2EXP_primdef"
|
|
|
83 |
"DIVMOD_2EXP_def" > "HOL4Word32.bits.DIVMOD_2EXP_def"
|
|
|
84 |
"DIV2_primdef" > "HOL4Word32.bits.DIV2_primdef"
|
|
|
85 |
"DIV2_def" > "HOL4Word32.bits.DIV2_def"
|
|
|
86 |
"DIV1" > "HOL4Word32.bits.DIV1"
|
|
|
87 |
"BIT_def" > "HOL4Word32.bits.BIT_def"
|
|
|
88 |
"BIT_SLICE_THM" > "HOL4Word32.bits.BIT_SLICE_THM"
|
|
|
89 |
"BIT_SLICE_LEM" > "HOL4Word32.bits.BIT_SLICE_LEM"
|
|
|
90 |
"BIT_SLICE" > "HOL4Word32.bits.BIT_SLICE"
|
|
|
91 |
"BIT_COMP_THM3" > "HOL4Word32.bits.BIT_COMP_THM3"
|
|
|
92 |
"BIT_BITS_THM" > "HOL4Word32.bits.BIT_BITS_THM"
|
|
|
93 |
"BITWISE_def" > "HOL4Word32.bits.BITWISE_def"
|
|
|
94 |
"BITWISE_THM" > "HOL4Word32.bits.BITWISE_THM"
|
|
|
95 |
"BITWISE_NOT_COR" > "HOL4Word32.bits.BITWISE_NOT_COR"
|
|
|
96 |
"BITWISE_LT_2EXP" > "HOL4Word32.bits.BITWISE_LT_2EXP"
|
|
|
97 |
"BITWISE_COR" > "HOL4Word32.bits.BITWISE_COR"
|
|
|
98 |
"BITS_primdef" > "HOL4Word32.bits.BITS_primdef"
|
|
|
99 |
"BITS_def" > "HOL4Word32.bits.BITS_def"
|
|
|
100 |
"BITS_ZERO3" > "HOL4Word32.bits.BITS_ZERO3"
|
|
|
101 |
"BITS_ZERO2" > "HOL4Word32.bits.BITS_ZERO2"
|
|
|
102 |
"BITS_ZERO" > "HOL4Word32.bits.BITS_ZERO"
|
|
|
103 |
"BITS_THM" > "HOL4Word32.bits.BITS_THM"
|
|
|
104 |
"BITS_SUC_THM" > "HOL4Word32.bits.BITS_SUC_THM"
|
|
|
105 |
"BITS_SUC" > "HOL4Word32.bits.BITS_SUC"
|
|
|
106 |
"BITS_SLICE_THM2" > "HOL4Word32.bits.BITS_SLICE_THM2"
|
|
|
107 |
"BITS_SLICE_THM" > "HOL4Word32.bits.BITS_SLICE_THM"
|
|
|
108 |
"BITS_LT_HIGH" > "HOL4Word32.bits.BITS_LT_HIGH"
|
|
|
109 |
"BITS_DIV_THM" > "HOL4Word32.bits.BITS_DIV_THM"
|
|
|
110 |
"BITS_COMP_THM2" > "HOL4Word32.bits.BITS_COMP_THM2"
|
|
|
111 |
"BITS_COMP_THM" > "HOL4Word32.bits.BITS_COMP_THM"
|
|
|
112 |
"BITSLT_THM" > "HOL4Word32.bits.BITSLT_THM"
|
|
|
113 |
"BITS2_THM" > "HOL4Word32.bits.BITS2_THM"
|
|
|
114 |
|
|
|
115 |
end
|