|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"RES_SELECT" > "RES_SELECT_def"
|
|
|
7 |
"RES_FORALL" > "RES_FORALL_def"
|
|
|
8 |
"RES_EXISTS_UNIQUE" > "RES_EXISTS_UNIQUE_def"
|
|
|
9 |
"RES_EXISTS" > "RES_EXISTS_def"
|
|
|
10 |
"RES_ABSTRACT" > "RES_ABSTRACT_def"
|
|
|
11 |
"IN" > "IN_def"
|
|
|
12 |
"ARB" > "ARB_def"
|
|
|
13 |
|
|
|
14 |
const_maps
|
|
|
15 |
"~" > "Not"
|
|
|
16 |
"bool_case" > "Datatype.bool.bool_case"
|
|
|
17 |
"\\/" > "op |"
|
|
|
18 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
|
|
|
19 |
"T" > "True"
|
|
|
20 |
"RES_SELECT" > "HOL4Base.bool.RES_SELECT"
|
|
|
21 |
"RES_FORALL" > "HOL4Base.bool.RES_FORALL"
|
|
|
22 |
"RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
|
|
|
23 |
"RES_EXISTS" > "HOL4Base.bool.RES_EXISTS"
|
|
17644
|
24 |
"ONTO" > "Fun.surj"
|
|
14516
|
25 |
"ONE_ONE" > "HOL4Setup.ONE_ONE"
|
|
|
26 |
"LET" > "HOL4Compat.LET"
|
|
|
27 |
"IN" > "HOL4Base.bool.IN"
|
|
|
28 |
"F" > "False"
|
|
16587
|
29 |
"COND" > "HOL.If"
|
|
14516
|
30 |
"ARB" > "HOL4Base.bool.ARB"
|
|
|
31 |
"?!" > "Ex1"
|
|
|
32 |
"?" > "Ex"
|
|
|
33 |
"/\\" > "op &"
|
|
|
34 |
"!" > "All"
|
|
|
35 |
|
|
|
36 |
thm_maps
|
|
|
37 |
"bool_case_thm" > "HOL4Base.bool.bool_case_thm"
|
|
|
38 |
"bool_case_ID" > "HOL4Base.bool.bool_case_ID"
|
|
|
39 |
"bool_case_DEF" > "HOL4Compat.bool_case_DEF"
|
|
17644
|
40 |
"bool_INDUCT" > "Datatype.bool.induct"
|
|
14516
|
41 |
"boolAxiom" > "HOL4Base.bool.boolAxiom"
|
|
|
42 |
"UNWIND_THM2" > "HOL.simp_thms_39"
|
|
|
43 |
"UNWIND_THM1" > "HOL.simp_thms_40"
|
|
17644
|
44 |
"UNWIND_FORALL_THM2" > "HOL4Base.bool.UNWIND_FORALL_THM2"
|
|
14516
|
45 |
"UNWIND_FORALL_THM1" > "HOL.simp_thms_42"
|
|
|
46 |
"UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP"
|
|
|
47 |
"UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
|
|
|
48 |
"T_DEF" > "HOL.True_def"
|
|
|
49 |
"TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"
|
|
|
50 |
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
|
|
|
51 |
"TRUTH" > "HOL.TrueI"
|
|
|
52 |
"SWAP_FORALL_THM" > "HOL4Base.bool.SWAP_FORALL_THM"
|
|
|
53 |
"SWAP_EXISTS_THM" > "HOL4Base.bool.SWAP_EXISTS_THM"
|
|
|
54 |
"SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM"
|
|
|
55 |
"SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE"
|
|
|
56 |
"SELECT_THM" > "HOL4Setup.EXISTS_DEF"
|
|
|
57 |
"SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial"
|
|
|
58 |
"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
|
|
|
59 |
"SELECT_AX" > "Hilbert_Choice.tfl_some"
|
|
|
60 |
"RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR"
|
|
|
61 |
"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
|
|
|
62 |
"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
|
|
|
63 |
"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
|
|
|
64 |
"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
|
|
|
65 |
"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
|
|
|
66 |
"RIGHT_AND_OVER_OR" > "HOL.conj_disj_distribR"
|
|
|
67 |
"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
|
|
|
68 |
"RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def"
|
|
|
69 |
"RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF"
|
|
|
70 |
"RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def"
|
|
|
71 |
"RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_DEF"
|
|
|
72 |
"RES_EXISTS_def" > "HOL4Base.bool.RES_EXISTS_def"
|
|
|
73 |
"RES_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def"
|
|
|
74 |
"RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
|
|
|
75 |
"RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF"
|
|
|
76 |
"RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF"
|
|
|
77 |
"REFL_CLAUSE" > "HOL.simp_thms_6"
|
|
|
78 |
"OR_INTRO_THM2" > "HOL.disjI2"
|
|
|
79 |
"OR_INTRO_THM1" > "HOL.disjI1"
|
|
|
80 |
"OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
|
|
17188
|
81 |
"OR_ELIM_THM" > "Recdef.tfl_disjE"
|
|
14516
|
82 |
"OR_DEF" > "HOL.or_def"
|
|
|
83 |
"OR_CONG" > "HOL4Base.bool.OR_CONG"
|
|
|
84 |
"OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
|
|
17644
|
85 |
"ONTO_THM" > "Fun.surj_def"
|
|
|
86 |
"ONTO_DEF" > "Fun.surj_def"
|
|
14516
|
87 |
"ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM"
|
|
|
88 |
"ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF"
|
|
|
89 |
"NOT_IMP" > "HOL.not_imp"
|
|
|
90 |
"NOT_FORALL_THM" > "Inductive.basic_monos_15"
|
|
|
91 |
"NOT_F" > "HOL.Eq_FalseI"
|
|
|
92 |
"NOT_EXISTS_THM" > "Inductive.basic_monos_16"
|
|
|
93 |
"NOT_DEF" > "HOL.simp_thms_19"
|
|
|
94 |
"NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
|
|
|
95 |
"NOT_AND" > "HOL4Base.bool.NOT_AND"
|
|
17188
|
96 |
"MONO_OR" > "Inductive.basic_monos_3"
|
|
14516
|
97 |
"MONO_NOT" > "HOL.rev_contrapos"
|
|
17644
|
98 |
"MONO_IMP" > "HOL4Base.bool.MONO_IMP"
|
|
17188
|
99 |
"MONO_EXISTS" > "Inductive.basic_monos_5"
|
|
14516
|
100 |
"MONO_COND" > "HOL4Base.bool.MONO_COND"
|
|
17188
|
101 |
"MONO_AND" > "Inductive.basic_monos_4"
|
|
14516
|
102 |
"MONO_ALL" > "Inductive.basic_monos_6"
|
|
|
103 |
"LET_THM" > "HOL.Let_def"
|
|
|
104 |
"LET_RATOR" > "HOL4Base.bool.LET_RATOR"
|
|
|
105 |
"LET_RAND" > "HOL4Base.bool.LET_RAND"
|
|
|
106 |
"LET_DEF" > "HOL4Compat.LET_def"
|
|
|
107 |
"LET_CONG" > "Recdef.let_cong"
|
|
|
108 |
"LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL"
|
|
|
109 |
"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
|
|
|
110 |
"LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
|
|
17644
|
111 |
"LEFT_FORALL_IMP_THM" > "HOL4Base.bool.LEFT_FORALL_IMP_THM"
|
|
14516
|
112 |
"LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
|
|
|
113 |
"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
|
|
|
114 |
"LEFT_AND_OVER_OR" > "HOL.conj_disj_distribL"
|
|
17644
|
115 |
"LEFT_AND_FORALL_THM" > "HOL4Base.bool.LEFT_AND_FORALL_THM"
|
|
14516
|
116 |
"IN_def" > "HOL4Base.bool.IN_def"
|
|
|
117 |
"IN_DEF" > "HOL4Base.bool.IN_DEF"
|
|
|
118 |
"INFINITY_AX" > "HOL4Setup.INFINITY_AX"
|
|
|
119 |
"IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F"
|
|
|
120 |
"IMP_F" > "HOL.notI"
|
|
|
121 |
"IMP_DISJ_THM" > "Inductive.basic_monos_11"
|
|
|
122 |
"IMP_CONG" > "HOL.imp_cong"
|
|
|
123 |
"IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES"
|
|
|
124 |
"IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as"
|
|
|
125 |
"F_IMP" > "HOL4Base.bool.F_IMP"
|
|
|
126 |
"F_DEF" > "HOL.False_def"
|
|
|
127 |
"FUN_EQ_THM" > "Fun.expand_fun_eq"
|
|
|
128 |
"FORALL_THM" > "HOL4Base.bool.FORALL_THM"
|
|
|
129 |
"FORALL_SIMP" > "HOL.simp_thms_35"
|
|
|
130 |
"FORALL_DEF" > "HOL.All_def"
|
|
|
131 |
"FORALL_AND_THM" > "HOL.all_conj_distrib"
|
|
|
132 |
"FALSITY" > "HOL.FalseE"
|
|
|
133 |
"EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
|
|
|
134 |
"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
|
|
|
135 |
"EXISTS_UNIQUE_DEF" > "HOL4Compat.EXISTS_UNIQUE_DEF"
|
|
|
136 |
"EXISTS_THM" > "HOL4Base.bool.EXISTS_THM"
|
|
|
137 |
"EXISTS_SIMP" > "HOL.simp_thms_36"
|
|
|
138 |
"EXISTS_REFL" > "HOL.simp_thms_37"
|
|
|
139 |
"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
|
|
|
140 |
"EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
|
|
|
141 |
"EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
|
|
17188
|
142 |
"ETA_THM" > "Presburger.fm_modd_pinf"
|
|
|
143 |
"ETA_AX" > "Presburger.fm_modd_pinf"
|
|
14516
|
144 |
"EQ_TRANS" > "Set.basic_trans_rules_31"
|
|
|
145 |
"EQ_SYM_EQ" > "HOL.eq_sym_conv"
|
|
|
146 |
"EQ_SYM" > "HOL.meta_eq_to_obj_eq"
|
|
17188
|
147 |
"EQ_REFL" > "Presburger.fm_modd_pinf"
|
|
14516
|
148 |
"EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
|
|
17644
|
149 |
"EQ_EXT" > "HOL4Base.bool.EQ_EXT"
|
|
14516
|
150 |
"EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
|
|
|
151 |
"EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES"
|
|
|
152 |
"DISJ_SYM" > "HOL.disj_comms_1"
|
|
|
153 |
"DISJ_IMP_THM" > "HOL.imp_disjL"
|
|
|
154 |
"DISJ_COMM" > "HOL.disj_comms_1"
|
|
17188
|
155 |
"DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
|
|
14516
|
156 |
"DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
|
|
|
157 |
"CONJ_SYM" > "HOL.conj_comms_1"
|
|
|
158 |
"CONJ_COMM" > "HOL.conj_comms_1"
|
|
|
159 |
"CONJ_ASSOC" > "HOL.conj_assoc"
|
|
|
160 |
"COND_RATOR" > "HOL4Base.bool.COND_RATOR"
|
|
|
161 |
"COND_RAND" > "HOL.if_distrib"
|
|
|
162 |
"COND_ID" > "HOL.if_cancel"
|
|
|
163 |
"COND_EXPAND" > "HOL4Base.bool.COND_EXPAND"
|
|
|
164 |
"COND_DEF" > "HOL4Compat.COND_DEF"
|
|
|
165 |
"COND_CONG" > "HOL4Base.bool.COND_CONG"
|
|
|
166 |
"COND_CLAUSES" > "HOL4Base.bool.COND_CLAUSES"
|
|
|
167 |
"COND_ABS" > "HOL4Base.bool.COND_ABS"
|
|
|
168 |
"BOTH_FORALL_OR_THM" > "HOL4Base.bool.BOTH_FORALL_OR_THM"
|
|
|
169 |
"BOTH_FORALL_IMP_THM" > "HOL4Base.bool.BOTH_FORALL_IMP_THM"
|
|
|
170 |
"BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM"
|
|
|
171 |
"BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM"
|
|
|
172 |
"BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
|
|
|
173 |
"BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
|
|
|
174 |
"BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
|
|
15647
|
175 |
"BOOL_CASES_AX" > "Datatype.bool.nchotomy"
|
|
17188
|
176 |
"BETA_THM" > "Presburger.fm_modd_pinf"
|
|
14516
|
177 |
"ARB_def" > "HOL4Base.bool.ARB_def"
|
|
|
178 |
"ARB_DEF" > "HOL4Base.bool.ARB_DEF"
|
|
|
179 |
"AND_INTRO_THM" > "HOL.conjI"
|
|
|
180 |
"AND_IMP_INTRO" > "HOL.imp_conjL"
|
|
|
181 |
"AND_DEF" > "HOL.and_def"
|
|
|
182 |
"AND_CONG" > "HOL4Base.bool.AND_CONG"
|
|
|
183 |
"AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
|
|
|
184 |
"AND2_THM" > "HOL.conjunct2"
|
|
|
185 |
"AND1_THM" > "HOL.conjunct1"
|
|
17188
|
186 |
"ABS_SIMP" > "Presburger.fm_modd_pinf"
|
|
14516
|
187 |
"ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
|
|
|
188 |
|
|
|
189 |
ignore_thms
|
|
|
190 |
"UNBOUNDED_THM"
|
|
|
191 |
"UNBOUNDED_DEF"
|
|
|
192 |
"BOUNDED_THM"
|
|
|
193 |
"BOUNDED_DEF"
|
|
|
194 |
|
|
|
195 |
end
|