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"


24 
"ONTO" > "HOL4Setup.ONTO"


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"

15647

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"


44 
"UNWIND_FORALL_THM2" > "HOL.simp_thms_41"


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"


85 
"ONTO_THM" > "HOL4Setup.ONTO_DEF"


86 
"ONTO_DEF" > "HOL4Setup.ONTO_DEF"


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"


98 
"MONO_IMP" > "Set.imp_mono"

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"


111 
"LEFT_FORALL_IMP_THM" > "HOL.imp_ex"


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"


115 
"LEFT_AND_FORALL_THM" > "HOL.all_simps_1"


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"


149 
"EQ_EXT" > "HOL.meta_eq_to_obj_eq"


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
