(*  Title       : HRealAbs.ML
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Absolute value function for the hyperreals
                  Similar to RealAbs.thy
*) 

(*----------------------------------------------------------------------------
       Properties of the absolute value function over the reals
       (adapted version of previously proved theorems about abs)
 ----------------------------------------------------------------------------*)
Goalw [hrabs_def] "hrabs r = (if 0hr<=r then r else -r)";
by (Step_tac 1);
qed "hrabs_iff";

Goalw [hrabs_def] "hrabs 0hr = 0hr";
by (rtac (hypreal_le_refl RS if_P) 1);
qed "hrabs_zero";

Addsimps [hrabs_zero];

Goalw [hrabs_def] "hrabs 0hr = -0hr";
by (rtac (hypreal_minus_zero RS ssubst) 1);
by (rtac if_cancel 1);
qed "hrabs_minus_zero";

val [prem] = goalw thy [hrabs_def] "0hr<=x ==> hrabs x = x";
by (rtac (prem RS if_P) 1);
qed "hrabs_eqI1";

val [prem] = goalw thy [hrabs_def] "0hr<x ==> hrabs x = x";
by (simp_tac (simpset() addsimps [(prem 
    RS hypreal_less_imp_le),hrabs_eqI1]) 1);
qed "hrabs_eqI2";

val [prem] = goalw thy [hrabs_def,hypreal_le_def] 
    "x<0hr ==> hrabs x = -x";
by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
qed "hrabs_minus_eqI2";

Goal "!!x. x<=0hr ==> hrabs x = -x";
by (dtac hypreal_le_imp_less_or_eq 1);
by (fast_tac (HOL_cs addIs [hrabs_minus_zero,
    hrabs_minus_eqI2]) 1);
qed "hrabs_minus_eqI1";

Goalw [hrabs_def,hypreal_le_def] "0hr<= hrabs x";
by (full_simp_tac (simpset()setloop (split_tac [expand_if])) 1);
by (Step_tac 1);
by (auto_tac (claset() addDs [hypreal_minus_zero_less_iff RS iffD2,
    hypreal_less_asym],simpset()));
qed "hrabs_ge_zero";

Goal "hrabs(hrabs x)=hrabs x";
by (res_inst_tac [("r1","hrabs x")] (hrabs_iff RS ssubst) 1);
by (blast_tac (claset() addIs [if_P,hrabs_ge_zero]) 1);
qed "hrabs_idempotent";

Goalw [hrabs_def] "(x=0hr) = (hrabs x = 0hr)";
by (full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
qed "hrabs_zero_iff";
Addsimps [hrabs_zero_iff RS sym];

Goal  "(x ~= 0hr) = (hrabs x ~= 0hr)";
by (full_simp_tac (simpset() addsimps [hrabs_zero_iff RS sym] 
    setloop (split_tac [expand_if])) 1);
qed "hrabs_not_zero_iff";

Goalw [hrabs_def] "x<=hrabs x";
by (full_simp_tac (simpset() addsimps [hypreal_le_refl] 
    setloop (split_tac [expand_if])) 1);
by (auto_tac (claset() addDs [not_hypreal_leE RS hypreal_less_imp_le],
    simpset() addsimps [hypreal_le_zero_iff]));
qed "hrabs_ge_self";

Goalw [hrabs_def] "-x<=hrabs x";
by (full_simp_tac (simpset() addsimps [hypreal_le_refl,
    hypreal_ge_zero_iff] setloop (split_tac [expand_if])) 1);
qed "hrabs_ge_minus_self";

Goalw [hrabs_def] "hrabs(x*y) = (hrabs x)*(hrabs y)";
by (auto_tac (claset(),simpset() addsimps [hypreal_minus_mult_eq1,
   hypreal_minus_mult_commute,hypreal_minus_mult_eq2] 
   setloop (split_tac [expand_if])));
by (blast_tac (claset() addDs [hypreal_le_mult_order]) 1);
by (auto_tac (claset() addSDs [not_hypreal_leE],simpset()));
by (EVERY1[dtac hypreal_mult_le_zero, assume_tac, dtac hypreal_le_anti_sym]);
by (EVERY[dtac hypreal_mult_le_zero 3, assume_tac 3, dtac hypreal_le_anti_sym 3]);
by (dtac hypreal_mult_less_zero1 5 THEN assume_tac 5);
by (auto_tac (claset() addDs [hypreal_less_asym,sym],
    simpset() addsimps [hypreal_minus_mult_eq2 RS sym] @ hypreal_mult_ac));
qed "hrabs_mult";

Goalw [hrabs_def] "!!x. x~= 0hr ==> hrabs(hrinv(x)) = hrinv(hrabs(x))";
by (auto_tac (claset(),simpset() addsimps [hypreal_minus_hrinv] 
    setloop (split_tac [expand_if])));
by (ALLGOALS(dtac not_hypreal_leE));
by (etac hypreal_less_asym 1);
by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq,
          hypreal_hrinv_gt_zero]) 1);
by (dtac (hrinv_not_zero RS not_sym) 1);
by (rtac (hypreal_hrinv_less_zero RSN (2,hypreal_less_asym)) 1);
by (assume_tac 2);
by (blast_tac (claset() addSDs [hypreal_le_imp_less_or_eq]) 1);
qed "hrabs_hrinv";

val [prem] = goal thy "y ~= 0hr ==> \
\            hrabs(x*hrinv(y)) = hrabs(x)*hrinv(hrabs(y))";
by (res_inst_tac [("c1","hrabs y")] (hypreal_mult_left_cancel RS subst) 1);
by (simp_tac (simpset() addsimps [(hrabs_not_zero_iff RS sym), prem]) 1);
by (simp_tac (simpset() addsimps [(hrabs_mult RS sym), prem, 
    hrabs_not_zero_iff RS sym] @ hypreal_mult_ac) 1);
qed "hrabs_mult_hrinv";

Goal "hrabs(x+y) <= hrabs x + hrabs y";
by (EVERY1 [res_inst_tac [("Q1","0hr<=x+y")] 
    (expand_if RS ssubst), rtac conjI]);
by (asm_simp_tac (simpset() addsimps [hrabs_eqI1,
    hypreal_add_le_mono,hrabs_ge_self]) 1);
by (asm_simp_tac (simpset() addsimps [not_hypreal_leE,
    hrabs_minus_eqI2,hypreal_add_le_mono,
    hrabs_ge_minus_self,hypreal_minus_add_distrib]) 1);
qed "hrabs_triangle_ineq";

Goal "hrabs(w + x + y) <= hrabs(w) + hrabs(x) + hrabs(y)";
by (auto_tac (claset() addSIs [(hrabs_triangle_ineq 
    RS hypreal_le_trans),hypreal_add_left_le_mono1],
    simpset() addsimps [hypreal_add_assoc]));
qed "hrabs_triangle_ineq_three";

Goalw [hrabs_def] "hrabs(-x)=hrabs(x)";
by (auto_tac (claset() addSDs [not_hypreal_leE,
   hypreal_less_asym] addIs [hypreal_le_anti_sym],
   simpset() addsimps [hypreal_ge_zero_iff] 
   setloop (split_tac [expand_if])));
qed "hrabs_minus_cancel";

Goal "hrabs(x + -y) = hrabs (y + -x)";
by (rtac (hrabs_minus_cancel RS subst) 1);
by (simp_tac (simpset() addsimps 
    [hypreal_minus_add_distrib,hypreal_add_commute]) 1);
qed "hrabs_minus_add_cancel";

Goal "hrabs(x + -y) <= hrabs x + hrabs y";
by (res_inst_tac [("x1","y")] (hrabs_minus_cancel RS subst) 1);
by (rtac hrabs_triangle_ineq 1);
qed "rhabs_triangle_minus_ineq";

val prem1::prem2::rest = 
goal thy "[| hrabs x < r; hrabs y < s |] ==> hrabs(x+y) < r + s";
by (rtac hypreal_le_less_trans 1);
by (rtac hrabs_triangle_ineq 1);
by (rtac ([prem1,prem2] MRS hypreal_add_less_mono) 1);
qed "hrabs_add_less";

Goal "!!x y. [| hrabs x < r; hrabs y < s |] ==> hrabs(x+ -y) < r + s";
by (rotate_tac 1 1);
by (dtac (hrabs_minus_cancel RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [hrabs_add_less]) 1);
qed "hrabs_add_minus_less";

val prem1::prem2::rest = 
    goal thy "[| hrabs x<r; hrabs y<s |] ==> hrabs(x*y)<r*s";
by (simp_tac (simpset() addsimps [hrabs_mult]) 1);
by (rtac hypreal_mult_le_less_trans 1);
by (rtac hrabs_ge_zero 1);
by (rtac prem2 1);
by (rtac hypreal_mult_less_mono1 1);
by (rtac (prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)) 1);
by (rtac prem1 1);
by (rtac ([prem1 RS (hrabs_ge_zero RS hypreal_le_less_trans),
   prem2 RS (hrabs_ge_zero RS hypreal_le_less_trans)] 
   MRS hypreal_mult_order) 1);
qed "hrabs_mult_less";

Goal "!! x y r. 1hr < hrabs x ==> hrabs y <= hrabs(x*y)";
by (cut_inst_tac [("x1","y")] (hrabs_ge_zero RS hypreal_le_imp_less_or_eq) 1);
by (EVERY1[etac disjE,rtac hypreal_less_imp_le]);
by (dres_inst_tac [("x1","1hr")]  (hypreal_less_minus_iff RS iffD1) 1);
by (forw_inst_tac [("y","hrabs x +-1hr")] hypreal_mult_order 1);
by (assume_tac 1);
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
    hrabs_mult, hypreal_mult_commute,hypreal_minus_mult_eq2 RS sym]) 1);
by (dtac sym 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_le_refl,hrabs_mult]) 1);
qed "hrabs_mult_le";

Goal "!!x. [| 1hr < hrabs x; r < hrabs y|] ==> r < hrabs(x*y)";
by (fast_tac (HOL_cs addIs [hrabs_mult_le, hypreal_less_le_trans]) 1);
qed "hrabs_mult_gt";

Goal "!!r. hrabs x < r ==> 0hr < r";
by (blast_tac (claset() addSIs [hypreal_le_less_trans,
    hrabs_ge_zero]) 1);
qed "hrabs_less_gt_zero";

Goalw [hrabs_def] "hrabs 1hr = 1hr";
by (auto_tac (claset() addSDs [not_hypreal_leE 
    RS hypreal_less_asym],simpset() addsimps 
    [hypreal_zero_less_one] setloop (split_tac [expand_if])));
qed "hrabs_one";

val prem1::prem2::rest = 
    goal thy "[| 0hr < x ; x < r |] ==> hrabs x < r";
by (simp_tac (simpset() addsimps [(prem1 RS hrabs_eqI2),prem2]) 1);
qed "hrabs_lessI";

Goal "hrabs x =x | hrabs x = -x";
by (cut_inst_tac [("x","0hr"),("y","x")] hypreal_linear 1);
by (fast_tac (claset() addIs [hrabs_eqI2,hrabs_minus_eqI2,
                            hrabs_zero,hrabs_minus_zero]) 1);
qed "hrabs_disj";

Goal "!!x. hrabs x = y ==> x = y | -x = y";
by (dtac sym 1);
by (hyp_subst_tac 1);
by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1);
by (REPEAT(Asm_simp_tac 1));
qed "hrabs_eq_disj";

Goal "(hrabs x < r) = (-r < x & x < r)";
by (Step_tac 1);
by (rtac (hypreal_less_swap_iff RS iffD2) 1);
by (asm_simp_tac (simpset() addsimps [(hrabs_ge_minus_self 
    RS hypreal_le_less_trans)]) 1);
by (asm_simp_tac (simpset() addsimps [(hrabs_ge_self 
    RS hypreal_le_less_trans)]) 1);
by (EVERY1 [dtac (hypreal_less_swap_iff RS iffD1), rotate_tac 1, 
            dtac (hypreal_minus_minus RS subst), 
            cut_inst_tac [("x","x")] hrabs_disj, dtac disjE ]);
by (assume_tac 3 THEN Auto_tac);
qed "hrabs_interval_iff";

Goal "(hrabs x < r) = (- x < r & x < r)";
by (auto_tac (claset(),simpset() addsimps [hrabs_interval_iff]));
by (dtac (hypreal_less_swap_iff RS iffD1) 1);
by (dtac (hypreal_less_swap_iff RS iffD1) 2);
by (Auto_tac);
qed "hrabs_interval_iff2";

Goal 
     "(hrabs (x + -y) < r) = (y + -r < x & x < y + r)";
by (auto_tac (claset(),simpset() addsimps 
     [hrabs_interval_iff]));
by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
by (ALLGOALS(dtac (hypreal_less_minus_iff RS iffD1)));
by (ALLGOALS(rtac (hypreal_less_minus_iff RS iffD2)));
by (auto_tac (claset(),simpset() addsimps 
    [hypreal_minus_add_distrib] addsimps hypreal_add_ac));
qed "hrabs_add_minus_interval_iff";

Goal "!!x. x < y ==> hrabs(y + -x) = y + -x";
by (dtac (hypreal_less_minus_iff RS iffD1) 1);
by (etac hrabs_eqI2 1);
qed "hrabs_less_eqI2";

Goal "!!x. x < y ==> hrabs(x + -y) = y + -x";
by (auto_tac (claset() addDs [hrabs_less_eqI2],
              simpset() addsimps [hrabs_minus_add_cancel]));
qed "hrabs_less_eqI2a";

Goal "!!x. x <= y ==> hrabs(y + -x) = y + -x";
by (auto_tac (claset() addDs  [hypreal_le_imp_less_or_eq,
              hrabs_less_eqI2],simpset()));
qed "hrabs_le_eqI2";

Goal "!!x. x <= y ==> hrabs(x + -y) = y + -x";
by (auto_tac (claset() addDs [hrabs_le_eqI2],
              simpset() addsimps [hrabs_minus_add_cancel]));
qed "hrabs_le_eqI2a";

(* Needed in GEOM.ML *)
Goal 
     "!!A. y + - x + (y + - z) = hrabs (x + - z) \
\     ==> y = z | x = y";
by (dtac (sym RS hrabs_eq_disj) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc 
    RS sym,hypreal_add_right_cancel,hypreal_minus_add_distrib]));
by (auto_tac (claset(),simpset() addsimps [hypreal_add_left_cancel]
    @ hypreal_add_ac));
qed "hrabs_add_lemma_disj";

(* Needed in GEOM.ML *)
Goal 
     "!!A. x + - y + (z + - y) = hrabs (x + - z) \
\     ==> y = z | x = y";
by (rtac (hypreal_minus_eq_cancel RS subst) 1);
by (res_inst_tac [("b1","y")] (hypreal_minus_eq_cancel RS subst) 1);
by (rtac hrabs_add_lemma_disj 1);
by (asm_full_simp_tac (simpset() addsimps [hrabs_minus_add_cancel] 
         @ hypreal_add_ac) 1);
qed "hrabs_add_lemma_disj2";
 
(*---------------------------------------------------------------------
                      Relating hrabs to abs
 ---------------------------------------------------------------------*)
Goal "hrabs (hypreal_of_real r) = hypreal_of_real (rabs r)";
by (cut_inst_tac [("R1.0","r"),("R2.0","0r")] real_linear 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
by (forward_tac [hypreal_of_real_less_iff RS iffD1] 1);
by (forward_tac [hypreal_of_real_less_iff RS iffD1] 2);
by (auto_tac (claset() addSDs [rabs_minus_eqI2, hrabs_minus_eqI2,
    rabs_eqI2, hrabs_eqI2],simpset() addsimps [hypreal_of_real_zero,
    hypreal_of_real_minus]));
qed "hypreal_of_real_hrabs";

(*--------------------------------------------------------------*)
Goalw [congruent_def]
  "congruent hyprel (%X. hyprel^^{%n. rabs (X n)})";
by (safe_tac (claset()));
by (ALLGOALS(Fuf_tac));
qed "hrabs_congruent";

(*Resolve th against the corresponding facts for hrabs*)
val hrabs_ize  = RSLIST [equiv_hyprel, hrabs_congruent];