src/HOL/Hyperreal/HyperOrd.ML
author paulson
Wed, 10 Jan 2001 17:21:31 +0100
changeset 10857 47b1f34ddd09
parent 10784 27e4d90b35b5
child 10919 144ede948e58
permissions -rw-r--r--
revisions e.g. images, transitive closure...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:	 Real/Hyperreal/HyperOrd.ML
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author:      Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright:   1998 University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
                 2000 University of Edinburgh
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
    Description: Type "hypreal" is a linear order and also 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
                 satisfies plus_ac0: + is an AC-operator with zero
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
(**** The simproc abel_cancel ****)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
(*** Two lemmas needed for the simprocs ***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    14
Goal "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
by (stac hypreal_add_left_commute 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    16
by (rtac hypreal_add_left_cancel 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    17
qed "hypreal_add_cancel_21";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    18
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    19
(*A further rule to deal with the case that
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
  everything gets cancelled on the right.*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
Goal "((x::hypreal) + (y + z) = y) = (x = -z)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
by (stac hypreal_add_left_commute 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    23
by (res_inst_tac [("t", "y")] (hypreal_add_zero_right RS subst) 1
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
    THEN stac hypreal_add_left_cancel 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
by (simp_tac (simpset() addsimps [hypreal_eq_diff_eq RS sym]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
qed "hypreal_add_cancel_end";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
structure Hyperreal_Cancel_Data =
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
struct
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    31
  val ss		= HOL_ss
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    32
  val eq_reflection	= eq_reflection
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    33
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    34
  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
  val T			= Type("HyperDef.hypreal",[])
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
  val zero		= Const ("0", T)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    37
  val restrict_to_left  = restrict_to_left
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    38
  val add_cancel_21	= hypreal_add_cancel_21
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    39
  val add_cancel_end	= hypreal_add_cancel_end
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    40
  val add_left_cancel	= hypreal_add_left_cancel
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    41
  val add_assoc		= hypreal_add_assoc
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    42
  val add_commute	= hypreal_add_commute
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    43
  val add_left_commute	= hypreal_add_left_commute
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    44
  val add_0		= hypreal_add_zero_left
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
  val add_0_right	= hypreal_add_zero_right
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    47
  val eq_diff_eq	= hypreal_eq_diff_eq
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    48
  val eqI_rules		= [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    49
  fun dest_eqI th = 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    50
      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    51
	      (HOLogic.dest_Trueprop (concl_of th)))
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    52
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    53
  val diff_def		= hypreal_diff_def
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    54
  val minus_add_distrib	= hypreal_minus_add_distrib
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    55
  val minus_minus	= hypreal_minus_minus
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    56
  val minus_0		= hypreal_minus_zero
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    57
  val add_inverses	= [hypreal_add_minus, hypreal_add_minus_left]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    58
  val cancel_simps	= [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    59
end;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    60
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    61
structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    62
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    63
Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    64
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    65
Goal "- (z - y) = y - (z::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    66
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    67
qed "hypreal_minus_diff_eq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    68
Addsimps [hypreal_minus_diff_eq];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    69
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    70
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    71
Goal "((x::hypreal) < y) = (-y < -x)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    72
by (stac hypreal_less_minus_iff 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    73
by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    74
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    75
qed "hypreal_less_swap_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    76
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    77
Goalw [hypreal_zero_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    78
      "((0::hypreal) < x) = (-x < x)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    79
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    80
by (auto_tac (claset(), simpset() addsimps [hypreal_less, hypreal_minus]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    81
by (ALLGOALS(Ultra_tac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    82
qed "hypreal_gt_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    83
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    84
Goal "(A::hypreal) < B ==> A + C < B + C";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    85
by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    86
by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    87
by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    88
by (auto_tac (claset() addSIs [exI], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    89
              simpset() addsimps [hypreal_less_def,hypreal_add]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    90
by (Ultra_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    91
qed "hypreal_add_less_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    92
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    93
Goal "!!(A::hypreal). A < B ==> C + A < C + B";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    94
by (auto_tac (claset() addIs [hypreal_add_less_mono1],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    95
    simpset() addsimps [hypreal_add_commute]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    96
qed "hypreal_add_less_mono2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    97
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    98
Goal "(x < (0::hypreal)) = (x < -x)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    99
by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   100
by (stac hypreal_gt_zero_iff 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   101
by (Full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   102
qed "hypreal_lt_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   103
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   104
Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   105
by (auto_tac (claset(), simpset() addsimps [hypreal_lt_zero_iff RS sym]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   106
qed "hypreal_ge_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   107
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   108
Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   109
by (auto_tac (claset(), simpset() addsimps [hypreal_gt_zero_iff RS sym]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   110
qed "hypreal_le_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   111
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   112
Goalw [hypreal_zero_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   113
      "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   114
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   115
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   116
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   117
              simpset() addsimps [hypreal_less_def,hypreal_add]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   118
by (auto_tac (claset() addSIs [exI],
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   119
              simpset() addsimps [hypreal_less_def,hypreal_add]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   120
by (ultra_tac (claset() addIs [real_add_order], simpset()) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   121
qed "hypreal_add_order";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   122
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   123
Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   124
by (auto_tac (claset() addDs [sym, order_le_imp_less_or_eq]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   125
                       addIs [hypreal_add_order],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   126
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   127
qed "hypreal_add_order_le";            
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   128
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   129
Goalw [hypreal_zero_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   130
          "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   131
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   132
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   133
by (auto_tac (claset() addSIs [exI],
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   134
              simpset() addsimps [hypreal_less_def,hypreal_mult]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   135
by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   136
	       simpset()) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   137
qed "hypreal_mult_order";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   138
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   139
Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   140
by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   141
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   142
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   143
qed "hypreal_mult_less_zero1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   144
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   145
Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   146
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   147
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   148
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   149
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   150
qed "hypreal_mult_less_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   151
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   152
Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   153
by (res_inst_tac [("x","%n. #0")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   154
by (res_inst_tac [("x","%n. #1")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   155
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   156
        simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   157
qed "hypreal_zero_less_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   158
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   159
Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   160
by (REPEAT(dtac order_le_imp_less_or_eq 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   161
by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   162
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   163
qed "hypreal_le_add_order";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   164
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   165
(*** Monotonicity results ***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   166
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   167
Goal "(v+z < w+z) = (v < (w::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   168
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   169
qed "hypreal_add_right_cancel_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   170
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   171
Goal "(z+v < z+w) = (v < (w::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   172
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   173
qed "hypreal_add_left_cancel_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   174
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   175
Addsimps [hypreal_add_right_cancel_less, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   176
          hypreal_add_left_cancel_less];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   177
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   178
Goal "(v+z <= w+z) = (v <= (w::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   179
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   180
qed "hypreal_add_right_cancel_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   181
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   182
Goal "(z+v <= z+w) = (v <= (w::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   183
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   184
qed "hypreal_add_left_cancel_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   185
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   186
Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   187
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   188
Goal  "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   189
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   190
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   191
by (dtac hypreal_add_order 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   192
by (thin_tac "0 < y2 + - z2" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   193
by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   194
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   195
      simpset() addsimps [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   196
                delsimps [hypreal_minus_add_distrib]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   197
qed "hypreal_add_less_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   198
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   199
Goal "(q1::hypreal) <= q2  ==> x + q1 <= x + q2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   200
by (dtac order_le_imp_less_or_eq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   201
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   202
by (auto_tac (claset() addSIs [order_less_imp_le,hypreal_add_less_mono1],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   203
              simpset() addsimps [hypreal_add_commute]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   204
qed "hypreal_add_left_le_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   205
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   206
Goal "(q1::hypreal) <= q2  ==> q1 + x <= q2 + x";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   207
by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   208
              simpset() addsimps [hypreal_add_commute]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   209
qed "hypreal_add_le_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   210
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   211
Goal "[|(i::hypreal)<=j;  k<=l |] ==> i + k <= j + l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   212
by (etac (hypreal_add_le_mono1 RS order_trans) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   213
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   214
qed "hypreal_add_le_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   215
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   216
Goal "[|(i::hypreal)<j;  k<=l |] ==> i + k < j + l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   217
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   218
                       addIs [hypreal_add_less_mono1,hypreal_add_less_mono],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   219
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   220
qed "hypreal_add_less_le_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   221
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   222
Goal "[|(i::hypreal)<=j;  k<l |] ==> i + k < j + l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   223
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   224
                       addIs [hypreal_add_less_mono2,hypreal_add_less_mono],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   225
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   226
qed "hypreal_add_le_less_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   227
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   228
Goal "(A::hypreal) + C < B + C ==> A < B";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   229
by (Full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   230
qed "hypreal_less_add_right_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   231
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   232
Goal "(C::hypreal) + A < C + B ==> A < B";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   233
by (Full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   234
qed "hypreal_less_add_left_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   235
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   236
Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   237
by (auto_tac (claset() addDs [hypreal_add_less_le_mono],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   238
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   239
qed "hypreal_add_zero_less_le_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   240
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   241
Goal "!!(A::hypreal). A + C <= B + C ==> A <= B";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   242
by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   243
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   244
qed "hypreal_le_add_right_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   245
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   246
Goal "!!(A::hypreal). C + A <= C + B ==> A <= B";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   247
by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   248
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   249
qed "hypreal_le_add_left_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   250
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   251
Goal "(0::hypreal) <= x*x";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   252
by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   253
by (auto_tac (claset() addIs [hypreal_mult_order,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   254
                              hypreal_mult_less_zero1,order_less_imp_le],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   255
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   256
qed "hypreal_le_square";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   257
Addsimps [hypreal_le_square];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   258
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   259
Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   260
by (auto_tac (claset() addSDs [hypreal_le_square RS order_le_less_trans],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   261
      simpset() addsimps [hypreal_minus_zero_less_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   262
qed "hypreal_less_minus_square";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   263
Addsimps [hypreal_less_minus_square];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   264
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   265
Goal "(0*x<r)=((0::hypreal)<r)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   266
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   267
qed "hypreal_mult_0_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   268
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   269
Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";       
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   270
by (rotate_tac 1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   271
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   272
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   273
by (dtac hypreal_mult_order 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   274
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   275
					   hypreal_mult_commute ]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   276
qed "hypreal_mult_less_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   277
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   278
Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";       
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   279
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   280
qed "hypreal_mult_less_mono2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   281
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   282
Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   283
by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   284
by (auto_tac (claset() addIs [hypreal_mult_less_mono1], simpset()));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   285
qed "hypreal_mult_le_less_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   286
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   287
Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   288
by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   289
				      hypreal_mult_le_less_mono1]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   290
qed "hypreal_mult_le_less_mono2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   291
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   292
val prem1::prem2::prem3::rest = goal thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   293
     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   294
by (rtac ([[prem1,prem2] MRS hypreal_mult_less_mono2, prem3] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   295
          MRS order_less_trans) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   296
qed "hypreal_mult_less_trans";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   297
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   298
Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   299
by (dtac order_le_imp_less_or_eq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   300
by (fast_tac (HOL_cs addEs [hypreal_mult_0_less RS iffD2,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   301
                            hypreal_mult_less_trans]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   302
qed "hypreal_mult_le_less_trans";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   303
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   304
Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   305
by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   306
by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   307
qed "hypreal_mult_le_le_trans";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   308
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   309
Goal "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   310
by (etac (hypreal_mult_less_mono1 RS order_less_trans) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   311
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   312
by (etac hypreal_mult_less_mono2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   313
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   314
qed "hypreal_mult_less_mono";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   315
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   316
(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   317
Goal "[| x < y;  r1 < r2;  (0::hypreal) <= r1;  0 <= x|] ==> r1 * x < r2 * y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   318
by (subgoal_tac "0<r2" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   319
by (blast_tac (claset() addIs [order_le_less_trans]) 2); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   320
by (case_tac "x=0" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   321
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   322
	               addIs [hypreal_mult_less_mono, hypreal_mult_order],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   323
	      simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   324
qed "hypreal_mult_less_mono'";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   325
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   326
Goal "0 < x ==> 0 < inverse (x::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   327
by (EVERY1[rtac ccontr, dtac hypreal_leI]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   328
by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   329
by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   330
by (dtac (hypreal_not_refl2 RS not_sym RS hypreal_inverse_not_zero) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   331
by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   332
by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   333
by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   334
                 simpset() addsimps [hypreal_minus_zero_less_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   335
qed "hypreal_inverse_gt_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   336
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   337
Goal "x < 0 ==> inverse (x::hypreal) < 0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   338
by (ftac hypreal_not_refl2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   339
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   340
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   341
by (stac (hypreal_minus_inverse RS sym) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   342
by (auto_tac (claset() addIs [hypreal_inverse_gt_zero],  simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   343
qed "hypreal_inverse_less_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   344
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   345
Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   346
by (auto_tac (claset() addIs [order_antisym], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   347
qed "hypreal_add_nonneg_eq_0_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   348
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   349
Goal "(x*y = 0) = (x = 0 | y = (0::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   350
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   351
by (blast_tac (claset() addDs [hypreal_mult_zero_disj]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   352
qed "hypreal_mult_is_0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   353
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   354
Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   355
by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   356
                         hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   357
qed "hypreal_three_squares_add_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   358
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   359
Goal "(x::hypreal)*x <= x*x + y*y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   360
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   361
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   362
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   363
              simpset() addsimps [hypreal_mult,hypreal_add,hypreal_le]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   364
qed "hypreal_self_le_add_pos";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   365
Addsimps [hypreal_self_le_add_pos];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   366
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   367
(*lcp: new lemma unfortunately needed...*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   368
Goal "-(x*x) <= (y*y::real)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   369
by (rtac order_trans 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   370
by (rtac real_le_square 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   371
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   372
qed "minus_square_le_square";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   373
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   374
Goal "(x::hypreal)*x <= x*x + y*y + z*z";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   375
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   376
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   377
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   378
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   379
	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   380
				  minus_square_le_square]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   381
qed "hypreal_self_le_add_pos2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   382
Addsimps [hypreal_self_le_add_pos2];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   383
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   384
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   385
(*----------------------------------------------------------------------------
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   386
               Existence of infinite hyperreal number
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   387
 ----------------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   388
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   389
Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   390
by (rtac Rep_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   391
qed "Rep_hypreal_omega";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   392
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   393
(* existence of infinite number not corresponding to any real number *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   394
(* use assumption that member FreeUltrafilterNat is not finite       *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   395
(* a few lemmas first *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   396
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   397
Goal "{n::nat. x = real_of_nat n} = {} | \
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   398
\     (EX y. {n::nat. x = real_of_nat n} = {y})";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   399
by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   400
qed "lemma_omega_empty_singleton_disj";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   401
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   402
Goal "finite {n::nat. x = real_of_nat n}";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   403
by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   404
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   405
qed "lemma_finite_omega_set";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   406
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   407
Goalw [omega_def,hypreal_of_real_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   408
      "~ (EX x. hypreal_of_real x = whr)";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   409
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   410
    simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym, 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   411
                    lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   412
qed "not_ex_hypreal_of_real_eq_omega";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   413
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   414
Goal "hypreal_of_real x ~= whr";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   415
by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   416
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   417
qed "hypreal_of_real_not_eq_omega";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   418
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   419
(* existence of infinitesimal number also not *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   420
(* corresponding to any real number *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   421
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   422
Goal "inverse (real_of_nat x) = inverse (real_of_nat y) ==> x = y";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   423
by (rtac (inj_real_of_nat RS injD) 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   424
by (Asm_full_simp_tac 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   425
qed "real_of_nat_inverse_inj";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   426
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   427
Goal "{n::nat. x = inverse(real_of_nat(Suc n))} = {} | \
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   428
\     (EX y. {n::nat. x = inverse(real_of_nat(Suc n))} = {y})";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   429
by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   430
qed "lemma_epsilon_empty_singleton_disj";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   431
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   432
Goal "finite {n::nat. x = inverse(real_of_nat(Suc n))}";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   433
by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   434
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   435
qed "lemma_finite_epsilon_set";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   436
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   437
Goalw [epsilon_def,hypreal_of_real_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   438
      "~ (EX x. hypreal_of_real x = ehr)";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   439
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   440
  simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   441
qed "not_ex_hypreal_of_real_eq_epsilon";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   442
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   443
Goal "hypreal_of_real x ~= ehr";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   444
by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   445
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   446
qed "hypreal_of_real_not_eq_epsilon";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   447
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   448
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   449
by Auto_tac;  
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   450
by (auto_tac (claset(),
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   451
     simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   452
qed "hypreal_epsilon_not_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   453
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   454
Goal "ehr = inverse(whr)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   455
by (asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   456
                     [hypreal_inverse, omega_def, epsilon_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   457
qed "hypreal_epsilon_inverse_omega";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   458
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   459
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   460
(* this proof is so much simpler than one for reals!! *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   461
Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   462
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   463
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   464
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   465
      simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   466
by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   467
qed "hypreal_inverse_less_swap";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   468
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   469
Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   470
by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   471
by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   472
by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   473
by (rtac hypreal_inverse_less_swap 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   474
by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_gt_zero]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   475
qed "hypreal_inverse_less_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   476
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   477
Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   478
by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   479
                                hypreal_inverse_gt_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   480
qed "hypreal_mult_inverse_less_mono1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   481
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   482
Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   483
by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   484
                                hypreal_inverse_gt_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   485
qed "hypreal_mult_inverse_less_mono2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   486
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   487
Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   488
by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   489
by (dtac (hypreal_not_refl2 RS not_sym) 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   490
by (auto_tac (claset() addSDs [hypreal_mult_inverse],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   491
              simpset() addsimps hypreal_mult_ac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   492
qed "hypreal_less_mult_right_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   493
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   494
Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   495
by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   496
    simpset() addsimps [hypreal_mult_commute]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   497
qed "hypreal_less_mult_left_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   498
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   499
Goal "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   500
by (forw_inst_tac [("y","r")] order_less_trans 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   501
by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   502
by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   503
by (auto_tac (claset() addIs [order_less_trans], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   504
qed "hypreal_mult_less_gt_zero"; 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   505
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   506
Goal "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   507
by (REPEAT(dtac order_le_imp_less_or_eq 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   508
by (rtac hypreal_less_or_eq_imp_le 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   509
by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   510
                         hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   511
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   512
qed "hypreal_mult_le_ge_zero"; 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   513
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   514
(*----------------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   515
     Some convenient biconditionals for products of signs 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   516
 ----------------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   517
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   518
Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   519
 by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   520
               simpset() addsimps [order_le_less, linorder_not_less, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   521
                              hypreal_mult_order, hypreal_mult_less_zero1]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   522
by (ALLGOALS (rtac ccontr)); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   523
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   524
              simpset() addsimps [order_le_less, linorder_not_less]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   525
by (ALLGOALS (etac rev_mp)); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   526
by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   527
by (auto_tac (claset() addDs [order_less_not_sym], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   528
              simpset() addsimps [hypreal_mult_commute]));  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   529
qed "hypreal_zero_less_mult_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   530
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   531
Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   532
by (auto_tac (claset() addDs [hypreal_mult_zero_disj],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   533
              simpset() addsimps [order_le_less, linorder_not_less,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   534
                                  hypreal_zero_less_mult_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   535
qed "hypreal_zero_le_mult_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   536
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   537
Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   538
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   539
              simpset() addsimps [hypreal_zero_le_mult_iff, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   540
                                  linorder_not_le RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   541
by (auto_tac (claset() addDs [order_less_not_sym],  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   542
              simpset() addsimps [linorder_not_le]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   543
qed "hypreal_mult_less_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   544
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   545
Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   546
by (auto_tac (claset() addDs [order_less_not_sym], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   547
              simpset() addsimps [hypreal_zero_less_mult_iff, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   548
                                  linorder_not_less RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   549
qed "hypreal_mult_le_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   550