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
     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" > "Fun.surj"
    25   "ONE_ONE" > "HOL4Setup.ONE_ONE"
    26   "LET" > "HOL4Compat.LET"
    27   "IN" > "HOL4Base.bool.IN"
    28   "F" > "False"
    29   "COND" > "HOL.If"
    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"
    40   "bool_INDUCT" > "Datatype.bool.induct_correctness"
    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"
    81   "OR_ELIM_THM" > "Recdef.tfl_disjE"
    82   "OR_DEF" > "HOL.or_def"
    83   "OR_CONG" > "HOL4Base.bool.OR_CONG"
    84   "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
    85   "ONTO_THM" > "Fun.surj_def"
    86   "ONTO_DEF" > "Fun.surj_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"
    96   "MONO_OR" > "Inductive.basic_monos_3"
    97   "MONO_NOT" > "HOL.rev_contrapos"
    98   "MONO_IMP" > "Set.imp_mono"
    99   "MONO_EXISTS" > "Inductive.basic_monos_5"
   100   "MONO_COND" > "HOL4Base.bool.MONO_COND"
   101   "MONO_AND" > "Inductive.basic_monos_4"
   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"
   142   "ETA_THM" > "Presburger.fm_modd_pinf"
   143   "ETA_AX" > "Presburger.fm_modd_pinf"
   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"
   147   "EQ_REFL" > "Presburger.fm_modd_pinf"
   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"
   155   "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
   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"
   175   "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
   176   "BETA_THM" > "Presburger.fm_modd_pinf"
   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"
   186   "ABS_SIMP" > "Presburger.fm_modd_pinf"
   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