--- a/src/HOL/Hyperreal/HRealAbs.ML Tue Jan 27 09:44:14 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title : HRealAbs.ML
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : Absolute value function for the hyperreals
- Similar to RealAbs.thy
-*)
-
-(*------------------------------------------------------------
- absolute value on hyperreals as pointwise operation on
- equivalence class representative
- ------------------------------------------------------------*)
-
-Goalw [hrabs_def]
- "abs (number_of v :: hypreal) = \
-\ (if neg (number_of v) then number_of (bin_minus v) \
-\ else number_of v)";
-by (Simp_tac 1);
-qed "hrabs_number_of";
-Addsimps [hrabs_number_of];
-
-(*------------------------------------------------------------
- Properties of the absolute value function over the reals
- (adapted version of previously proved theorems about abs)
- ------------------------------------------------------------*)
-
-Goal "(0::hypreal)<=x ==> abs x = x";
-by (asm_simp_tac (simpset() addsimps [hrabs_def]) 1);
-qed "hrabs_eqI1";
-
-Goal "(0::hypreal)<x ==> abs x = x";
-by (asm_simp_tac (simpset() addsimps [order_less_imp_le, hrabs_eqI1]) 1);
-qed "hrabs_eqI2";
-
-Goal "x<(0::hypreal) ==> abs x = -x";
-by (asm_simp_tac (simpset() addsimps [hypreal_le_def, hrabs_def]) 1);
-qed "hrabs_minus_eqI2";
-
-Goal "x<=(0::hypreal) ==> abs x = -x";
-by (auto_tac (claset() addDs [order_antisym], simpset() addsimps [hrabs_def]));qed "hrabs_minus_eqI1";
-
-Addsimps [abs_mult];
-
-Goalw [hrabs_def] "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)";
-by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-qed "hrabs_add_less";
-
-Goal "abs x < r ==> (0::hypreal) < r";
-by (blast_tac (claset() addSIs [order_le_less_trans, abs_ge_zero]) 1);
-qed "hrabs_less_gt_zero";
-
-Goal "abs x = (x::hypreal) | abs x = -x";
-by (simp_tac (simpset() addsimps [hrabs_def]) 1);
-qed "hrabs_disj";
-
-Goal "abs x = (y::hypreal) ==> x = y | -x = y";
-by (asm_full_simp_tac (simpset() addsimps [hrabs_def]
- addsplits [split_if_asm]) 1);
-qed "hrabs_eq_disj";
-
-(* Needed in Geom.ML *)
-Goal "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y";
-by (asm_full_simp_tac (simpset() addsimps [hrabs_def]
- addsplits [split_if_asm]) 1);
-qed "hrabs_add_lemma_disj";
-
-(* Needed in Geom.ML?? *)
-Goal "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y";
-by (asm_full_simp_tac (simpset() addsimps [hrabs_def]
- addsplits [split_if_asm]) 1);
-qed "hrabs_add_lemma_disj2";
-
-
-(*----------------------------------------------------------
- Relating hrabs to abs through embedding of IR into IR*
- ----------------------------------------------------------*)
-Goalw [hypreal_of_real_def]
- "abs (hypreal_of_real r) = hypreal_of_real (abs r)";
-by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs]));
-qed "hypreal_of_real_hrabs";
-
-
-(*----------------------------------------------------------------------------
- Embedding of the naturals in the hyperreals
- ----------------------------------------------------------------------------*)
-
-Goal "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
-qed "hypreal_of_nat_add";
-Addsimps [hypreal_of_nat_add];
-
-Goal "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
-qed "hypreal_of_nat_mult";
-Addsimps [hypreal_of_nat_mult];
-
-Goalw [hypreal_of_nat_def]
- "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
-by (auto_tac (claset() addIs [hypreal_add_less_mono1], simpset()));
-qed "hypreal_of_nat_less_iff";
-Addsimps [hypreal_of_nat_less_iff RS sym];
-
-(*------------------------------------------------------------*)
-(* naturals embedded in hyperreals *)
-(* is a hyperreal c.f. NS extension *)
-(*------------------------------------------------------------*)
-
-Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def]
- "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})";
-by Auto_tac;
-qed "hypreal_of_nat_iff";
-
-Goal "inj hypreal_of_nat";
-by (simp_tac (simpset() addsimps [inj_on_def, hypreal_of_nat_def]) 1);
-qed "inj_hypreal_of_nat";
-
-Goalw [hypreal_of_nat_def]
- "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)";
-by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
-qed "hypreal_of_nat_Suc";
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "hypreal_of_nat (number_of v :: nat) = \
-\ (if neg (number_of v) then 0 \
-\ else (number_of v :: hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1);
-qed "hypreal_of_nat_number_of";
-Addsimps [hypreal_of_nat_number_of];
-
-Goal "hypreal_of_nat 0 = 0";
-by (simp_tac (simpset() delsimps [numeral_0_eq_0]
- addsimps [numeral_0_eq_0 RS sym]) 1);
-qed "hypreal_of_nat_zero";
-Addsimps [hypreal_of_nat_zero];
-
-Goal "hypreal_of_nat 1 = 1";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_Suc]) 1);
-qed "hypreal_of_nat_one";
-Addsimps [hypreal_of_nat_one];