src/HOL/Import/HOL/arithmetic.imp
author nipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 31790 05c92381363c
parent 30925 c38cbc0ac8d1
child 33657 a4179bf442d1
permissions -rw-r--r--
corrected and unified thm names
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "nat_elim__magic" > "nat_elim__magic_def"
     7   "ODD" > "ODD_def"
     8   "FACT" > "FACT_def"
     9   "EVEN" > "EVEN_def"
    10 
    11 const_maps
    12   "num_case" > "Nat.nat.nat_case"
    13   "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
    14   "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
    15   "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
    16   "NUMERAL" > "HOL4Compat.NUMERAL"
    17   "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
    18   "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
    19   "FUNPOW" > "HOL4Compat.FUNPOW"
    20   "EXP" > "Power.power_class.power" :: "nat => nat => nat"
    21   "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
    22   "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
    23   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
    24   ">=" > "HOL4Compat.nat_ge"
    25   ">" > "HOL4Compat.nat_gt"
    26   "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
    27   "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
    28   "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
    29   "*" > "HOL.times_class.times" :: "nat => nat => nat"
    30 
    31 thm_maps
    32   "num_case_def" > "HOL4Compat.num_case_def"
    33   "num_case_cong" > "HOL4Base.arithmetic.num_case_cong"
    34   "num_case_compute" > "HOL4Base.arithmetic.num_case_compute"
    35   "num_CASES" > "Nat.nat.nchotomy"
    36   "nat_elim__magic_def" > "HOL4Base.arithmetic.nat_elim__magic_def"
    37   "nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
    38   "ZERO_MOD" > "HOL4Base.arithmetic.ZERO_MOD"
    39   "ZERO_LESS_EXP" > "HOL4Base.arithmetic.ZERO_LESS_EXP"
    40   "ZERO_LESS_EQ" > "Nat.le0"
    41   "ZERO_DIV" > "HOL4Base.arithmetic.ZERO_DIV"
    42   "WOP" > "HOL4Base.arithmetic.WOP"
    43   "TWO" > "HOL4Base.arithmetic.TWO"
    44   "TIMES2" > "NatSimprocs.nat_mult_2"
    45   "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
    46   "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left"
    47   "SUC_NOT" > "Nat.nat.simps_2"
    48   "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
    49   "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
    50   "SUB_SUB" > "Nat.diff_diff_right"
    51   "SUB_RIGHT_SUB" > "Nat.diff_diff_left"
    52   "SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ"
    53   "SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS"
    54   "SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ"
    55   "SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER"
    56   "SUB_RIGHT_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_EQ"
    57   "SUB_RIGHT_ADD" > "HOL4Base.arithmetic.SUB_RIGHT_ADD"
    58   "SUB_PLUS" > "Nat.diff_diff_left"
    59   "SUB_MONO_EQ" > "Nat.diff_Suc_Suc"
    60   "SUB_LESS_OR" > "HOL4Base.arithmetic.SUB_LESS_OR"
    61   "SUB_LESS_EQ_ADD" > "HOL4Base.arithmetic.SUB_LESS_EQ_ADD"
    62   "SUB_LESS_EQ" > "Nat.diff_le_self"
    63   "SUB_LESS_0" > "Nat.zero_less_diff"
    64   "SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC"
    65   "SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB"
    66   "SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ"
    67   "SUB_LEFT_LESS" > "Nat.less_diff_conv"
    68   "SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv"
    69   "SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER"
    70   "SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ"
    71   "SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD"
    72   "SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0"
    73   "SUB_EQ_0" > "Nat.diff_is_0_eq"
    74   "SUB_EQUAL_0" > "Nat.diff_self_eq_0"
    75   "SUB_ELIM_THM" > "HOL4Base.arithmetic.SUB_ELIM_THM"
    76   "SUB_CANCEL" > "HOL4Base.arithmetic.SUB_CANCEL"
    77   "SUB_ADD" > "Nat.le_add_diff_inverse2"
    78   "SUB_0" > "HOL4Base.arithmetic.SUB_0"
    79   "SUB" > "HOL4Compat.SUB"
    80   "RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
    81   "RIGHT_ADD_DISTRIB" > "Nat.nat_distrib_1"
    82   "PRE_SUC_EQ" > "HOL4Base.arithmetic.PRE_SUC_EQ"
    83   "PRE_SUB1" > "HOL4Base.arithmetic.PRE_SUB1"
    84   "PRE_SUB" > "HOL4Base.arithmetic.PRE_SUB"
    85   "PRE_ELIM_THM" > "HOL4Base.arithmetic.PRE_ELIM_THM"
    86   "OR_LESS" > "Nat.Suc_le_lessD"
    87   "ONE" > "Nat.One_nat_def"
    88   "ODD_OR_EVEN" > "HOL4Base.arithmetic.ODD_OR_EVEN"
    89   "ODD_MULT" > "HOL4Base.arithmetic.ODD_MULT"
    90   "ODD_EXISTS" > "HOL4Base.arithmetic.ODD_EXISTS"
    91   "ODD_EVEN" > "HOL4Base.arithmetic.ODD_EVEN"
    92   "ODD_DOUBLE" > "HOL4Base.arithmetic.ODD_DOUBLE"
    93   "ODD_ADD" > "HOL4Base.arithmetic.ODD_ADD"
    94   "ODD" > "HOL4Base.arithmetic.ODD"
    95   "NUMERAL_DEF" > "HOL4Compat.NUMERAL_def"
    96   "NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2_def"
    97   "NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1_def"
    98   "NOT_ZERO_LT_ZERO" > "Nat.neq0_conv"
    99   "NOT_SUC_LESS_EQ_0" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ_0"
   100   "NOT_SUC_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ"
   101   "NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ"
   102   "NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
   103   "NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
   104   "NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
   105   "NOT_LESS" > "Nat.le_def"
   106   "NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
   107   "NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
   108   "NOT_GREATER" > "Nat.le_def"
   109   "NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
   110   "NORM_0" > "HOL4Base.arithmetic.NORM_0"
   111   "MULT_SYM" > "Int.zmult_ac_2"
   112   "MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
   113   "MULT_SUC" > "Nat.mult_Suc_right"
   114   "MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
   115   "MULT_MONO_EQ" > "Nat.Suc_mult_cancel1"
   116   "MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1"
   117   "MULT_LEFT_1" > "Finite_Set.AC_mult.f_e.left_ident"
   118   "MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES"
   119   "MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO"
   120   "MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
   121   "MULT_EQ_0" > "Nat.mult_is_0"
   122   "MULT_DIV" > "Divides.div_mult_self_is_m"
   123   "MULT_COMM" > "Int.zmult_ac_2"
   124   "MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
   125   "MULT_ASSOC" > "Int.zmult_ac_1"
   126   "MULT_0" > "Nat.mult_0_right"
   127   "MULT" > "HOL4Compat.MULT"
   128   "MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
   129   "MOD_TIMES2" > "HOL4Base.arithmetic.MOD_TIMES2"
   130   "MOD_TIMES" > "HOL4Base.arithmetic.MOD_TIMES"
   131   "MOD_PLUS" > "HOL4Base.arithmetic.MOD_PLUS"
   132   "MOD_P" > "HOL4Base.arithmetic.MOD_P"
   133   "MOD_ONE" > "Divides.mod_1"
   134   "MOD_MULT_MOD" > "HOL4Base.arithmetic.MOD_MULT_MOD"
   135   "MOD_MULT" > "HOL4Base.arithmetic.MOD_MULT"
   136   "MOD_MOD" > "HOL4Base.arithmetic.MOD_MOD"
   137   "MOD_EQ_0" > "HOL4Base.arithmetic.MOD_EQ_0"
   138   "MOD_COMMON_FACTOR" > "HOL4Base.arithmetic.MOD_COMMON_FACTOR"
   139   "MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED"
   140   "MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT"
   141   "MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ"
   142   "MIN_LT" > "HOL4Base.arithmetic.MIN_LT"
   143   "MIN_LE" > "HOL4Base.arithmetic.MIN_LE"
   144   "MIN_IDEM" > "Finite_Set.min.f.ACI_4"
   145   "MIN_DEF" > "HOL4Compat.MIN_DEF"
   146   "MIN_COMM" > "Finite_Set.min.f.ACI_2"
   147   "MIN_ASSOC" > "Finite_Set.min.f.ACI_1"
   148   "MIN_0" > "HOL4Base.arithmetic.MIN_0"
   149   "MAX_LT" > "HOL4Base.arithmetic.MAX_LT"
   150   "MAX_LE" > "HOL4Base.arithmetic.MAX_LE"
   151   "MAX_IDEM" > "Finite_Set.max.f.ACI_4"
   152   "MAX_DEF" > "HOL4Compat.MAX_DEF"
   153   "MAX_COMM" > "Finite_Set.max.f.ACI_2"
   154   "MAX_ASSOC" > "Finite_Set.max.f.ACI_1"
   155   "MAX_0" > "HOL4Base.arithmetic.MAX_0"
   156   "LESS_TRANS" > "Nat.less_trans"
   157   "LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT"
   158   "LESS_SUC_EQ_COR" > "Nat.Suc_lessI"
   159   "LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS"
   160   "LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD"
   161   "LESS_OR_EQ" > "HOL4Compat.LESS_OR_EQ"
   162   "LESS_OR" > "Nat.Suc_leI"
   163   "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
   164   "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
   165   "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
   166   "LESS_MONO_REV" > "Nat.Suc_less_SucD"
   167   "LESS_MONO_MULT" > "Nat.mult_le_mono1"
   168   "LESS_MONO_EQ" > "Nat.Suc_less_eq"
   169   "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
   170   "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
   171   "LESS_MONO_ADD" > "Nat.add_less_mono1"
   172   "LESS_MOD" > "Divides.mod_less"
   173   "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
   174   "LESS_LESS_EQ_TRANS" > "Nat.less_le_trans"
   175   "LESS_LESS_CASES" > "HOL4Base.arithmetic.LESS_LESS_CASES"
   176   "LESS_IMP_LESS_OR_EQ" > "Nat.le_simps_1"
   177   "LESS_IMP_LESS_ADD" > "Nat.trans_less_add1"
   178   "LESS_EXP_SUC_MONO" > "HOL4Base.arithmetic.LESS_EXP_SUC_MONO"
   179   "LESS_EQ_TRANS" > "Nat.le_trans"
   180   "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
   181   "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
   182   "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
   183   "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
   184   "LESS_EQ_MONO" > "Nat.Suc_le_mono"
   185   "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
   186   "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
   187   "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
   188   "LESS_EQ_EXISTS" > "Nat.le_iff_add"
   189   "LESS_EQ_CASES" > "Nat.nat_le_linear"
   190   "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
   191   "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
   192   "LESS_EQ_ADD" > "Nat.le_add1"
   193   "LESS_EQ_0" > "Nat.le_0_eq"
   194   "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
   195   "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
   196   "LESS_EQ" > "Nat.le_simps_3"
   197   "LESS_DIV_EQ_ZERO" > "Divides.div_less"
   198   "LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP"
   199   "LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES"
   200   "LESS_ANTISYM" > "HOL4Base.arithmetic.LESS_ANTISYM"
   201   "LESS_ADD_SUC" > "HOL4Base.arithmetic.LESS_ADD_SUC"
   202   "LESS_ADD_NONZERO" > "HOL4Base.arithmetic.LESS_ADD_NONZERO"
   203   "LESS_ADD_1" > "HOL4Base.arithmetic.LESS_ADD_1"
   204   "LESS_ADD" > "HOL4Base.arithmetic.LESS_ADD"
   205   "LESS_0_CASES" > "HOL4Base.arithmetic.LESS_0_CASES"
   206   "LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
   207   "LEFT_ADD_DISTRIB" > "Nat.nat_distrib_2"
   208   "LE" > "HOL4Base.arithmetic.LE"
   209   "INV_PRE_LESS_EQ" > "HOL4Base.arithmetic.INV_PRE_LESS_EQ"
   210   "INV_PRE_LESS" > "HOL4Base.arithmetic.INV_PRE_LESS"
   211   "INV_PRE_EQ" > "HOL4Base.arithmetic.INV_PRE_EQ"
   212   "GREATER_OR_EQ" > "HOL4Compat.GREATER_OR_EQ"
   213   "GREATER_EQ" > "HOL4Compat.real_ge"
   214   "GREATER_DEF" > "HOL4Compat.GREATER_DEF"
   215   "FUN_EQ_LEMMA" > "HOL4Base.arithmetic.FUN_EQ_LEMMA"
   216   "FUNPOW" > "HOL4Compat.FUNPOW"
   217   "FACT_LESS" > "HOL4Base.arithmetic.FACT_LESS"
   218   "FACT" > "HOL4Base.arithmetic.FACT"
   219   "EXP_INJECTIVE" > "Power.power_inject_exp"
   220   "EXP_EQ_1" > "HOL4Base.arithmetic.EXP_EQ_1"
   221   "EXP_EQ_0" > "HOL4Base.arithmetic.EXP_EQ_0"
   222   "EXP_ALWAYS_BIG_ENOUGH" > "HOL4Base.arithmetic.EXP_ALWAYS_BIG_ENOUGH"
   223   "EXP_ADD" > "Power.power_add"
   224   "EXP_1" > "HOL4Base.arithmetic.EXP_1"
   225   "EXP" > "HOL4Compat.EXP"
   226   "EXISTS_GREATEST" > "HOL4Base.arithmetic.EXISTS_GREATEST"
   227   "EVEN_OR_ODD" > "HOL4Base.arithmetic.EVEN_OR_ODD"
   228   "EVEN_ODD_EXISTS" > "HOL4Base.arithmetic.EVEN_ODD_EXISTS"
   229   "EVEN_ODD" > "HOL4Base.arithmetic.EVEN_ODD"
   230   "EVEN_MULT" > "HOL4Base.arithmetic.EVEN_MULT"
   231   "EVEN_EXISTS" > "HOL4Base.arithmetic.EVEN_EXISTS"
   232   "EVEN_DOUBLE" > "HOL4Base.arithmetic.EVEN_DOUBLE"
   233   "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
   234   "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
   235   "EVEN" > "HOL4Base.arithmetic.EVEN"
   236   "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
   237   "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
   238   "EQ_LESS_EQ" > "Orderings.order_eq_iff"
   239   "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
   240   "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
   241   "DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE"
   242   "DIV_P" > "HOL4Base.arithmetic.DIV_P"
   243   "DIV_ONE" > "Divides.div_1"
   244   "DIV_MULT" > "HOL4Base.arithmetic.DIV_MULT"
   245   "DIV_LESS_EQ" > "HOL4Base.arithmetic.DIV_LESS_EQ"
   246   "DIV_LESS" > "Divides.div_less_dividend"
   247   "DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT"
   248   "DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID"
   249   "DIVISION" > "HOL4Compat.DIVISION"
   250   "DA" > "HOL4Base.arithmetic.DA"
   251   "COMPLETE_INDUCTION" > "Nat.less_induct"
   252   "CANCEL_SUB" > "Nat.eq_diff_iff"
   253   "ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
   254   "ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
   255   "ADD_SUC" > "Nat.add_Suc_right"
   256   "ADD_SUB" > "Nat.diff_add_inverse2"
   257   "ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le"
   258   "ADD_INV_0_EQ" > "HOL4Base.arithmetic.ADD_INV_0_EQ"
   259   "ADD_INV_0" > "Nat.add_eq_self_zero"
   260   "ADD_EQ_SUB" > "HOL4Base.arithmetic.ADD_EQ_SUB"
   261   "ADD_EQ_1" > "HOL4Base.arithmetic.ADD_EQ_1"
   262   "ADD_EQ_0" > "Nat.add_is_0"
   263   "ADD_DIV_ADD_DIV" > "HOL4Base.arithmetic.ADD_DIV_ADD_DIV"
   264   "ADD_COMM" > "Finite_Set.AC_add.f.AC_2"
   265   "ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
   266   "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
   267   "ADD_0" > "Finite_Set.AC_add.f_e.ident"
   268   "ADD1" > "Nat_Numeral.Suc_eq_plus1"
   269   "ADD" > "HOL4Compat.ADD"
   270 
   271 end