src/HOL/Import/HOL/realax.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17644 bd59bfd4bf37
child 19233 77ca20b0ed77
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "treal_of_hreal" > "treal_of_hreal_def"
     7   "treal_neg" > "treal_neg_def"
     8   "treal_mul" > "treal_mul_def"
     9   "treal_lt" > "treal_lt_def"
    10   "treal_inv" > "treal_inv_def"
    11   "treal_eq" > "treal_eq_def"
    12   "treal_add" > "treal_add_def"
    13   "treal_1" > "treal_1_def"
    14   "treal_0" > "treal_0_def"
    15   "hreal_of_treal" > "hreal_of_treal_def"
    16 
    17 type_maps
    18   "real" > "RealDef.real"
    19 
    20 const_maps
    21   "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal"
    22   "treal_neg" > "HOL4Real.realax.treal_neg"
    23   "treal_mul" > "HOL4Real.realax.treal_mul"
    24   "treal_lt" > "HOL4Real.realax.treal_lt"
    25   "treal_inv" > "HOL4Real.realax.treal_inv"
    26   "treal_eq" > "HOL4Real.realax.treal_eq"
    27   "treal_add" > "HOL4Real.realax.treal_add"
    28   "treal_1" > "HOL4Real.realax.treal_1"
    29   "treal_0" > "HOL4Real.realax.treal_0"
    30   "real_neg" > "uminus" :: "real => real"
    31   "real_mul" > "op *" :: "real => real => real"
    32   "real_lt" > "op <" :: "real => real => bool"
    33   "real_add" > "op +" :: "real => real => real"
    34   "real_1" > "1" :: "real"
    35   "real_0" > "0" :: "real"
    36   "inv" > "HOL.inverse" :: "real => real"
    37   "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
    38 
    39 thm_maps
    40   "treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def"
    41   "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal"
    42   "treal_neg_def" > "HOL4Real.realax.treal_neg_def"
    43   "treal_neg" > "HOL4Real.realax.treal_neg"
    44   "treal_mul_def" > "HOL4Real.realax.treal_mul_def"
    45   "treal_mul" > "HOL4Real.realax.treal_mul"
    46   "treal_lt_def" > "HOL4Real.realax.treal_lt_def"
    47   "treal_lt" > "HOL4Real.realax.treal_lt"
    48   "treal_inv_def" > "HOL4Real.realax.treal_inv_def"
    49   "treal_inv" > "HOL4Real.realax.treal_inv"
    50   "treal_eq_def" > "HOL4Real.realax.treal_eq_def"
    51   "treal_eq" > "HOL4Real.realax.treal_eq"
    52   "treal_add_def" > "HOL4Real.realax.treal_add_def"
    53   "treal_add" > "HOL4Real.realax.treal_add"
    54   "treal_1_def" > "HOL4Real.realax.treal_1_def"
    55   "treal_1" > "HOL4Real.realax.treal_1"
    56   "treal_0_def" > "HOL4Real.realax.treal_0_def"
    57   "treal_0" > "HOL4Real.realax.treal_0"
    58   "hreal_of_treal_def" > "HOL4Real.realax.hreal_of_treal_def"
    59   "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
    60   "TREAL_NEG_WELLDEF" > "HOL4Real.realax.TREAL_NEG_WELLDEF"
    61   "TREAL_MUL_WELLDEFR" > "HOL4Real.realax.TREAL_MUL_WELLDEFR"
    62   "TREAL_MUL_WELLDEF" > "HOL4Real.realax.TREAL_MUL_WELLDEF"
    63   "TREAL_MUL_SYM" > "HOL4Real.realax.TREAL_MUL_SYM"
    64   "TREAL_MUL_LINV" > "HOL4Real.realax.TREAL_MUL_LINV"
    65   "TREAL_MUL_LID" > "HOL4Real.realax.TREAL_MUL_LID"
    66   "TREAL_MUL_ASSOC" > "HOL4Real.realax.TREAL_MUL_ASSOC"
    67   "TREAL_LT_WELLDEFR" > "HOL4Real.realax.TREAL_LT_WELLDEFR"
    68   "TREAL_LT_WELLDEFL" > "HOL4Real.realax.TREAL_LT_WELLDEFL"
    69   "TREAL_LT_WELLDEF" > "HOL4Real.realax.TREAL_LT_WELLDEF"
    70   "TREAL_LT_TRANS" > "HOL4Real.realax.TREAL_LT_TRANS"
    71   "TREAL_LT_TOTAL" > "HOL4Real.realax.TREAL_LT_TOTAL"
    72   "TREAL_LT_REFL" > "HOL4Real.realax.TREAL_LT_REFL"
    73   "TREAL_LT_MUL" > "HOL4Real.realax.TREAL_LT_MUL"
    74   "TREAL_LT_ADD" > "HOL4Real.realax.TREAL_LT_ADD"
    75   "TREAL_LDISTRIB" > "HOL4Real.realax.TREAL_LDISTRIB"
    76   "TREAL_ISO" > "HOL4Real.realax.TREAL_ISO"
    77   "TREAL_INV_WELLDEF" > "HOL4Real.realax.TREAL_INV_WELLDEF"
    78   "TREAL_INV_0" > "HOL4Real.realax.TREAL_INV_0"
    79   "TREAL_EQ_TRANS" > "HOL4Real.realax.TREAL_EQ_TRANS"
    80   "TREAL_EQ_SYM" > "HOL4Real.realax.TREAL_EQ_SYM"
    81   "TREAL_EQ_REFL" > "HOL4Real.realax.TREAL_EQ_REFL"
    82   "TREAL_EQ_EQUIV" > "HOL4Real.realax.TREAL_EQ_EQUIV"
    83   "TREAL_EQ_AP" > "HOL4Real.realax.TREAL_EQ_AP"
    84   "TREAL_BIJ_WELLDEF" > "HOL4Real.realax.TREAL_BIJ_WELLDEF"
    85   "TREAL_BIJ" > "HOL4Real.realax.TREAL_BIJ"
    86   "TREAL_ADD_WELLDEFR" > "HOL4Real.realax.TREAL_ADD_WELLDEFR"
    87   "TREAL_ADD_WELLDEF" > "HOL4Real.realax.TREAL_ADD_WELLDEF"
    88   "TREAL_ADD_SYM" > "HOL4Real.realax.TREAL_ADD_SYM"
    89   "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV"
    90   "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID"
    91   "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
    92   "TREAL_10" > "HOL4Real.realax.TREAL_10"
    93   "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
    94   "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
    95   "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
    96   "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
    97   "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
    98   "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
    99   "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
   100   "REAL_LT_REFL" > "Orderings.order_less_irrefl"
   101   "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
   102   "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
   103   "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
   104   "REAL_INV_0" > "Ring_and_Field.division_by_zero_class.inverse_zero"
   105   "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
   106   "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   107   "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
   108   "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
   109   "REAL_10" > "HOL4Compat.REAL_10"
   110   "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"
   111   "HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL"
   112   "HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE"
   113   "HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD"
   114   "HREAL_LT_GT" > "HOL4Real.realax.HREAL_LT_GT"
   115   "HREAL_LT_ADDR" > "HOL4Real.realax.HREAL_LT_ADDR"
   116   "HREAL_LT_ADDL" > "HOL4Real.realax.HREAL_LT_ADDL"
   117   "HREAL_LT_ADD2" > "HOL4Real.realax.HREAL_LT_ADD2"
   118   "HREAL_EQ_LADD" > "HOL4Real.realax.HREAL_EQ_LADD"
   119   "HREAL_EQ_ADDR" > "HOL4Base.hreal.HREAL_NOZERO"
   120   "HREAL_EQ_ADDL" > "HOL4Real.realax.HREAL_EQ_ADDL"
   121 
   122 ignore_thms
   123   "real_tybij"
   124   "real_of_hreal"
   125   "real_neg"
   126   "real_mul"
   127   "real_lt"
   128   "real_inv"
   129   "real_add"
   130   "real_TY_DEF"
   131   "real_1"
   132   "real_0"
   133   "hreal_of_real"
   134   "SUP_ALLPOS_LEMMA4"
   135   "SUP_ALLPOS_LEMMA3"
   136   "SUP_ALLPOS_LEMMA2"
   137   "SUP_ALLPOS_LEMMA1"
   138   "REAL_POS"
   139   "REAL_ISO_EQ"
   140 
   141 end