author  obua 
Mon, 29 Aug 2005 16:51:39 +0200  
changeset 17188  a26a4fc323ed 
parent 16775  c1b87ef4a1c3 
child 17644  bd59bfd4bf37 
permissions  rwrr 
14516  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" 

17188  94 
"REAL_MUL_SYM" > "IntDef.zmult_ac_2" 
14516  95 
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV" 
17188  96 
"REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident" 
14516  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" 

15647  100 
"REAL_LT_REFL" > "Orderings.order_less_irrefl" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15647
diff
changeset

101 
"REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" 
14796  102 
"REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" 
15647  103 
"REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" 
14516  104 
"REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" 
17188  105 
"REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2" 
14516  106 
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV" 
17188  107 
"REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident" 
14516  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 