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