src/HOL/Import/HOL/bits.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 44763 b50d5d694838
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "bit" > "bit_def"
     7   "TIMES_2EXP" > "TIMES_2EXP_primdef"
     8   "SLICE" > "SLICE_primdef"
     9   "SBIT" > "SBIT_primdef"
    10   "MOD_2EXP" > "MOD_2EXP_primdef"
    11   "LSBn" > "LSBn_primdef"
    12   "DIV_2EXP" > "DIV_2EXP_primdef"
    13   "DIVMOD_2EXP" > "DIVMOD_2EXP_primdef"
    14   "DIV2" > "DIV2_primdef"
    15   "BITWISE" > "BITWISE_primdef"
    16   "BITS" > "BITS_primdef"
    17 
    18 const_maps
    19   "bit" > "HOL4Word32.bits.bit"
    20   "TIMES_2EXP" > "HOL4Word32.bits.TIMES_2EXP"
    21   "SLICE" > "HOL4Word32.bits.SLICE"
    22   "SBIT" > "HOL4Word32.bits.SBIT"
    23   "MOD_2EXP" > "HOL4Word32.bits.MOD_2EXP"
    24   "LSBn" > "HOL4Word32.bits.LSBn"
    25   "DIV_2EXP" > "HOL4Word32.bits.DIV_2EXP"
    26   "DIVMOD_2EXP" > "HOL4Word32.bits.DIVMOD_2EXP"
    27   "DIV2" > "HOL4Word32.bits.DIV2"
    28   "BITS" > "HOL4Word32.bits.BITS"
    29 
    30 const_renames
    31   "BIT" > "bit"
    32 
    33 thm_maps
    34   "bit_def" > "HOL4Word32.bits.bit_def"
    35   "ZERO_LT_TWOEXP" > "HOL4Word32.bits.ZERO_LT_TWOEXP"
    36   "TWOEXP_MONO2" > "HOL4Word32.bits.TWOEXP_MONO2"
    37   "TWOEXP_MONO" > "HOL4Word32.bits.TWOEXP_MONO"
    38   "TWOEXP_DIVISION" > "HOL4Word32.bits.TWOEXP_DIVISION"
    39   "TIMES_2EXP_primdef" > "HOL4Word32.bits.TIMES_2EXP_primdef"
    40   "TIMES_2EXP_def" > "HOL4Word32.bits.TIMES_2EXP_def"
    41   "SUC_SUB" > "HOL4Word32.bits.SUC_SUB"
    42   "SLICE_primdef" > "HOL4Word32.bits.SLICE_primdef"
    43   "SLICE_def" > "HOL4Word32.bits.SLICE_def"
    44   "SLICE_ZERO" > "HOL4Word32.bits.SLICE_ZERO"
    45   "SLICE_THM" > "HOL4Word32.bits.SLICE_THM"
    46   "SLICE_LEM3" > "HOL4Word32.bits.SLICE_LEM3"
    47   "SLICE_LEM2" > "HOL4Word32.bits.SLICE_LEM2"
    48   "SLICE_LEM1" > "HOL4Word32.bits.SLICE_LEM1"
    49   "SLICE_COMP_THM" > "HOL4Word32.bits.SLICE_COMP_THM"
    50   "SLICELT_THM" > "HOL4Word32.bits.SLICELT_THM"
    51   "SBIT_primdef" > "HOL4Word32.bits.SBIT_primdef"
    52   "SBIT_def" > "HOL4Word32.bits.SBIT_def"
    53   "SBIT_DIV" > "HOL4Word32.bits.SBIT_DIV"
    54   "ODD_MOD2_LEM" > "HOL4Word32.bits.ODD_MOD2_LEM"
    55   "NOT_ZERO_ADD1" > "Nat.not0_implies_Suc"
    56   "NOT_MOD2_LEM2" > "HOL4Word32.bits.NOT_MOD2_LEM2"
    57   "NOT_MOD2_LEM" > "HOL4Word32.bits.NOT_MOD2_LEM"
    58   "NOT_BITS2" > "HOL4Word32.bits.NOT_BITS2"
    59   "NOT_BITS" > "HOL4Word32.bits.NOT_BITS"
    60   "NOT_BIT" > "HOL4Word32.bits.NOT_BIT"
    61   "MOD_PLUS_RIGHT" > "HOL4Word32.bits.MOD_PLUS_RIGHT"
    62   "MOD_PLUS_1" > "HOL4Word32.bits.MOD_PLUS_1"
    63   "MOD_ADD_1" > "HOL4Word32.bits.MOD_ADD_1"
    64   "MOD_2EXP_primdef" > "HOL4Word32.bits.MOD_2EXP_primdef"
    65   "MOD_2EXP_def" > "HOL4Word32.bits.MOD_2EXP_def"
    66   "MOD_2EXP_MONO" > "HOL4Word32.bits.MOD_2EXP_MONO"
    67   "MOD_2EXP_LT" > "HOL4Word32.bits.MOD_2EXP_LT"
    68   "MOD_2EXP_LEM" > "HOL4Word32.bits.MOD_2EXP_LEM"
    69   "LSBn_primdef" > "HOL4Word32.bits.LSBn_primdef"
    70   "LSBn_def" > "HOL4Word32.bits.LSBn_def"
    71   "LSB_ODD" > "HOL4Word32.bits.LSB_ODD"
    72   "LESS_EXP_MULT2" > "HOL4Word32.bits.LESS_EXP_MULT2"
    73   "LESS_EQ_EXP_MULT" > "HOL4Word32.bits.LESS_EQ_EXP_MULT"
    74   "EXP_SUB_LESS_EQ" > "HOL4Word32.bits.EXP_SUB_LESS_EQ"
    75   "EVEN_MOD2_LEM" > "HOL4Word32.bits.EVEN_MOD2_LEM"
    76   "DIV_MULT_THM2" > "HOL4Word32.bits.DIV_MULT_THM2"
    77   "DIV_MULT_THM" > "HOL4Word32.bits.DIV_MULT_THM"
    78   "DIV_MULT_LEM" > "HOL4Word32.bits.DIV_MULT_LEM"
    79   "DIV_MULT_1" > "HOL4Word32.bits.DIV_MULT_1"
    80   "DIV_2EXP_primdef" > "HOL4Word32.bits.DIV_2EXP_primdef"
    81   "DIV_2EXP_def" > "HOL4Word32.bits.DIV_2EXP_def"
    82   "DIVMOD_2EXP_primdef" > "HOL4Word32.bits.DIVMOD_2EXP_primdef"
    83   "DIVMOD_2EXP_def" > "HOL4Word32.bits.DIVMOD_2EXP_def"
    84   "DIV2_primdef" > "HOL4Word32.bits.DIV2_primdef"
    85   "DIV2_def" > "HOL4Word32.bits.DIV2_def"
    86   "DIV1" > "HOL4Word32.bits.DIV1"
    87   "BIT_def" > "HOL4Word32.bits.BIT_def"
    88   "BIT_SLICE_THM" > "HOL4Word32.bits.BIT_SLICE_THM"
    89   "BIT_SLICE_LEM" > "HOL4Word32.bits.BIT_SLICE_LEM"
    90   "BIT_SLICE" > "HOL4Word32.bits.BIT_SLICE"
    91   "BIT_COMP_THM3" > "HOL4Word32.bits.BIT_COMP_THM3"
    92   "BIT_BITS_THM" > "HOL4Word32.bits.BIT_BITS_THM"
    93   "BITWISE_def" > "HOL4Word32.bits.BITWISE_def"
    94   "BITWISE_THM" > "HOL4Word32.bits.BITWISE_THM"
    95   "BITWISE_NOT_COR" > "HOL4Word32.bits.BITWISE_NOT_COR"
    96   "BITWISE_LT_2EXP" > "HOL4Word32.bits.BITWISE_LT_2EXP"
    97   "BITWISE_COR" > "HOL4Word32.bits.BITWISE_COR"
    98   "BITS_primdef" > "HOL4Word32.bits.BITS_primdef"
    99   "BITS_def" > "HOL4Word32.bits.BITS_def"
   100   "BITS_ZERO3" > "HOL4Word32.bits.BITS_ZERO3"
   101   "BITS_ZERO2" > "HOL4Word32.bits.BITS_ZERO2"
   102   "BITS_ZERO" > "HOL4Word32.bits.BITS_ZERO"
   103   "BITS_THM" > "HOL4Word32.bits.BITS_THM"
   104   "BITS_SUC_THM" > "HOL4Word32.bits.BITS_SUC_THM"
   105   "BITS_SUC" > "HOL4Word32.bits.BITS_SUC"
   106   "BITS_SLICE_THM2" > "HOL4Word32.bits.BITS_SLICE_THM2"
   107   "BITS_SLICE_THM" > "HOL4Word32.bits.BITS_SLICE_THM"
   108   "BITS_LT_HIGH" > "HOL4Word32.bits.BITS_LT_HIGH"
   109   "BITS_DIV_THM" > "HOL4Word32.bits.BITS_DIV_THM"
   110   "BITS_COMP_THM2" > "HOL4Word32.bits.BITS_COMP_THM2"
   111   "BITS_COMP_THM" > "HOL4Word32.bits.BITS_COMP_THM"
   112   "BITSLT_THM" > "HOL4Word32.bits.BITSLT_THM"
   113   "BITS2_THM" > "HOL4Word32.bits.BITS2_THM"
   114 
   115 end