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