Session Group-Ring-Module

Theory Algebra1

(**                Algebra1
                                  author Hidetsune Kobayashi
                                  Department of Mathematics
                                  Nihon University
                                  hikoba@math.cst.nihon-u.ac.jp
                                  May 3, 2004.
                                  April 6, 2007 (revised)

 chapter 0. Preliminaries
   section 1.   Natural numbers and Integers
   section 2.   Sets
   section 3.   Functions
   section 4.   Nsets, set of natural numbers
   section 4'.  Lower bounded set of integers
   section 5.   Augmented integer: integer and ∞ -∞
   section 6.   amin, amax
   section 7.   cardinality of sets

 Note. Some lemmas in this chapter are already formalized by L. Paulson
       and others.

 chapter 1.  Ordered Set
   section 1.   Basic Concepts of Ordered Sets
**)

theory Algebra1
imports Main "HOL-Library.FuncSet"
begin

chapter "Preliminaries"

text‹Some of the lemmas of this section are proved in src/HOL/Integ
   of Isabelle version 2003.›

section "Lemmas for logical manipulation"

lemma True_then:"True  P  P"
by simp

lemma ex_conjI:"P c; Q c  c. P c  Q c"
by blast

lemma forall_spec:" b. P b  Q b; P a  Q a"
by simp

lemma a_b_exchange:"a; a = b  b"
by simp

lemma eq_prop:" P; P = Q  Q"
by simp

lemma forball_contra:"yA. P x y  ¬ Q y; yA. Q y  R y 
                    yA. (¬ P x y)  R y"
by blast

lemma forball_contra1:"yA. P x y  Q y; yA. ¬ Q y  yA. ¬ P x y"
by blast

section "Natural numbers and Integers"

text‹Elementary properties of natural numbers and integers›

lemma nat_nonzero_pos:"(a::nat)  0  0 < a"
by simp

lemma add_both:"(a::nat) = b  a + c = b + c"
by simp

lemma add_bothl:"a = b  c + a = c + b"
by simp

lemma diff_Suc:"(n::nat)  m  m - n + Suc 0 = Suc m - n"
by arith

lemma le_convert:"a = b; a  c  b  c"
by simp

lemma ge_convert:"a = b; c  a  c  b"
by simp

lemma less_convert:" a = b; c < b   c < a"
by auto

lemma ineq_conv1:"a = b; a < c  b < c"
by simp

lemma diff_Suc_pos:"0 < a - Suc 0   0 < a"
by simp

lemma minus_SucSuc:"a - Suc (Suc 0) = a - Suc 0 - Suc 0"
by simp

lemma Suc_Suc_Tr:"Suc (Suc 0)  n  Suc (n - Suc (Suc 0)) = n - Suc 0"
by arith

lemma Suc_Suc_less:"Suc 0 < a  Suc (a - Suc (Suc 0)) < a"
by arith

lemma diff_zero_eq:"n = (0::nat)  m = m - n"
by simp

lemma Suc_less_le:"x < Suc n  x  n"
by auto

lemma less_le_diff:"x < n  x  n - Suc 0"
by arith

lemma le_pre_le:"x  n - Suc 0  x  n"
by arith

lemma nat_not_less:"¬ (m::nat) < n  n  m"
by (rule contrapos_pp, simp+)

lemma less_neq:"n < (m::nat)  n  m"
by (simp add:nat_neq_iff[THEN sym, of "n" "m"])

lemma less_le_diff1:"n  0  ((m::nat) < n) = (m  (n - Suc 0))"
by arith

lemma nat_not_less1:"n  0  (¬ (m::nat) < n) = (¬ m  (n - Suc 0))"
by arith

lemma nat_eq_le:"m = (n::nat)  m  n"
by simp


subsection "Integers"

lemma non_zero_int:" (n::int)  0  0 < n  n < 0"
by arith

lemma zgt_0_zge_1:"(0::int) < z  1  z"
by arith

lemma not_zle:"(¬ (n::int)  m) =  (m < n)"
by auto

lemma not_zless:"(¬ (n::int) < m) = (m  n)"
by auto

lemma zle_imp_zless_or_eq:"(n::int)  m  n < m  n = m"
by arith

lemma zminus_zadd_cancel:" - z + (z + w) = (w::int)"
by simp

lemma int_neq_iff:"((w::int)  z) = (w < z)  (z < w)"
by auto

lemma zless_imp_zle:"(z::int) < z'  z  z'"
by simp

lemma zdiff:"z - (w::int) = z + (- w)"
by simp

lemma zle_zless_trans:" (i::int)  j; j < k  i < k"
by arith

lemma zless_zle_trans:" (i::int) < j; j  k  i < k"
by arith

lemma zless_neq:"(i::int) < j  i  j"
by simp

lemma int_mult_mono:" i < j; (0::int) < k   k * i < k * j"
apply (frule zmult_zless_mono2_lemma [of "i" "j" "nat k"])
apply simp apply simp
done

lemma int_mult_le:"i  j; (0::int)  k  k * i  k * j"
apply (simp add:order_le_less)
 apply (case_tac "i < j")
  apply (case_tac "0 < k")
   apply simp
  apply simp
 apply simp
done

lemma int_mult_le1:"i  j; (0::int)  k  i * k  j * k"
apply (simp add:mult.commute[of _ "k"])
apply (simp add:int_mult_le)
done

lemma zmult_zminus_right:"(w::int) * (- z) = - (w * z)"
apply (insert distrib_left[of "w" "z" "-z"])
apply simp
done

lemma zmult_zle_mono1_neg:"(i::int)  j; k  0  j * k  i * k"
apply (subgoal_tac "0  - k") prefer 2 apply simp
apply (frule int_mult_le [of "i" "j" "- k"], assumption+)
apply (simp add:mult.commute)
done

lemma zmult_zless_mono_neg:"(i::int) < j; k < 0  j * k < i * k"
apply (subgoal_tac "0 < -k",
       frule int_mult_mono[of "i" "j" "-k"], assumption+,
       simp add:mult.commute, simp)
done

lemma zmult_neg_neg:"i < (0::int); j < 0   0 < i * j"
apply (frule zmult_zless_mono_neg[of "i" "0" "j"], assumption)
apply simp
done

lemma zmult_pos_pos:"(0::int) < i; 0 < j  0 < i * j"
apply (frule int_mult_mono[of "0" "i" "j"], assumption+)
apply (simp add:mult.commute)
done

lemma zmult_pos_neg:"(0::int) < i; j < 0  i * j < 0"
apply (frule zmult_zless_mono_neg[of "0" "i" "j"], assumption+, simp)
done

lemma zmult_neg_pos:"i < (0::int); 0 < j  i * j < 0"
apply (frule int_mult_mono[of "i" "0" "j"], assumption+,
       simp add:mult.commute)
done

lemma zle:"((z::int)  w) = (¬ (w < z))"
by auto

lemma times_1_both:"(0::int) < z; z * z' = 1  z = 1  z' = 1"
apply (subgoal_tac "0 < z'")
 apply (frule zgt_0_zge_1[of "z'"],
        subgoal_tac "z' = 1", simp,
        subgoal_tac "1 < z'  1 = z'", thin_tac "1  z'", thin_tac "0 < z'")
 apply (rule contrapos_pp, simp+,
        frule int_mult_mono[of "1" "z'" "z"], assumption+, simp, arith)
apply (rule contrapos_pp, simp+, simp add:zle[THEN sym],
       frule zless_imp_zle[of "0" "z"], frule int_mult_le[of "z'" "0" "z"],
       assumption+, simp)
done

lemma zminus_minus:"i - - (j::int) = i + j"
by simp

lemma zminus_minus_pos:"(n::int) < 0  0 < - n"
by simp

lemma zadd_zle_mono:"w'  w; z'  (z::int)  w' + z'  w + z"
by simp

lemma zmult_zle_mono:"i  (j::int); 0 < k  k * i   k * j"
apply (case_tac "i = j") apply simp
apply (frule zle_imp_zless_or_eq[of "i" "j"])
 apply (thin_tac "i  j") apply simp
done

lemma zmult_zle_mono_r:"i  (j::int); 0 < k  i * k  j * k"
apply (frule zmult_zle_mono[of "i" "j" "k"], assumption)
apply (simp add:mult.commute)
done

lemma pos_zmult_pos:" 0  (a::int); 0 < (b::int)  a  a * b"
apply (case_tac "a = 0") apply simp
apply (frule zle_imp_zless_or_eq[of "0" "a"]) apply (thin_tac "0  a")
apply simp
done

lemma pos_mult_l_gt:"(0::int) < w; i  j; 0  i  i  w * j"
by (metis not_zless pos_zmult_pos order_trans mult.commute)

lemma  pos_mult_r_gt:"(0::int) < w; i  j; 0  i  i  j * w"
apply (frule pos_mult_l_gt[of "w" "i" "j"], assumption+)
apply (simp add:mult.commute[of "w" "j"])
done

lemma mult_pos_iff:"(0::int) < i; 0  i * j   0  j"
apply (rule contrapos_pp, simp+)
 apply (cut_tac linorder_linear[of "0" "j"]) apply simp
 apply (simp add:not_zle)
 apply (frule int_mult_mono[of "j" "0" "i"], assumption+)  apply simp
done

lemma zmult_eq:"(0::int) < w; z = z'  w * z = w * z'"
by simp

lemma zmult_eq_r:"(0::int) < w; z = z'  z * w =  z' * w"
by simp


lemma zdiv_eq_l:"(0::int) < w; z * w  = z' * w   z = z'"
by simp

lemma zdiv_eq_r:"(0::int) < w; w * z  = w * z'   z = z'"
by simp

lemma int_nat_minus:"0 < (n::int)  nat (n - 1) = (nat n) - 1"
by arith

lemma int_nat_add:"0 < (n::int); 0 < (m::int)  (nat (n - 1)) + (nat (m - 1)) + (Suc 0) = nat (n + m - 1)"
by arith

lemma int_equation:"(x::int) = y + z  x - y = z"
by simp

lemma int_pos_mult_monor:" 0 < (n::int); 0  n * m   0  m"
by (rule mult_pos_iff, assumption+)

lemma int_pos_mult_monol:" 0 < (m::int); 0  n * m   0  n"
apply (rule int_pos_mult_monor, assumption+)
apply (simp add:mult.commute)
done

lemma zdiv_positive:"(0::int)  a; 0 < b  0  a div b"
apply (frule_tac a = 0 and a' = a and b = b in zdiv_mono1, assumption+)
apply simp
done

lemma zdiv_pos_mono_r:" (0::int) < w; w * z  w * z'  z  z'"
apply (rule contrapos_pp, simp+)
done (** zmult_div_mono to rename **)

lemma zdiv_pos_mono_l:" (0::int) < w; z * w  z' * w  z  z'"
apply (simp add:mult.commute)
done

lemma zdiv_pos_pos_l:" (0::int) < w; 0  z * w  0  z"
by (simp add:mult.commute, frule zdiv_pos_mono_r[of "w" "0" "z"], simp,
        assumption)

section "Sets"

(* Preliminary properties of sets are proved here. Some of them are
 already proved by L. Paulson and others. *)

subsection "A short notes for proof steps"

subsection "Sets"

lemma inEx:"x  A  yA. y = x"
by simp

lemma inEx_rev:" yA. y = x  x  A"
by blast

lemma nonempty_ex:"A  {}  x. x  A"
by blast

lemma ex_nonempty:"x. x  A  A  {}"
by blast

lemma not_eq_outside:"a  A  bA. b  a"
by blast

lemma ex_nonempty_set:"a. P a  {x. P x}  {}"
by blast

lemma nonempty: "x  A  A  {}"
by blast

lemma subset_self:"A  A"
by simp

lemma conditional_subset:"{xA. P x}  A"
by blast

lemma bsubsetTr:"{x. x  A  P x}  A"
by blast

lemma sets_not_eq:"A  B; B  A  aA. a  B"
by blast

lemma diff_nonempty:"A  B; B  A  A - B  {}"
by blast

lemma sub_which1:"A  B  B  A; x  A; x  B  B  A"
by blast

lemma sub_which2:"A  B  B  A; x  A; x  B  A  B"
by blast

lemma nonempty_int: "A  B  {}  x. x  A  B "
by blast

lemma no_meet1:"A  B = {} a  A. a  B"
by blast

lemma no_meet2:"A  B = {} a  B. a  A"
by blast

lemma elem_some:"x  A  yA. x = y"
by blast

lemma singleton_sub:"a  A  {a}  A"
by blast

lemma eq_elem_in: " a  A; a = b   b  A"
by simp

lemma eq_set_inc: " a  A; A = B   a  B"
by simp

lemma eq_set_not_inc:"a  A; A = B   a  B"
by simp

lemma int_subsets: " A1  A; B1  B   A1  B1  A  B"
by blast

lemma inter_mono:"A  B  A  C  B  C"
by blast

lemma sub_Un1:"B   B  C"
by blast

lemma sub_Un2:"C   B  C"
by blast

lemma subset_contr:" A  B; B  A   False"
by blast

lemma psubset_contr:" A  B; B  A   False"
by blast

lemma eqsets_sub:"A = B  A  B"
by simp

lemma not_subseteq:" ¬ A  B  a  A. a  B"
by blast

lemma in_un1:" x  A  B; x  B   x  A"
by blast

lemma proper_subset:"A  B; x  A; x  B  A  B"
by blast

lemma in_un2:" x  A  B; x  A   x  B"
by simp

lemma diff_disj:"x  A  A - {x} = A"
by auto

lemma in_diff:"x  a; x  A  x  A - {a}"
by simp

lemma in_diff1:"x  A - {a}  x  a"
by simp

lemma sub_inserted1:"Y  insert a X; ¬ Y  X  a  X  a  Y"
by blast

lemma sub_inserted2:"Y  insert a X; ¬ Y  X  Y = (Y - {a})  {a}"
by blast

lemma insert_sub:" A  B; a  B  (insert a A)  B"
by blast

lemma insert_diff:"A  (insert b B)  A - {b}  B"
by blast

lemma insert_inc1:"A  insert a A"
by blast

lemma insert_inc2:"a  insert a A"
by simp

lemma nonempty_some:"A  {}  (SOME x. x  A)  A"
apply (frule nonempty_ex[of "A"])
apply (rule someI2_ex) apply simp+
done

lemma mem_family_sub_Un:"A  C  A   C"
by blast

lemma sub_Union:"XC. A  X  A   C"
by blast

lemma family_subset_Un_sub:"AC. A  B   C  B"
by blast

lemma in_set_with_P:"P x  x  {y. P y}"
by blast

lemma sub_single:"A  {}; A  {a}  A = {a}"
by blast

lemma not_sub_single:"A  {}; A  {a}  ¬ A  {a}"
by blast

lemma not_sub:"¬ A  B  a. aA  a  B"
by blast


section "Functions"

definition
  cmp :: "['b  'c, 'a  'b]  ('a  'c)" where
  "cmp g f = (λx. g (f x))"

definition
  idmap :: "'a set  ('a  'a)" where
  "idmap A = (λxA. x)"

definition
  constmap :: "['a set, 'b set]  ('a 'b)" where
  "constmap A B = (λxA. SOME y. y  B)"

definition
  invfun :: "['a set, 'b set, 'a  'b]  ('b  'a)" where
  "invfun A B (f :: 'a  'b) = (λyB.(SOME x. (x  A  f x = y)))"

abbreviation
  INVFUN :: "['a  'b, 'b set, 'a set]  ('b  'a)"  ("(3_¯⇘_,_)" [82,82,83]82) where
  "f¯B,A == invfun A B f"

lemma eq_fun:" f  A  B; f = g   g  A  B"
by simp

lemma eq_fun_eq_val:" f = g  f x = g x"
by simp

lemma eq_elems_eq_val:"x = y  f x = f y"
by simp

lemma cmp_fun:"f  A  B; g  B  C   cmp g f  A  C"
by (auto simp add:cmp_def)

lemma cmp_fun_image:"f  A  B; g  B  C  
                          (cmp g f) ` A =  g ` (f ` A)"
apply (rule equalityI)
 apply (rule subsetI, simp add:image_def)
 apply (erule bexE, simp add:cmp_def, blast)
 apply (rule subsetI, simp add:image_def[of g])
 apply (erule bexE, simp)
 apply (simp add:image_def cmp_def)
 apply blast
done

lemma cmp_fun_sub_image:"f  A  B; g  B  C; A1  A 
                          (cmp g f) ` A1 =  g ` (f ` A1)"
apply (rule equalityI)
 apply (rule subsetI, simp add:image_def)
 apply (erule bexE, simp add:cmp_def, blast)
 apply (rule subsetI, simp add:image_def[of g])
 apply (erule bexE, simp)
 apply (simp add:image_def cmp_def)
 apply blast
done


lemma restrict_fun_eq:"xA. f x = g x  (λxA. f x) = (λxA. g x)"
 apply (simp add:fun_eq_iff)
done

lemma funcset_mem: "f  A  B; x  A  f x  B"
apply (simp add: Pi_def)
done

lemma img_subset:"f  A  B  f ` A  B"
apply (rule subsetI)
apply (simp add:image_def, erule bexE, simp)
apply (simp add:funcset_mem)
done

lemma funcset_mem1:"lA. f l  B; x  A  f x  B"
apply simp
done

lemma func_to_img:"f  A  B  f  A  f ` A"
by (simp add:Pi_def)

lemma funcset_eq:" f  extensional A; g  extensional A; xA. f x = g x    f = g"
apply (simp add:extensionalityI)
done

lemma eq_funcs:"f  A  B; g  A  B; f = g; x  A  f x = g x"
by simp

lemma restriction_of_domain:" f  A  B; A1  A  
  restrict f A1  A1  B"
by blast

lemma restrict_restrict:" restrict f A  A  B; A1  A  
      restrict (restrict f A) A1 = restrict f A1"
apply (rule funcset_eq[of _ "A1"])
 apply (simp add:restrict_def extensional_def)
 apply (simp add:restrict_def extensional_def)
apply (rule ballI) apply simp
 apply (simp add:subsetD)
done

lemma restr_restr_eq:" restrict f A  A  B; restrict f A = restrict g A;
A1  A   restrict f A1 = restrict g A1"
 apply (subst restrict_restrict[THEN sym, of "f" "A" "B" "A1"], assumption+)
 apply (simp add:restrict_restrict[THEN sym, of "g" "A" "B" "A1"])
done

lemma funcTr:" f  A  B; g  A  B; f = g; a  A  f a = g a"
apply simp
done

lemma funcTr1:"f = g; a  A  f a = g a"
apply simp
done

lemma restrictfun_im:" (restrict f A)  A  B; A1  A  
       (restrict f A) ` A1 = f ` A1"
apply (subgoal_tac "xA1. x  A")
apply (simp add:image_def)
apply (rule ballI) apply (simp add:subsetD)
done

lemma mem_in_image:" f  A  B; a  A  f a  f ` A "
apply (simp add:image_def)
 apply blast
done

lemma mem_in_image1:" lA. f l  B; a  A  f a  f ` A "
apply simp
done

lemma mem_in_image2:"a  A  f a  f ` A"
apply simp
done

lemma mem_in_image3:"b  f ` A  a  A. b = f a"
by (simp add:image_def)

lemma elem_in_image2: " f  A  B; A1  A; x  A1  f x  f` A1"
 apply (simp add:image_def)
 apply blast
 done

lemma funcs_nonempty:" A  {}; B  {}   (A  B)  {}"
apply (subgoal_tac "constmap A B  A  B") apply (simp add:nonempty)
apply (simp add:Pi_def)
 apply (rule allI) apply (rule impI)
 apply (simp add:constmap_def)
 apply (frule nonempty_ex[of "B"])
 apply (rule someI2_ex) apply assumption+
done

lemma idmap_funcs: "idmap A  A  A"
 apply (simp add:Pi_def restrict_def idmap_def)
 done


lemma l_idmap_comp: "f  extensional A; f  A  B 
                   compose A (idmap B) f = f"
apply (rule funcset_eq[of _ "A"])
 apply (simp add:compose_def)
 apply assumption
 apply (rule ballI)
 apply (simp add:funcset_mem[of "f" "A" "B"] compose_def idmap_def)
 done

lemma r_idmap_comp:"f  extensional A; f  A  B 
                                   compose A f (idmap A) = f"
apply (rule funcset_eq[of _ "A"])
 apply (simp add:compose_def)
 apply assumption
 apply (rule ballI)
 apply (simp add:funcset_mem[of "f" "A" "B"] compose_def idmap_def)
 done

lemma extend_fun: " f  A  B; B  B1   f  A  B1"
 apply (simp add:Pi_def restrict_def)
 apply (rule allI) apply (rule impI)
 apply (simp add:subsetD)
 done

lemma restrict_fun: " f  A  B; A1  A   restrict f A1  A1  B"
 apply (simp add:Pi_def restrict_def)
 apply (rule allI) apply (rule impI)
 apply (simp add:subsetD)
 done

lemma set_of_hom: "x  A. f x  B  restrict f A  A  B"
 apply (simp add:Pi_def restrict_def)
 done

lemma composition : " f  A   B; g  B  C  (compose A g f)  A   C"
 apply (simp add:Pi_def restrict_def compose_def)
 done

lemma comp_assoc:"f  A  B; g  B  C; h  C  D  
     compose A h (compose A g f) = compose A (compose B h g) f"
apply (rule funcset_eq[of _ "A"])
 apply (simp add:compose_def)
 apply (simp add:compose_def)
apply (rule ballI)
 apply (simp add:funcset_mem[of "f" "A" "B"] compose_def)
 done

lemma restrictfun_inj: " inj_on f A; A1  A   inj_on (restrict f A1) A1"
 apply (simp add:inj_on_def)
 apply (simp add:subsetD)
done

lemma restrict_inj:"inj_on f A; A1  A  inj_on f A1"
apply (simp add:inj_on_def)
 apply ((rule ballI)+, rule impI)
 apply (frule_tac c = x in subsetD[of "A1" "A"], assumption+,
        frule_tac c = y in subsetD[of "A1" "A"], assumption+)
 apply simp
done

lemma injective:" inj_on f A; x  A; y  A; x  y   f x  f y"
apply (rule contrapos_pp, simp+)
 apply (simp add:inj_on_def)
done

lemma injective_iff:" inj_on f A; x  A; y  A 
                        (x = y) = (f x = f y)"
apply (rule iffI, simp)
apply (rule contrapos_pp, simp+)
apply (frule injective[of "f" "A" "x" "y"], assumption+)
apply simp
done

lemma injfun_elim_image:"f  A  B; inj_on f A; x  A 
                f ` (A - {x}) = (f ` A) - {f x}"
apply (rule equalityI)
 apply (rule subsetI, simp add:image_def, erule bexE)
 apply (simp, (erule conjE)+)
 apply (rule contrapos_pp, simp+)
 apply (erule disjE, simp add:inj_on_def, blast)
 apply (frule_tac x = xaa and y = x in injective[of f A ], assumption+,
        blast)

 apply (rule subsetI, simp add:image_def)
 apply (rule contrapos_pp, simp+, erule conjE, erule bexE)
 apply (frule_tac x = xaa in bspec)
 apply (simp, rule contrapos_pp, simp+)
done

lemma cmp_inj:"f  A  B; g  B  C; inj_on f A; inj_on g B  
         inj_on (cmp g f) A"
apply (simp add:inj_on_def [of "cmp g f"])
apply (rule ballI)+
apply (simp add:cmp_def) apply (rule impI)
apply (subgoal_tac "f x = f y")
apply (simp add:inj_on_def [of "f"])
apply (frule_tac x = x in funcset_mem [of "f" "A" "B"], assumption+)
apply (frule_tac x = y in funcset_mem [of "f" "A" "B"], assumption+)
apply (simp add:inj_on_def [of "g"])
done

lemma cmp_assoc:"f  A  B; g  B  C; h  C  D; x  A 
                          (cmp h (cmp g f)) x  = (cmp (cmp h g) f) x"
apply (simp add:cmp_def)
done

lemma bivar_fun: " f  A  (B  C); a  A   f a  B  C"
by (simp add:Pi_def)

lemma bivar_fun_mem: " f  A  (B  C); a  A; b  B   f a b  C"
 apply (frule funcset_mem[of "f" "A" "B  C"], assumption+)
 apply (rule funcset_mem[of "f a" "B" "C"], assumption+)
 done

lemma bivar_func_eq:"aA. bB. f a b = g a b  
                         (λxA. λyB. f x y) =  (λxA. λyB. g x y)"
apply (subgoal_tac "xA. (λyB. f x y) = (λyB. g x y)")
apply (rule funcset_eq [of _ "A"])
 apply (simp add:extensional_def restrict_def)
 apply (simp add:extensional_def restrict_def)
 apply (rule ballI)
 apply simp
apply (rule ballI)
 apply (rule funcset_eq [of _ "B"])
 apply (simp add:restrict_def extensional_def)
 apply (simp add:restrict_def extensional_def)
apply (rule ballI) apply simp
done

lemma set_image: " f  A  B; A1  A; A2  A  
            f`(A1  A2)  (f` A1)  (f` A2)"
 apply (simp add: image_def)
 apply auto
 done

lemma image_sub: "f  A  B; A1  A   (f`A1)  B"
by (auto simp add:image_def)

lemma image_sub0: "f  A  B  (f`A)  B"
by (simp add:image_sub[of "f" "A" "B" "A"])

lemma image_nonempty:"f  A  B; A1  A; A1  {}   f ` A1  {}"
by (frule nonempty_some[of "A1"],
       frule elem_in_image2[of "f" "A" "B" "A1" "SOME x. x  A1"],
        assumption+, simp add:nonempty)

lemma im_set_mono: "f A  B; A1  A2; A2  A   (f ` A1)  (f ` A2)"
 apply (simp add:image_def)
 apply auto
 done

lemma im_set_un:" fA  B; A1  A; A2  A  
             f`(A1  A2) = (f`A1)  (f`A2)"
apply (simp add:image_def)
 apply auto
 done

lemma im_set_un1:"lA. f l  B; A = A1  A2 
                                f `(A1  A2) = f `(A1)  f `(A2)"
apply (rule equalityI,
       rule subsetI, simp add:image_def, erule bexE)
 apply blast
apply (rule subsetI,
       simp add:image_def, erule disjE, erule bexE, blast)
 apply (erule bexE) apply blast
done

lemma im_set_un2:"A = A1  A2   f `A = f `(A1)  f `(A2)"
apply (rule equalityI,
       rule subsetI, simp add:image_def, erule bexE, blast)
apply (rule subsetI,
       simp add:image_def, erule disjE, erule bexE, blast, erule bexE, blast)
done

definition
  invim::"['a  'b, 'a set, 'b set]  'a set" where
  "invim f A B = {x. xA  f x  B}"

lemma invim: " f:A  B; B1  B   invim f A B1  A"
  by (auto simp add:invim_def)

lemma setim_cmpfn: " f:A  B; g:B  C; A1  A  
               (compose A g f)` A1 = g`(f` A1)"
apply (simp add:image_def compose_def)
 apply auto
 done

definition
  surj_to :: "['a  'b, 'a set, 'b set]  bool" where
  "surj_to f A B  f`A = B"

lemma surj_to_test:" f  A  B; bB. aA. f a = b  
                                                  surj_to f A B"
by (auto simp add:surj_to_def image_def)

lemma surj_to_image:"f  A  B  surj_to f A (f ` A)"
apply (rule surj_to_test[of "f" "A" "f ` A"])
apply (rule func_to_img[of "f" "A" "B"], assumption)
apply (rule ballI, simp add:image_def, erule bexE, simp)
apply blast
done

lemma surj_to_el:" f  A  B; surj_to f A B   bB. aA. f a = b"
 apply (simp add:surj_to_def image_def)
 apply auto
 done

lemma surj_to_el1:" f  A  B; surj_to f A B; bB  aA. f a = b"
 apply (simp add:surj_to_el)
 done

lemma surj_to_el2:"surj_to f A B; b  B  aA. f a = b"
 apply (simp add:surj_to_def image_def)
 apply (frule sym, thin_tac "{y. xA. y = f x} = B", simp)
 apply (erule bexE, simp, blast)
done

lemma compose_surj: "f:A  B; surj_to f A B; g : B  C; surj_to g B C 
                          surj_to (compose A g f) A C "
apply (simp add:surj_to_def compose_def image_def)
 apply auto
 done

lemma cmp_surj: "f:A  B; surj_to f A B; g : B  C; surj_to g B C 
                          surj_to (cmp g f) A C "
apply (rule surj_to_test, simp add:cmp_fun)
apply (rule ballI, simp add:surj_to_def [of "g"], frule sym,
       thin_tac "g ` B = C", simp, simp add:image_def,
       simp add:cmp_def)
 apply auto
apply (simp add:surj_to_def, frule sym,
       thin_tac " f ` A = B", simp add:image_def)
 apply auto
done

lemma inj_onTr0:" f  A  B; x  A; y  A; inj_on f A; f x = f y  x = y"
apply (simp add:inj_on_def)
 done

lemma inj_onTr1:"inj_on f A; x  A; y  A; f x = f y   x = y"
apply (simp add:inj_on_def)
done

lemma inj_onTr2:"inj_on f A; x  A; y  A; f x  f y   x  y"
apply (rule contrapos_pp, simp+)
done  (* premis inj_on can be changed to some condition indicating f to be
         a function *)


lemma comp_inj: " f  A  B; inj_on f A; g  B  C; inj_on g B 
               inj_on (compose A g f) A "
apply (simp add:inj_on_def [of "compose A g f"])
 apply (rule ballI)+ apply (rule impI)
 apply (rule inj_onTr0 [of "f" "A" "B"], assumption+)
 apply (frule funcset_mem [of "f" "A" "B" _], assumption+)
 apply (rotate_tac -3)
 apply (frule funcset_mem [of "f" "A" "B" _], assumption+)
 apply (rule inj_onTr0 [of "g" "B" "C" _], assumption+)
 apply (simp add:compose_def)
 done

lemma cmp_inj_1: " f  A  B; inj_on f A; g  B  C; inj_on g B 
               inj_on (cmp g f) A "
apply (simp add:inj_on_def [of "cmp g f"])
apply (rule ballI)+ apply (rule impI)
apply (simp add:cmp_def)
apply (frule_tac x = x in funcset_mem [of "f" "A" "B"], assumption+)
apply (frule_tac x = y in funcset_mem [of "f" "A" "B"], assumption+)
apply (frule_tac x = "f x" and y = "f y" in inj_onTr1 [of "g" "B"],
                       assumption+)
apply (rule_tac x = x and y = y in inj_onTr1 [of "f" "A"], assumption+)
done

lemma cmp_inj_2: "lA. f l  B; inj_on f A; kB. g k  C; inj_on g B 
               inj_on (cmp g f) A "
apply (simp add:inj_on_def [of "cmp g f"])
apply (rule ballI)+ apply (rule impI)
apply (simp add:cmp_def)
apply (frule_tac x = x in funcset_mem1 [of "A" "f" "B"], assumption+)
apply (frule_tac x = y in funcset_mem1 [of "A" "f" "B"], assumption+)
apply (frule_tac x = "f x" and y = "f y" in inj_onTr1 [of "g" "B"],
                       assumption+)
apply (rule_tac x = x and y = y in inj_onTr1 [of "f" "A"], assumption+)
done

lemma invfun_mem:" f  A  B; inj_on f A; surj_to f A B; b  B 
                        (invfun A B f) b  A"
apply (simp add:invfun_def)
 apply (simp add:surj_to_def image_def) apply (frule sym)
 apply (thin_tac "{y. xA. y = f x} = B") apply simp
 apply (thin_tac "B = {y. xA. y = f x}") apply auto
 apply (rule someI2_ex)
 apply blast apply simp
 done


lemma inv_func:" f  A  B; inj_on f A; surj_to f A B
                        (invfun A B f)  B  A"
apply (simp add:Pi_def)
 apply (rule allI) apply (rule impI)
 apply (rule invfun_mem) apply (rule funcsetI)
 apply simp+
 done

lemma invfun_r:" fA  B; inj_on f A; surj_to f A B; b  B 
                       f ((invfun A B f) b) = b"
apply (simp add:invfun_def)
 apply (rule someI2_ex)
 apply (simp add:surj_to_def image_def)
 apply auto
 done

lemma invfun_l:"f  A  B; inj_on f A; surj_to f A B; a  A
                       (invfun A B f) (f a) = a"
apply (simp add:invfun_def Pi_def restrict_def)
apply (rule someI2_ex) apply auto
apply (simp add:inj_on_def)
done

lemma invfun_inj:"f  A  B; inj_on f A; surj_to f A B
                        inj_on (invfun A B f) B"
apply (simp add:inj_on_def [of "invfun A B f" "B"] )
 apply auto
 apply (frule_tac b = y in invfun_r [of "f" "A" "B"], assumption+)
 apply (frule_tac b = x in invfun_r [of "f" "A" "B"], assumption+)
 apply simp
 done

lemma invfun_surj:"f  A  B; inj_on f A; surj_to f A B
                        surj_to (invfun A B f) B A "
apply (simp add:surj_to_def [of "invfun A B f" "B" "A"] image_def)
apply (rule equalityI)
 apply (rule subsetI) apply (simp add:CollectI)
 apply auto
apply (simp add:invfun_mem)
apply (frule funcset_mem [of "f" "A" "B"], assumption+)
 apply (frule_tac t = x in invfun_l [of "f" "A" "B", THEN sym], assumption+)
 apply auto
done

definition
  bij_to :: "['a  'b, 'a set, 'b set]  bool" where
  "bij_to f A B  surj_to f A B  inj_on f A"

lemma idmap_bij:"bij_to (idmap A) A A"
apply (simp add:bij_to_def)
apply (rule conjI)
apply (simp add:surj_to_def, simp add:image_def, simp add:idmap_def)

apply (simp add:inj_on_def, simp add:idmap_def)
done

lemma bij_invfun:"f  A  B; bij_to f A B 
                              bij_to (invfun A B f) B A"
apply (simp add:bij_to_def)
apply (simp add:invfun_inj invfun_surj)
done

lemma l_inv_invfun:" f  A  B; inj_on f A; surj_to f A B
                       compose A (invfun A B f) f = idmap A"
apply (rule ext)
 apply (simp add:compose_def idmap_def)
apply (rule impI)
apply (simp add:invfun_l)
done

lemma invfun_mem1:"f  A  B; bij_to f A B; b  B 
                 (invfun A B f) b  A"
apply (simp add:bij_to_def, erule conjE)
apply (simp add:invfun_mem)
done

lemma invfun_r1:" fA  B; bij_to f A B; b  B 
                       f ((invfun A B f) b) = b"
apply (simp add:bij_to_def, erule conjE)
apply (rule invfun_r, assumption+)
done

lemma invfun_l1:"f  A  B; bij_to f A B; a  A
                       (invfun A B f) (f a) = a"
apply (simp add:bij_to_def, erule conjE)
apply (rule invfun_l, assumption+)
done

lemma compos_invfun_r:"f  A  B; bij_to f A B; g  A  C; h  B  C;
       g  extensional A; compose B g (invfun A B f) = h 
       g = compose A h f"
apply (rule funcset_eq[of g A "compose A h f"], assumption)
 apply (simp add:compose_def extensional_def)
 apply (rule ballI)
 apply (frule sym, thin_tac "compose B g (invfun A B f) = h", simp)
 apply (simp add:compose_def Pi_def invfun_l1)
done

lemma compos_invfun_l:"f  A  B; bij_to f A B; g  C  B; h  C  A;
       compose C (invfun A B f) g = h; g  extensional C  
                     g = compose C f h"
apply (rule funcset_eq[of g C "compose C f h"], assumption)
       apply (simp add:compose_def extensional_def)
apply (rule ballI)
apply (frule sym, thin_tac "compose C (invfun A B f) g = h",
       simp add:compose_def)
apply (frule_tac x = x in funcset_mem[of g C B], assumption)
apply (simp add:invfun_r1)
done

lemma invfun_set:"f  A  B; bij_to f A B; C  B 
                f ` ((invfun A B f)` C) = C"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add:image_def, erule exE,
        erule conjE, erule bexE, simp,
        frule_tac c = xb in subsetD[of "C" "B"], assumption+)
 apply (simp add:bij_to_def, erule conjE,
        simp add:invfun_r)

apply (rule subsetI, simp add:image_def)
 apply (frule_tac c = x in subsetD[of "C" "B"], assumption+,
        simp add:bij_to_def, erule conjE,
        frule_tac b = x in invfun_r[of "f" "A" "B"], assumption+)
 apply (frule sym, thin_tac "f (invfun A B f x) = x")
 apply blast
done

lemma compos_bij:"f  A  B; bij_to f A B; g  B  C; bij_to g B C 
                   bij_to (compose A g f) A C"
apply (simp add:bij_to_def, (erule conjE)+)
apply (simp add:comp_inj[of "f" "A" "B" "g" "C"])
apply (simp add:compose_surj)
done

section "Nsets"

 (* NSet is the set of natural numbers, and "Nset n" is the set of
natural numbers from 0 through n  *)

definition
  nset :: "[nat, nat]  (nat) set" where
  "nset i j = {k. i  k  k  j}"

definition
  slide :: "nat  nat  nat" where
  "slide i j == i + j"

definition
  sliden :: "nat  nat  nat" where
  "sliden i j == j - i"

definition
  jointfun :: "[nat, nat  'a, nat, nat  'a]  (nat  'a)" where
  "(jointfun n f m g) = (λi. if i  n then f i else  g ((sliden (Suc n)) i))"

definition
  skip :: "nat  (nat  nat)" where
  "skip i = (λx. (if i = 0 then Suc x else
                 (if x  {j. j  (i - Suc 0)} then x  else Suc x)))"

lemma nat_pos:"0  (l::nat)"
apply simp
done

lemma Suc_pos:"Suc k  r  0 < r"
apply simp
done

lemma nat_pos2:"(k::nat) < r  0 < r"
apply simp
done

lemma eq_le_not:"(a::nat)  b; ¬ a < b   a = b"
apply auto
done

lemma im_of_constmap:"(constmap {0} {a}) ` {0} = {a}"
apply (simp add:constmap_def)
done

lemma noteq_le_less:" m  (n::nat); m  n   m < n"
apply auto
done

lemma nat_not_le_less:"(¬ (n::nat)  m) = (m < n)"
by (simp add: not_le)

lemma self_le:"(n::nat)  n"
apply simp
done

lemma n_less_Suc:"(n::nat) < Suc n"
apply simp
done

lemma less_diff_pos:"i < (n::nat)  0 < n - i"
apply auto
done

lemma less_diff_Suc:"i < (n::nat)  n - (Suc i) = (n - i) - (Suc 0)"
apply auto
done

lemma less_pre_n:"0 < n  n - Suc 0 < n"
apply simp
done

lemma Nset_inc_0:"(0::nat)  {i. i  n}"
apply simp
done

lemma Nset_1:"{i. i  Suc 0} = {0, Suc 0}"
apply auto
done

lemma Nset_1_1:"(k  Suc 0) = (k = 0  k = Suc 0)"
apply (rule iffI)
apply (case_tac "k = 0", simp+)
apply (erule disjE, simp+)
done

lemma Nset_2:"{i, j} = {j, i}"
apply auto
done

lemma Nset_nonempty:"{i. i  (n::nat)}  {}"
apply (subgoal_tac "0  {i. i  n}")
apply (rule nonempty[of 0], assumption)
apply simp
done

lemma Nset_le:"x  {i. i  n}  x  n"
apply simp
done

lemma n_in_Nsetn:"(n::nat)  {i. i  n}"
apply simp
done

lemma Nset_pre:" (x::nat)  {i. i  (Suc n)}; x  Suc n   x  {i. i  n}"
apply simp
done

lemma Nset_pre1:"{i. i  (Suc n)} - {Suc n} = {i. i  n}"
apply (rule equalityI)
 apply (rule subsetI, simp)+
done

lemma le_Suc_mem_Nsetn:"x  Suc n  x - Suc 0  {i. i  n}"
apply (frule diff_le_mono[of x "Suc n" "Suc 0"],
       thin_tac "x  Suc n", simp)
done

lemma le_Suc_diff_le:"x  Suc n  x - Suc 0  n"
apply (frule diff_le_mono[of x "Suc n" "Suc 0"],
       thin_tac "x  Suc n", simp)
done

lemma Nset_not_pre:" x  {i. i  n}; x  {i. i  (Suc n)}  x = Suc n"
by simp

lemma mem_of_Nset:"x  (n::nat)  x  {i. i  n}"
apply simp
done

lemma less_mem_of_Nset:"x < (n::nat)  x  {i. i  n}"
apply (frule less_imp_le [of "x" "n"])
apply simp
done

lemma Nset_nset:"{i. i  (Suc (n + m))} = {i. i  n} 
                                            nset (Suc n) (Suc (n + m))"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add:nset_def)
  apply (auto simp add: nset_def)
done

lemma Nset_nset_1:"0 < n; i < n  {j. j  n} = {j. j  i} 
                                                           nset (Suc i) n"
apply auto
 apply (simp add:nset_def)
 apply (simp add:nset_def)
done

lemma Nset_img0:"f  {j. j  Suc n}  B; (f (Suc n))  f ` {j. j  n} 
                   f ` {j. j  Suc n} = f ` {j. j  n}"
  by (auto simp add: le_Suc_eq)

lemma Nset_img:"f  {j. j  Suc n}  B 
         insert (f (Suc n)) (f ` {j. j  n}) = f ` {j. j  Suc n}"
  by (auto elim: le_SucE)

primrec nasc_seq :: "[nat set, nat, nat]  nat"
where
  dec_seq_0: "nasc_seq A a 0 = a"
| dec_seq_Suc: "nasc_seq A a (Suc n) =
                     (SOME b. ((b  A)  (nasc_seq A a n) < b))"

lemma nasc_seq_mem:"(a::nat)  A; ¬ (m. mA  (xA. x  m)) 
                        (nasc_seq A a n)  A"
apply (induct n)
apply (simp_all add: not_le)
apply (subgoal_tac "xA. (nasc_seq A a n) < x") prefer 2 apply blast
 apply (thin_tac "m. m  A  (xA. m < x)",
        rule someI2_ex, blast, simp)
done

lemma nasc_seqn:"(a::nat)  A; ¬ (m. mA  (xA. x  m)) 
                               (nasc_seq A a n) < (nasc_seq A a (Suc n))"
apply (simp,
       frule nasc_seq_mem [of "a" "A" "n"], simp)
apply (simp add: not_le,
       subgoal_tac "xA. (nasc_seq A a n) < x") prefer 2 apply simp
 apply (thin_tac "m. m  A  (xA. m < x)",
        rule someI2_ex, blast, simp)
done

lemma nasc_seqn1:"(a::nat)  A; ¬ (m. mA  (xA. x  m)) 
                             Suc (nasc_seq A a n)  (nasc_seq A a (Suc n))"
apply (frule nasc_seqn [of "a" "A" "n"], assumption+)
 apply simp
done

lemma ubs_ex_n_maxTr:"(a::nat)  A; ¬ (m. mA  (xA. x  m))
        (a + n)  (nasc_seq A a n)"
apply (induct_tac n)
 apply simp
apply (frule_tac n = n in nasc_seqn1[of "a" "A"], assumption+,
       subgoal_tac "Suc (a + n)  Suc (nasc_seq A a n)",
       frule_tac i = "Suc (a + n)" and j = "Suc (nasc_seq A a n)" and
                  k = "nasc_seq A a (Suc n)" in le_trans, assumption+,
       simp, thin_tac "Suc (nasc_seq A a n)  nasc_seq A a (Suc n)",
       subst Suc_le_mono, assumption+)
done

lemma ubs_ex_n_max:"A  {}; A  {i. i  (n::nat)} 
                                      ∃!m. mA  (xA. x  m)"
apply (frule nonempty_ex[of "A"])
 apply (thin_tac "A  {}")
 apply (erule exE)
apply (rename_tac a)
apply (rule ex_ex1I)
prefer 2
 apply (erule conjE)+
 apply (frule_tac x = y in bspec, assumption+,
        thin_tac "xA. x  m",
        frule_tac x = m in bspec, assumption+,
        thin_tac "xA. x  y", simp)

apply (rule contrapos_pp, simp+)

apply (frule_tac a = a and A = A and n = "n + 1" in ubs_ex_n_maxTr, simp)
apply (frule_tac a = a in nasc_seq_mem[of _ "A" "n + 1"], simp)
apply (frule_tac c = "nasc_seq A a (n + 1)" in subsetD[of "A" "{i. i  n}"],
         assumption+, simp)
done

definition
  n_max :: "nat set  nat" where
  "n_max A = (THE m. m  A  (xA. x  m))"

lemma n_max:"A  {i. i  (n::nat)}; A  {} 
                    (n_max A)  A  (xA. x  (n_max A))"
apply (simp add:n_max_def)
apply (frule ubs_ex_n_max[of "A" "n"], assumption)
apply (rule theI')
apply assumption
done

lemma n_max_eq_sets:"A = B; A  {}; n. A  {j. j  n} 
                          n_max A = n_max B"
by simp
 (* n_max has no meaning unless conditions A ≠ {}; ∃n. A ⊆ {j. j ≤ n} *)

lemma skip_mem:"l  {i. i  n}  (skip i l)  {i. i  (Suc n)}"
apply (case_tac "i = 0")
 apply (simp add:skip_def)
 apply (simp)+
apply (simp add:skip_def)
done

lemma skip_fun:"(skip i)  {i. i  n}  {i. i  (Suc n)}"
apply (rule Pi_I)
apply (rule skip_mem, assumption)
done

lemma skip_im_Tr0:"x  {i. i  n}  skip 0 x = Suc x"
apply (simp add:skip_def)
done

lemma skip_im_Tr0_1:"0 < y  skip 0 (y - Suc 0) = y"
apply (simp add:skip_def)
done

lemma skip_im_Tr1:" i  {i. i  (Suc n)}; 0 < i; x  i - Suc 0  
           skip i x = x"
by (simp add:skip_def)

lemma skip_im_Tr1_1:" i  {i. i  (Suc n)}; 0 < i; x < i 
                       skip i x = x"
apply (frule less_le_diff[of x i])
apply (simp add:skip_def)
done

lemma skip_im_Tr1_2:" i  (Suc n); x < i   skip i x = x"
apply (rule skip_im_Tr1_1[of i n x], simp+)
done

lemma skip_im_Tr2:" 0 < i; i  {i. i  (Suc n)}; i  x 
      skip i x = Suc x"
by (simp add:skip_def)

lemma skip_im_Tr2_1:"i  {i. i  (Suc n)}; i  x 
                             skip i x = Suc x"
apply (case_tac "i = 0")
   apply (simp add:skip_def)
apply (simp, rule skip_im_Tr2, assumption+, simp+)
done

lemma skip_im_Tr3:"x  {i. i  n}  skip (Suc n) x = x"
apply (simp add:skip_def)
done

lemma skip_im_Tr4:"x  Suc n; 0 < x  x - Suc 0  n"
 apply (simp add:Suc_le_mono [of "x - Suc 0" "n", THEN sym])
done

lemma skip_fun_im:"i  {j. j  (Suc n)} 
              (skip i) ` {j. j  n} = ({j. j  (Suc n)} - {i})"
apply (rule equalityI)
 apply (rule subsetI)
 apply (case_tac "i = 0", simp)
 apply (simp add:image_def, erule exE, erule conjE)
 apply (cut_tac x = xa in skip_im_Tr0[of _ n], simp, simp)

 apply (simp add:image_def, erule exE, erule conjE, simp)
 apply (case_tac "xa < i")
 apply (frule_tac x = xa in skip_im_Tr1_2[of i n], simp+)
 apply (cut_tac m1 = xa and n1 = i in nat_not_le_less[THEN sym], simp)
 apply (cut_tac x = xa and n = n in skip_im_Tr2_1[of i], simp+)

apply (rule subsetI, simp, erule conjE)
 apply (cut_tac x = x and y = i in less_linear, simp)
 apply (erule disjE)
 apply (simp add:image_def)
 apply (frule_tac x = x in skip_im_Tr1_2[of i n], assumption,
        frule_tac x = x and y = i and z = "Suc n" in less_le_trans,
        assumption+,
        frule_tac m = x and n = "Suc n" in Suc_leI,
        simp only:Suc_le_mono,
        frule sym, thin_tac "skip i x = x", blast)
 apply (cut_tac x = "x - Suc 0" in skip_im_Tr2_1[of i n],
        simp, simp add:less_le_diff)
 apply (cut_tac x = i and n = x in less_le_diff, assumption,
        simp add:image_def)
 apply (frule_tac m = x and n = "Suc n" and l = "Suc 0" in diff_le_mono,
        simp)
 apply (frule sym, thin_tac "skip i (x - Suc 0) = x", blast)
done

lemma skip_fun_im1:"i  {j. j  (Suc n)}; x  {j. j  n} 
                      (skip i) x  ({j. j  (Suc n)} - {i})"
by (subst skip_fun_im[THEN sym], assumption,
    simp add:image_def, blast)

lemma skip_id:"l < i  skip i l = l"
apply (simp add:skip_def )
 done

lemma Suc_neq:"0 < i; i - Suc 0 < l  i  Suc l"
by (rule contrapos_pp, simp+)

lemma skip_il_neq_i:"skip i l  i"
apply (auto simp add:skip_def)
done

lemma skip_inj:"i  {k. k  n}; j  {k. k  n}; i  j 
                         skip k i  skip k j"
apply (simp add:skip_def)
done

lemma le_imp_add_int:" i  (j::nat)  k. j = i + k"
 apply (case_tac "i = j")
 apply simp
 apply (frule le_imp_less_or_eq) apply (thin_tac "i  j")
 apply simp
 apply (insert less_imp_add_positive [of "i" "j"])
 apply simp
 apply blast
 done

lemma jointfun_hom0:" f  {j. j  n}  A; g  {k. k  m}  B  
        (jointfun n f m g)  {l. l  (Suc (n + m))}   (A  B)"
by (simp add:jointfun_def sliden_def Pi_def)

lemma jointfun_mem:"j  (n::nat). f j  A; j  m. g j  B;
             l  (Suc (n + m))  (jointfun n f m g) l  (A  B)"
apply (rule funcset_mem[of "jointfun n f m g" "{j. j  Suc (n + m)}" "A  B"
       l])
apply (rule jointfun_hom0)
apply simp+
done

lemma jointfun_inj:"f  {j. j  n}  B; inj_on f {j. j  n};
      b  f ` {j. j  n} 
      inj_on (jointfun n f 0 (λk{0::nat}. b)) {j. j  Suc n}"
  apply (simp add:inj_on_def, (rule allI, rule impI)+, rule impI)
  apply (case_tac "x = Suc n", simp)
        apply (case_tac "y = Suc n", simp)
        apply (frule_tac m = y and n = "Suc n" in noteq_le_less, assumption)
           apply (
               frule_tac x = y and n = "Suc n" in less_le_diff,
               thin_tac "y < Suc n", thin_tac "y  Suc n",
               simp add:jointfun_def sliden_def)
      apply (case_tac "y = Suc n", simp,
             frule_tac m = x and n = "Suc n" in noteq_le_less, assumption,
             frule_tac x = x and n = "Suc n" in less_le_diff,
             thin_tac "x < Suc n", thin_tac "x  Suc n",
             simp add:jointfun_def sliden_def)
      apply (rotate_tac -3, frule sym, thin_tac " f x = b", simp)
      apply (frule_tac m = x and n = "Suc n" in noteq_le_less, assumption,
             frule_tac x = x and n = "Suc n" in less_le_diff,
             thin_tac "x < Suc n", thin_tac "x  Suc n", simp,
             frule_tac m = y and n = "Suc n" in noteq_le_less, assumption,
             frule_tac x = y and n = "Suc n" in less_le_diff,
             thin_tac "y < Suc n", thin_tac "y  Suc n", simp,
             simp add:jointfun_def)
done

lemma slide_hom:"i  j  (slide i)  {l. l  (j - i)}  nset i j"
apply (simp add:Pi_def restrict_def)
apply (rule allI) apply (rule impI)
   apply (simp add:slide_def)
apply (simp add:nset_def)
done

lemma slide_mem:" i  j; l  {k. k  (j - i)}  slide i l  nset i j"
apply (frule slide_hom)
apply (rule funcset_mem, assumption+)
done

lemma slide_iM:"(slide i) ` {l. 0  l} = {k. i  k}"
apply (simp add:image_def slide_def)
apply (rule equalityI)
 apply (rule subsetI)
 apply simp
 apply auto
 apply (rule le_imp_add_int)
 apply assumption
done

lemma jointfun_hom:" f  {i. i  n}  A; g  {j. j  m}  B  
                   (jointfun n f m g)  {j. j  (Suc (n + m))}  A  B"
by (simp add:sliden_def Pi_def jointfun_def)

lemma im_jointfunTr1:"(jointfun n f m g) ` {i. i  n} = f ` {i. i  n}"
apply auto
  apply (simp add:jointfun_def)

  apply (simp add:jointfun_def)
 done

lemma im_jointfunTr2:"(jointfun n f m g) ` (nset (Suc n) (Suc (n + m))) =
                       g ` ({j. j  m})"
apply auto
 apply (simp add:nset_def) apply auto
 apply (frule_tac m = xa and n = "Suc (n + m)" and l = "Suc n" in diff_le_mono)
  apply simp
  apply (simp add:jointfun_def sliden_def)

 apply (simp add:image_def)
  apply (cut_tac le_add1[of "n" "m"],
         simp only:Suc_le_mono[THEN sym, of "n" "n+m"])
  apply (frule_tac l = xa in slide_mem[of "Suc n" "Suc (n + m)"])
  apply simp
 apply (subst jointfun_def)
  apply (subgoal_tac "inset (Suc n) (Suc (n+m)). ¬ (i  n) ")
  apply simp
  apply (thin_tac "inset (Suc n) (Suc (n + m)). ¬ i  n")
  apply (subgoal_tac "g xa = g (sliden (Suc n) (slide (Suc n) xa))")
  apply blast
  apply (simp add:slide_def sliden_def)
  apply (auto simp add: nset_def)
done

lemma im_jointfun:"f  {j. j  n}  A; g  {j. j  m}  B 
    (jointfun n f m g) `({j. j  (Suc (n + m))}) =
                           f `{j. j  n}  g `{j. j   m}"
 apply (cut_tac im_set_un1 [of "{j. j  (Suc (n + m))}" "jointfun n f m g"
        "A  B"  "{i. i  n}" "nset (Suc n) (Suc (n + m))"])
 apply (simp add:Nset_nset[THEN sym, of n m],
        simp add:im_jointfunTr1[of n f m g],
        simp add:im_jointfunTr2[of n f m g])
 apply (rule ballI)
 apply (simp add:jointfun_def,
        case_tac "l  n", simp add:Pi_def,
        simp add:sliden_def,
        simp add:nat_not_le_less,
        frule_tac m = n and n = l in Suc_leI,
        frule_tac m = l and n = "Suc (n + m)" and l = "Suc n" in diff_le_mono,
        thin_tac "l  Suc (n + m)", simp,
        simp add:Pi_def)
apply (simp add:Nset_nset[of n m])
done

lemma im_jointfun1:"(jointfun n f m g) `({j. j  (Suc (n + m))}) =
                                      f `{j. j  n}  g ` {j. j  m}"
apply (cut_tac Nset_nset[of "n" "m"])
apply (subst  im_set_un2[of "{j. j  (Suc (n + m))}" "{j. j  n}"
              "nset (Suc n) (Suc (n + m))" "jointfun n f m g"], assumption)
apply (simp add:im_jointfunTr1 im_jointfunTr2)
done

lemma jointfun_surj:"f  {j. j  n}  A; surj_to f {j. j  (n::nat)} A;
      g  {j. j  (m::nat)}  B; surj_to g {j. j  m} B 
       surj_to (jointfun n f m g) {j. j  Suc (n + m)} (A  B)"
 apply (simp add:surj_to_def [of "jointfun n f m g"])
 apply (simp add:im_jointfun)
 apply (simp add:surj_to_def)
 done

lemma Nset_un:"{j. j  (Suc n)} = {j. j  n}  {Suc n}"
apply (rule equalityI)
apply (rule subsetI)
 apply simp
 apply auto
done

lemma Nsetn_sub: "{j. j  n}  {j. j  (Suc n)}"
apply (rule subsetI)
apply simp
done

lemma Nset_pre_sub:"(0::nat) < k  {j. j  (k - Suc 0)}  {j. j  k}"
apply (rule subsetI)
apply simp
done

lemma Nset_pre_un:"(0::nat) < k  {j. j  k} = {j. j  (k - Suc 0)}  {k}"
apply (insert Nset_un [of "k - Suc 0"])
apply simp
done

lemma Nsetn_sub_mem:" l  {j. j  n}  l  {j. j  (Suc n)}"
apply simp
done

lemma Nsetn_sub_mem1:"j. j  {j. j  n}  j  {j. j  (Suc n)}"
by (simp add:Nsetn_sub_mem)

lemma Nset_Suc:"{j. j  (Suc n)} = insert (Suc n) {j. j  n}"
apply (rule equalityI)
apply (rule subsetI)
apply simp
apply auto
done

lemma nsetnm_sub_mem:"j. j nset n (n + m)  j  nset n (Suc (n + m))"
by (rule allI, simp add:nset_def)

lemma Nset_0:"{j. j  (0::nat)} = {0}"
by simp

lemma Nset_Suc0:"{i. i  (Suc 0)} = {0, Suc 0}"
apply (rule equalityI)
 apply (rule subsetI, simp)
 apply (case_tac "x = 0", simp)
 apply simp+
done

lemma Nset_Suc_Suc:"Suc (Suc 0)  n 
       {j. j  (n - Suc (Suc 0))} = {j. j  n} - {n - Suc 0, n}"
apply (insert Nset_un [of "n - (Suc 0)"])
apply (insert Nset_un [of "n - Suc (Suc 0)"])
apply (subgoal_tac "{j. j  (Suc (n - Suc (Suc 0)))} = {j. j  (n - Suc 0)}")
apply (simp,
       thin_tac "{j. j  n} =
       insert n (insert (Suc (n - Suc (Suc 0))) {j. j  n - Suc (Suc 0)})",
       thin_tac " {j. j  n - Suc 0} =
        insert (Suc (n - Suc (Suc 0))) {j. j  n - Suc (Suc 0)}",
       thin_tac "{j. j  Suc (n - Suc (Suc 0))} =
        insert (Suc (n - Suc (Suc 0))) {j. j  n - Suc (Suc 0)}")
apply (simp add:Suc_Suc_Tr)
apply (auto )
done

lemma func_pre:"f  {j. j  (Suc n)}  A  f  {j. j  n}  A"
by (simp add:Pi_def)

lemma image_Nset_Suc:"f ` ({j. j  (Suc n)}) =
                             insert (f (Suc n)) (f ` {j. j  n})"
apply (cut_tac Nset_un[of "n"])
apply (frule im_set_un2[of "{j. j  (Suc n)}" "{j. j  n}" "{Suc n}" "f"])
apply (simp add:Un_commute)
done

definition
  Nleast :: "nat set  nat" where
  "Nleast A = (THE a. (a  A  (xA. a  x)))"

definition
  Nlb :: "[nat set, nat]  bool" where
  "Nlb A n  (aA. n  a)"


primrec ndec_seq :: "[nat set, nat, nat]  nat" where
  ndec_seq_0  :"ndec_seq A a 0 = a"
| ndec_seq_Suc:"ndec_seq A a (Suc n) =
                      (SOME b. ((b  A)  b < (ndec_seq A a n)))"

lemma ndec_seq_mem:"a  (A::nat set); ¬ (m. mA  (xA. m  x)) 
                        (ndec_seq A a n)  A"
apply (induct_tac n)
 apply simp apply simp
 apply (simp add: not_less [symmetric])
apply (subgoal_tac "xA. x < (ndec_seq A a n)") prefer 2 apply blast
 apply (thin_tac "m. m  A  (xA. x < m)")
 apply (rule someI2_ex) apply blast
apply simp
done

lemma ndec_seqn:"a  (A::nat set);¬ (m. mA  (xA. m  x)) 
                       (ndec_seq A a (Suc n)) < (ndec_seq A a n)"
 apply (frule ndec_seq_mem [of "a" "A" "n"], assumption+)
 apply simp
 apply (simp add: not_less [symmetric])
 apply (subgoal_tac "xA. x < (ndec_seq A a n)") prefer 2 apply simp
 apply (thin_tac "m. m  A  (xA. x < m)")
apply (rule someI2_ex) apply blast
 apply simp
done

lemma ndec_seqn1:"a  (A::nat set); ¬ (m. mA  (xA. m  x)) 
                       (ndec_seq A a (Suc n))  (ndec_seq A a n) - 1"
apply (frule ndec_seqn [of "a" "A" "n"], assumption+,
       thin_tac "¬ (m. m  A  (xA. m  x))")
 apply (simp del:ndec_seq_Suc)
done

lemma ex_NleastTr:"a  (A::nat set); ¬ (m. mA  (xA. m  x)) 
                        (ndec_seq A a n)  (a - n)"
apply (induct_tac n)
 apply simp
apply (frule_tac n = n in ndec_seqn1[of "a" "A"], assumption+)
 apply (subgoal_tac "ndec_seq A a n - 1  (a - n) - 1") prefer 2
  apply arith
  apply arith
done

lemma nat_le:"((a::nat) - (a + 1))  0"
apply arith
done

lemma ex_Nleast:"(A::nat set)  {}  ∃!m. mA  (xA. m  x)"
apply (frule nonempty_ex[of "A"], thin_tac "A  {}",
       erule exE, rename_tac a)
apply (case_tac "0  A")
 apply (rule ex_ex1I, subgoal_tac "xA. 0  a", blast,
        rule ballI, simp)
 apply ((erule conjE)+,
        subgoal_tac "m  0", thin_tac "xA. m  x",
        subgoal_tac "y  0", thin_tac "xA. y  x",
        simp, blast, blast)
apply (rule ex_ex1I)
prefer 2 apply (erule conjE)+
  apply (subgoal_tac "m  y", thin_tac "xA. m  x",
         subgoal_tac "y  m", thin_tac "xA. y  x",
         simp, blast, blast)
apply (rule contrapos_pp, simp,
       frule_tac a = a and A = A and n = "a + 1" in ex_NleastTr, assumption+)
 apply (subgoal_tac "(a - (a + 1))  0")
 prefer 2 apply (rule nat_le)
 apply (frule_tac i = "ndec_seq A a (a + 1)" and j = "a - (a + 1)" and k = 0 in le_trans, assumption+,
        frule_tac a = a and n = "a + 1" in ndec_seq_mem [of _ "A"],
                                                          assumption+)
 apply (thin_tac "¬ (m. m  A  (xA. m  x))",
        thin_tac "ndec_seq A a (a + 1)  a - (a + 1)",
        thin_tac "a - (a + 1)  0")
apply simp
done

lemma Nleast:"(A::nat set)  {}  Nleast A  A  (xA. (Nleast A)  x)"
apply (frule ex_Nleast [of "A"])
 apply (simp add:Nleast_def)
 apply (rule theI')
 apply simp
done

subsection "Lemmas for existence of reduced chain."
(* Later some of these lemmas should be removed. *)

lemma jointgd_tool1:" 0 < i  0  i - Suc 0"
by arith

lemma jointgd_tool2:" 0 < i  i = Suc (i - Suc 0)"
by arith

lemma jointgd_tool3:"0 < i;  i  m  i - Suc 0  (m - Suc 0)"
by arith

lemma jointgd_tool4:"n < i  i - n = Suc( i - Suc n)"
by arith

lemma pos_prec_less:"0 < i  i - Suc 0 < i"
by arith

lemma Un_less_Un:"f  {j. j  (Suc n)}  (X::'a set set);
        A  (f ` {j. j  (Suc n)});
       i  {j. j  (Suc n)}; j  {l. l  (Suc n)}; i  j  f i  f j
        A  (compose {j. j  n} f (skip i) ` {j. j  n})"
apply (simp add:compose_def)
 apply (rule subsetI, simp)
 apply (frule_tac c = x and A = A and B = "x{j. j  Suc n}. f x" in
        subsetD, assumption+, simp)
 apply (erule exE, (erule conjE)+)
 apply (case_tac "xa = i", simp,
        frule_tac c = x in subsetD[of "f i" "f j"], assumption+)
 apply (cut_tac less_linear[of i j], simp, erule disjE,
        frule less_le_diff[of i j],
        cut_tac skip_im_Tr2_1[of i n "j - Suc 0"],
        simp,
        frule eq_elems_eq_val[THEN sym, of "skip i (j - Suc 0)" j f],
        cut_tac a = x in eq_set_inc[of _ "f j" "f (skip i (j - Suc 0))"],
              assumption+,
        frule le_Suc_diff_le[of j n], blast, simp, assumption, simp)
 apply (frule  skip_im_Tr1_2[of i n j], assumption,
        frule eq_elems_eq_val[THEN sym, of "skip i j" j f])
 apply (cut_tac a = x in eq_set_inc[of _ "f j" "f (skip i j)"],
              assumption+)
 apply (frule_tac x = j and y = i and z = "Suc n" in less_le_trans,
        assumption+,
        frule Suc_less_le[of j n], blast)
 apply (cut_tac x = xa and y = i in less_linear, simp,
        erule disjE,
        frule_tac x = xa in skip_im_Tr1_2[of i n], assumption)
 apply (frule_tac x1 = "skip i xa" and y1 = xa and f1 = f in
                  eq_elems_eq_val[THEN sym],
        frule_tac a = x and A = "f xa" and B = "f (skip i xa)" in eq_set_inc,
        assumption,
        frule_tac x = xa and y = i and z = "Suc n" in less_le_trans,
        assumption+,
        frule_tac x = xa and n = n in Suc_less_le, blast)
 apply (frule_tac x = i and n = xa in less_le_diff,
        cut_tac x = "xa - Suc 0" and n = n in skip_im_Tr2_1 [of i],
        simp, assumption,
        simp,
        frule_tac x1 = "skip i (xa - Suc 0)" and y1 = xa and f1 = f in
                  eq_elems_eq_val[THEN sym],
        frule_tac a = x and A = "f xa" and B = "f (skip i (xa - Suc 0))" in
        eq_set_inc, assumption,
        frule_tac x = xa and n = n in le_Suc_diff_le)
        apply blast
done

section "Lower bounded set of integers"

(* In this section. I prove that a lower bounded set of integers
  has the minimal element *)

definition "Zset = {x. (n::int). x = n}"

definition
  Zleast :: "int set  int" where
  "Zleast A = (THE a. (a  A  (xA. a  x)))"

definition
  LB :: "[int set, int]  bool" where
  "LB A n = (aA. n  a)"

lemma linorder_linear1:"(m::int) < n  n  m"
apply (subgoal_tac "m < n  n = m  n < m")
apply (case_tac "m < n") apply simp apply simp
apply (subgoal_tac "m < n  m = n  n < m")
apply blast
apply (simp add:less_linear)
done

primrec dec_seq :: "[int set, int, nat]  int"
where
  dec_seq_0: "dec_seq A a 0 = a"
| dec_seq_Suc: "dec_seq A a (Suc n) = (SOME b. ((b  A)  b < (dec_seq A a n)))"

lemma dec_seq_mem:"a  A; A  Zset;¬ (m. mA  (xA. m  x)) 
                        (dec_seq A a n)  A"
apply (induct_tac n)
 apply simp apply simp  apply (simp add:not_zle)
apply (subgoal_tac "xA. x < (dec_seq A a n)") prefer 2 apply blast
 apply (thin_tac "m. m  A  (xA. x < m)")
 apply (rule someI2_ex) apply blast
apply simp
done

lemma dec_seqn:"a  A; A  Zset;¬ (m. mA  (xA. m  x)) 
                       (dec_seq A a (Suc n)) < (dec_seq A a n)"
apply simp
 apply (frule dec_seq_mem [of "a" "A" "n"], assumption+)
 apply simp
 apply (simp add:not_zle)
 apply (subgoal_tac "xA. x < (dec_seq A a n)") prefer 2 apply simp
 apply (thin_tac "m. m  A  (xA. x < m)")
apply (rule someI2_ex) apply blast
 apply simp
done

lemma dec_seqn1:"a  A; A  Zset;¬ (m. mA  (xA. m  x)) 
                       (dec_seq A a (Suc n))  (dec_seq A a n) - 1"
apply (frule dec_seqn [of "a" "A" "n"], assumption+)
 apply simp
done

lemma lbs_ex_ZleastTr:"a  A; A  Zset;¬ (m. mA  (xA. m  x)) 
                        (dec_seq A a n)  (a - int(n))"
apply (induct_tac n)
 apply simp
apply (frule_tac n = n in dec_seqn1[of "a" "A"], assumption+)
 apply (subgoal_tac "dec_seq A a n - 1  a - (int n) - 1") prefer 2
   apply simp apply (thin_tac "dec_seq A a n  a - int n")
 apply (frule_tac x = "dec_seq A a (Suc n)" and y = "dec_seq A a n - 1" and
 z = "a - int n - 1" in order_trans, assumption+)
 apply (thin_tac "¬ (m. m  A  (xA. m  x))")
 apply (thin_tac "dec_seq A a (Suc n)  dec_seq A a n - 1")
 apply (thin_tac "dec_seq A a n - 1  a - int n - 1")
apply (subgoal_tac "a - int n - 1 = a - int (Suc n)") apply simp
 apply (thin_tac "dec_seq A a (Suc n)  a - int n - 1")
apply simp
done

lemma big_int_less:"a - int(nat(abs(a) + abs(N) + 1)) < N"
apply (simp add:zabs_def)
done

lemma lbs_ex_Zleast:"A  {}; A  Zset; LB A n  ∃!m. mA  (xA. m  x)"
apply (frule nonempty_ex[of "A"])
 apply (thin_tac "A  {}")
 apply (erule exE)
 apply (rename_tac a)
apply (rule ex_ex1I)
prefer 2
 apply (thin_tac "LB A n") apply (erule conjE)+
 apply (subgoal_tac "m  y") prefer 2 apply simp
 apply (subgoal_tac "y  m") prefer 2 apply simp
 apply (thin_tac "xA. m  x") apply (thin_tac "xA. y  x")
 apply simp
apply (rule contrapos_pp) apply simp
 apply (frule_tac a = a and A = A and n = "nat(abs(a) + abs(n) + 1)" in lbs_ex_ZleastTr, assumption+)
 apply (subgoal_tac "a - int(nat(abs(a) + abs(n) + 1)) < n")
 prefer 2 apply (rule big_int_less)
 apply (frule_tac x = "dec_seq A a (nat (¦a¦ + ¦n¦ + 1))" and y = "a - int (nat (¦a¦ + ¦n¦ + 1))" and z = n in order_le_less_trans, assumption+)
 apply (frule_tac a = a and n = "nat (¦a¦ + ¦n¦ + 1)" in dec_seq_mem [of _ "A"], assumption+)
 apply (thin_tac "¬ (m. m  A  (xA. m  x))")
 apply (thin_tac "dec_seq A a (nat (¦a¦ + ¦n¦ + 1))
            a - int (nat (¦a¦ + ¦n¦ + 1))")
 apply (thin_tac "a - int (nat (¦a¦ + ¦n¦ + 1)) < n")
apply (simp add:LB_def)
 apply (subgoal_tac "n  dec_seq A a (nat (¦a¦ + ¦n¦ + 1))")
 apply (thin_tac "aA. n  a") apply (simp add:not_zle)
 apply blast
done

lemma Zleast:"A  {}; A  Zset; LB A n  Zleast A  A 
               (xA. (Zleast A)  x)"
apply (frule lbs_ex_Zleast [of "A" "n"], assumption+)
 apply (simp add:Zleast_def)
 apply (rule theI')
 apply simp
done

lemma less_convert1:" a = c; a < b   c < b"
apply auto
done

lemma less_convert2:"a = b; b < c  a < c"
apply auto
done

section ‹Augmented integer: integer and ∞-∞›

definition
  zag :: "(int * int) set" where
  "zag = {(x,y) | x y. x * y = (0::int)  (y = -1  y = 0  y = 1)}"

definition
  zag_pl::"[(int * int), (int * int)]  (int * int)" where
  "zag_pl x y == if (snd x + snd y) = 2 then (0, 1)
                 else if (snd x + snd y) = 1 then (0, 1)
                 else if (snd x + snd y) = 0 then (fst x + fst y, 0)
                 else if (snd x + snd y) = -1 then (0, -1)
                 else if (snd x + snd y) = -2 then (0, -1) else undefined"

definition
  zag_t :: "[(int * int), (int * int)]  (int * int)" where
  "zag_t x y = (if (snd x)*(snd y) = 0 then
                     (if 0 < (fst x)*(snd y) + (snd x)*(fst y) then (0,1)
                           else (if (fst x)*(snd y) + (snd x)*(fst y) = 0
                               then ((fst x)*(fst y), 0) else (0, -1)))
            else (if 0 < (snd x)*(snd y) then (0, 1) else (0, -1)))"

definition "Ainteg = zag"

typedef ant = Ainteg
  morphisms Rep_Ainteg Abs_Ainteg
  unfolding Ainteg_def
proof
  show "(1, 0)  zag" unfolding zag_def by auto
qed

definition
  ant :: "int  ant" where
  "ant m = Abs_Ainteg( (m, 0))"

definition
  tna :: "ant  int" where
  "tna z = (if Rep_Ainteg(z)  (0,1)  Rep_Ainteg(z)  (0,-1) then
            fst (Rep_Ainteg(z)) else undefined)"

instantiation ant :: "{zero, one, plus, uminus, minus, times, ord}"
begin

definition
  Zero_ant_def  : "0 == ant 0"

definition
  One_ant_def   : "1 == ant 1"

definition
  add_ant_def:
   "z + w ==
       Abs_Ainteg (zag_pl (Rep_Ainteg z) (Rep_Ainteg w))"

definition
  minus_ant_def : "- z ==
         Abs_Ainteg((- (fst (Rep_Ainteg z)), - (snd (Rep_Ainteg z))))"

definition
    diff_ant_def:  "z - (w::ant) == z + (-w)"

definition
    mult_ant_def:
      "z * w ==
       Abs_Ainteg (zag_t (Rep_Ainteg z) (Rep_Ainteg w))"

definition
    le_ant_def:
     "(z::ant)  w == if (snd (Rep_Ainteg w)) = 1 then True
       else (if (snd (Rep_Ainteg w)) = 0 then (if (snd (Rep_Ainteg z)) = 1
       then False else (if (snd (Rep_Ainteg z)) = 0 then
        (fst (Rep_Ainteg z))  (fst (Rep_Ainteg w))  else True))
          else (if snd (Rep_Ainteg z) = -1 then True else False))"

definition
    less_ant_def: "((z::ant) < (w::ant)) == (z  w  z  w)"

instance ..

end

definition
  inf_ant :: ant  ("") where
  " = Abs_Ainteg((0,1))"

definition
  an :: "nat  ant" where
  "an m = ant (int m)"

definition
  na :: "ant  nat" where
  "na x = (if (x < 0) then 0 else
           if x   then (nat (tna x)) else undefined)"

definition
  UBset :: "ant  ant set" where
  "UBset z = {(x::ant).  x  z}"

definition
   LBset :: "ant  ant set" where
  "LBset z = {(x::ant). z  x}"

lemma ant_z_in_Ainteg:"(z::int, 0)  Ainteg"
apply (simp add:Ainteg_def zag_def)
done

lemma ant_inf_in_Ainteg:"((0::int), 1)  Ainteg"
apply (simp add:Ainteg_def zag_def)
done

lemma ant_minf_in_Ainteg:"((0::int), -1)  Ainteg"
apply (simp add:Ainteg_def zag_def)
done

lemma ant_0_in_Ainteg:"((0::int), 0)  Ainteg"
apply (simp add:Ainteg_def zag_def)
done

lemma an_0[simp]:"an 0 = 0"
by (simp add:an_def Zero_ant_def)

lemma an_1[simp]:"an 1 = 1"
by (simp add:an_def One_ant_def)

lemma mem_ant:"(a::ant) = -  ((z::int). a = ant z)  a = "
apply (case_tac "a = -  a = ")
 apply blast
apply (simp, simp add:ant_def,
       cut_tac Rep_Ainteg[of "a"],
       simp add:Ainteg_def zag_def,
       erule conjE, simp add:inf_ant_def,
       simp add:minus_ant_def,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply auto
apply (cut_tac Rep_Ainteg[of "a"],
       subgoal_tac "Abs_Ainteg (Rep_Ainteg a) = Abs_Ainteg ((0,-1))",
       thin_tac "Rep_Ainteg a = (0, -1)",
       simp add:Rep_Ainteg_inverse, simp)
apply (cut_tac Rep_Ainteg[of "a"],
       subgoal_tac "Abs_Ainteg (Rep_Ainteg a) = Abs_Ainteg ((0,0))",
       thin_tac "Rep_Ainteg a = (0, 0)",
       simp add:Rep_Ainteg_inverse, blast, simp)
apply (cut_tac Rep_Ainteg[of "a"],
       subgoal_tac "Abs_Ainteg (Rep_Ainteg a) = Abs_Ainteg ((0,1))",
       thin_tac "Rep_Ainteg a = (0, 1)",
       simp add:Rep_Ainteg_inverse, simp)
apply (cut_tac Rep_Ainteg[of "a"],
       subgoal_tac "Abs_Ainteg (Rep_Ainteg a) = Abs_Ainteg ((x,0))",
       thin_tac "Rep_Ainteg a = (x, 0)",
       simp add:Rep_Ainteg_inverse, blast, simp)
done

lemma minf:"- = Abs_Ainteg((0,-1))"
apply (simp add:inf_ant_def minus_ant_def,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
done

lemma z_neq_inf[simp]:"(ant z)   "
apply (rule contrapos_pp, simp+)
apply (simp add:ant_def inf_ant_def)
apply (subgoal_tac "Rep_Ainteg (Abs_Ainteg (z,0)) =
                      Rep_Ainteg (Abs_Ainteg (0,1))",
       thin_tac "Abs_Ainteg (z, 0) = Abs_Ainteg (0, 1)",
       cut_tac ant_z_in_Ainteg[of "z"],
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply simp
done

lemma z_neq_minf[simp]:"(ant z)  -"
apply (rule contrapos_pp, simp+)
apply (subgoal_tac "ant (-z) = ")
apply (cut_tac z_neq_inf[of "- z"], simp)
apply (simp add:ant_def inf_ant_def minus_ant_def)
apply (cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (subgoal_tac "- Abs_Ainteg (z, 0) = - Abs_Ainteg (0, -1)",
       thin_tac "Abs_Ainteg (z, 0) = Abs_Ainteg (0, -1)",
       simp add:minus_ant_def,
       cut_tac ant_z_in_Ainteg[of "z"],
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply simp
done

lemma minf_neq_inf[simp]:"-  "
apply (cut_tac ant_inf_in_Ainteg,
       simp add:inf_ant_def minus_ant_def Abs_Ainteg_inverse)
apply (rule contrapos_pp, simp+,
       subgoal_tac "Rep_Ainteg (Abs_Ainteg (0,-1)) =
                     Rep_Ainteg (Abs_Ainteg (0,1))",
       thin_tac "Abs_Ainteg (0, -1) = Abs_Ainteg (0, 1)",
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply simp
done


lemma a_ipi[simp]:" +  = "
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:zag_pl_def)
done

lemma a_zpi[simp]:"(ant z) +   = "
apply (simp add:add_ant_def inf_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "z"],
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:zag_pl_def)
done

lemma a_ipz[simp]:"  + (ant z) = "
apply (simp add:add_ant_def inf_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "z"],
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:zag_pl_def)
done

lemma a_zpz:"(ant m) + (ant n) = ant (m + n)"
apply (simp add:add_ant_def inf_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       cut_tac ant_z_in_Ainteg[of "n"],
       simp add:Abs_Ainteg_inverse,
       simp add:zag_pl_def)
done

lemma a_mpi[simp]:"- +   = 0"
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse,
       simp add:Zero_ant_def ant_def zag_pl_def)
done

lemma a_ipm[simp]:" + (-) = 0"
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse,
       simp add:Zero_ant_def ant_def zag_pl_def)
done

lemma a_mpm[simp]:"- + (-) = -"
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse,
       simp add:Zero_ant_def ant_def zag_pl_def)
done

lemma a_mpz[simp]:"- + (ant m) = -"
apply (simp add:add_ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_pl_def)
done

lemma a_zpm[simp]:"(ant m) + (-) = -"
apply (simp add:add_ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_pl_def)
done

lemma a_mdi[simp]:"- -   = - "
apply (simp add:diff_ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (simp add:add_ant_def,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_pl_def)
done

lemma a_zdz:"(ant m) - (ant n) = ant (m - n)"
apply (simp add:diff_ant_def minus_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "n"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:add_ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       cut_tac ant_z_in_Ainteg[of "-n"],
       simp add:Abs_Ainteg_inverse zag_pl_def)
done

lemma a_i_i[simp]:" *  = "
apply (simp add:mult_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_0_i[simp]:"0 *  = 0"
by (simp add:mult_ant_def inf_ant_def Zero_ant_def, simp add:ant_def,
    cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_i_0[simp]:" * 0 = 0"
by (simp add:mult_ant_def inf_ant_def Zero_ant_def, simp add:ant_def,
    cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_0_m[simp]:"0 * (-) = 0"
by (simp add:mult_ant_def inf_ant_def Zero_ant_def, simp add:ant_def,
    cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_m_0[simp]:"(-) * 0 = 0"
by (simp add:mult_ant_def inf_ant_def Zero_ant_def, simp add:ant_def,
    cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_m_i[simp]:"(-) *  = -"
by (simp add:mult_ant_def inf_ant_def minus_ant_def,
       cut_tac ant_inf_in_Ainteg, cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_i_m[simp]:" * (-) = - "
by (simp add:mult_ant_def inf_ant_def minus_ant_def,
       cut_tac ant_inf_in_Ainteg, cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse, simp add:zag_t_def)

lemma a_pos_i[simp]:"0 < m  (ant m) *  = "
apply (simp add:mult_ant_def inf_ant_def ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_i_pos[simp]:"0 < m   * (ant m) = "
apply (simp add:mult_ant_def inf_ant_def ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_neg_i[simp]:"m < 0  (ant m) *  = -"
apply (simp add:mult_ant_def inf_ant_def ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_i_neg[simp]:"m < 0   * (ant m) = -"
apply (simp add:mult_ant_def inf_ant_def ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done


lemma a_z_z:"(ant m) * (ant n) = ant (m*n)"
apply (simp add:mult_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       cut_tac ant_z_in_Ainteg[of "n"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_pos_m[simp]:"0 < m  (ant m) * (-) = -"
apply (simp add:mult_ant_def inf_ant_def minus_ant_def ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "m"],
      simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_m_pos[simp]:"0 < m  (-) * (ant m) = -"
apply (simp add:mult_ant_def inf_ant_def minus_ant_def ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "m"],
      simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_neg_m[simp]:"m < 0  (ant m) * (-) = "
apply (simp add:mult_ant_def inf_ant_def minus_ant_def ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "m"],
      simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma neg_a_m[simp]:"m < 0  (-) * (ant m) = "
apply (simp add:mult_ant_def inf_ant_def minus_ant_def ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "m"],
      simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done

lemma a_m_m[simp]:"(-) * (-) = "
apply (simp add:mult_ant_def inf_ant_def minus_ant_def ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      simp add:Abs_Ainteg_inverse)
apply (simp add:zag_t_def)
done


lemma inj_on_Abs_Ainteg:"inj_on Abs_Ainteg Ainteg"
apply (simp add:inj_on_def)
apply (rule ballI)+
apply (rule impI,
       subgoal_tac "Rep_Ainteg (Abs_Ainteg x) = Rep_Ainteg (Abs_Ainteg y)",
       thin_tac "Abs_Ainteg x = Abs_Ainteg y",
       simp add:Abs_Ainteg_inverse, simp)
done

lemma an_Suc:"an (Suc n) = an n + 1"
    apply (subst an_1[THEN sym])
    apply (simp del:an_1 add:an_def)
    apply (simp del:an_1 add:a_zpz, simp add:add.commute)
done

lemma aeq_zeq [iff]: "(ant m = ant n) = (m = n)"
apply (rule iffI)
apply (subgoal_tac "Rep_Ainteg (ant m) = Rep_Ainteg (ant n)",
       thin_tac "ant m = ant n",
       cut_tac ant_z_in_Ainteg[of "m"],
       cut_tac ant_z_in_Ainteg[of "n"],
       simp add:ant_def Abs_Ainteg_inverse)
apply simp+
done

lemma aminus:"- ant m = ant (-m)"
apply (simp add:ant_def minus_ant_def,
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)
done

lemma aminusZero:"- ant 0 = ant 0"
apply (simp add:aminus)
done

lemma  ant_0: "ant 0 = (0::ant)"
by (simp add: Zero_ant_def)

lemma inf_neq_0[simp]:"  0"
apply (cut_tac z_neq_inf[of "0"], frule not_sym)
apply (simp add:ant_0)
done

lemma zero_neq_inf[simp]:"0  "
by (cut_tac inf_neq_0, frule not_sym, simp)

lemma minf_neq_0[simp]:"-  0"
apply (cut_tac z_neq_minf[of "0"], frule not_sym)
apply (simp add:ant_0)
done

lemma zero_neq_minf[simp]:"0  -"
by (cut_tac minf_neq_0, frule not_sym, simp)

lemma a_minus_zero[simp]:"-(0::ant) = 0"
by (cut_tac aminusZero, simp add:ant_0)

lemma a_minus_minus: "- (- z) = (z::ant)"
apply (cut_tac mem_ant[of "z"])
apply (erule disjE, simp add:minf, simp add: minus_ant_def,
       cut_tac ant_minf_in_Ainteg,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (erule disjE) apply (erule exE, simp add:aminus)
apply (simp add:minf, simp add: minus_ant_def,
       cut_tac ant_minf_in_Ainteg,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:inf_ant_def)
done

lemma aminus_0: "- (- 0) = (0::ant)"
apply (simp add:a_minus_minus)
done

lemma a_a_z_0:" 0 < z; a * ant z = 0  a = 0"
by (rule contrapos_pp, simp+, cut_tac mem_ant[of "a"], erule disjE,
       simp, erule disjE, erule exE, simp add:a_z_z,
       simp only:ant_0[THEN sym], simp, simp)

lemma adiv_eq:" z  0; a * (ant z) = b * (ant z)  a = b"
apply (cut_tac mem_ant[of "a"], cut_tac mem_ant[of "b"],
      (erule disjE)+, simp, erule disjE, erule exE,
       cut_tac less_linear[of "z" "0"], erule disjE, simp add:a_z_z,
       frule sym, thin_tac " = ant (za * z)", simp,
       simp add:a_z_z, frule sym, thin_tac "-  = ant (za * z)", simp,
       cut_tac less_linear[of "z" "0"], erule disjE, simp,
       simp, erule disjE, erule exE)
apply (erule disjE,
        cut_tac less_linear[of "z" "0"], simp,
        erule disjE, simp add:a_z_z, simp add:a_z_z,
        erule disjE, erule exE, simp add:a_z_z,
        cut_tac less_linear[of "z" "0"], simp,
        erule disjE, simp add:a_z_z, simp add:a_z_z,
        erule disjE,
        cut_tac less_linear[of "z" "0"], simp,
        erule disjE, simp+)
apply (erule disjE, erule exE, simp add:a_z_z,
        cut_tac less_linear[of "z" "0"], simp, erule disjE, simp,
        frule sym, thin_tac "-  = ant (za * z)", simp,
        simp, frule sym, thin_tac " = ant (za * z)", simp,
        cut_tac less_linear[of "z" "0"], simp)
done

lemma aminus_add_distrib: "- (z + w) = (- z) + (- w::ant)"
apply (cut_tac mem_ant[of "z"], cut_tac mem_ant[of "w"],
       (erule disjE)+, simp add:a_minus_minus,
       erule disjE, erule exE, simp,
       simp add:a_minus_minus aminus, simp add:a_minus_minus)
apply ((erule disjE)+, erule exE,
       simp add:a_minus_minus, simp add:aminus,
       simp add:a_minus_minus)
apply ((erule disjE)+, (erule exE)+, simp add:a_zpz aminus,
      erule exE, simp add:aminus,
      erule disjE, erule exE, simp add:aminus, simp)
done

lemma aadd_commute:"(x::ant) + y = y + x"
apply (cut_tac mem_ant[of "x"], cut_tac mem_ant[of "y"])
apply (erule disjE, erule disjE, simp,
      erule disjE, erule exE, simp+,
      (erule disjE)+, erule exE, simp+)
apply ((erule disjE)+, (erule exE)+, simp add:a_zpz,
      erule exE, simp, erule disjE, erule exE, simp+)
done

definition
  aug_inf :: "ant set"  ("Z") where
  "Z = {(z::ant). z  - }"

definition
  aug_minf :: "ant set"  ("Z-") where
  "Z- = {(z::ant). z   }"

lemma z_in_aug_inf:"ant z  Z"
apply (simp add:aug_inf_def)
done

lemma Zero_in_aug_inf:"0  Z"
by (simp only:Zero_ant_def, simp add: aug_inf_def)

lemma z_in_aug_minf:"ant z  Z-"
by (simp add:aug_minf_def)

lemma mem_aug_minf:"a  Z-  a = -   (z. a = ant z)"
by (cut_tac mem_ant[of a], simp add:aug_minf_def)

lemma minus_an_in_aug_minf:" - an n   Z-"
apply (simp add:an_def)
apply (simp add:aminus)
apply (simp add:z_in_aug_minf)
done

lemma Zero_in_aug_minf:"0  Z-"
by (simp add:Zero_ant_def aug_minf_def)

lemma aadd_assoc_i: "x  Z; y  Z; z  Z  (x + y) + z = x + (y + z)"
apply (cut_tac mem_ant[of "x"],
       cut_tac mem_ant[of "y"],
       cut_tac mem_ant[of "z"], simp add:aug_inf_def,
      (erule disjE)+, (erule exE)+, (simp add:a_zpz)+,
      (erule exE)+, simp add:a_zpz)
apply ((erule disjE)+, (erule exE)+, simp,
        erule exE, simp,
      (erule disjE)+, (erule exE)+, simp add:a_zpz,
      erule exE, simp, erule disjE, erule exE, simp)
apply simp
done

lemma aadd_assoc_m: "x  Z-; y  Z-; z  Z- 
                                 (x + y) + z = x + (y + z)"
apply (cut_tac mem_ant[of "x"],
       cut_tac mem_ant[of "y"],
       cut_tac mem_ant[of "z"], simp add:aug_minf_def )
apply ((erule disjE)+, simp, erule exE, simp,
       erule disjE, erule exE, simp, (erule exE)+, simp add:a_zpz)
apply ((erule disjE)+, erule exE, simp, (erule exE)+, simp,
        erule disjE, erule exE, simp, erule exE, simp add:a_zpz)
apply ((erule exE)+, simp add:a_zpz)
done

lemma aadd_0_r: "x + (0::ant) = x"
apply (cut_tac mem_ant[of "x"], simp add:Zero_ant_def)
apply ((erule disjE)+, simp)
apply (erule disjE, erule exE, simp add:a_zpz,
       simp)
done

lemma aadd_0_l: "(0::ant) + x = x"
apply (cut_tac mem_ant[of "x"], simp add:Zero_ant_def)
apply ((erule disjE)+, simp)
apply (erule disjE, erule exE, simp, simp add:a_zpz, simp)
done

lemma aadd_minus_inv: "(- x) + x = (0::ant)"  (** ⟶ aadd_minus_l **)
apply (cut_tac mem_ant[of "x"],
       erule disjE, simp add:a_minus_minus,
       erule disjE, erule exE, simp add:aminus, simp add:a_zpz,
       simp add:Zero_ant_def, simp)
done

lemma aadd_minus_r: "x + (- x) = (0::ant)"
apply (cut_tac  aadd_minus_inv[of "x"])
apply (simp add:aadd_commute)
done

lemma ant_minus_inj:"ant z  ant w  - ant z  - ant w"
by (simp add:aminus)

lemma aminus_mult_minus: "(- (ant z)) * (ant w) = - ((ant z) * (ant w))"
apply (simp add:ant_def minus_ant_def,
       cut_tac ant_z_in_Ainteg[of "z"],
       cut_tac ant_z_in_Ainteg[of "-z"],
       cut_tac ant_z_in_Ainteg[of "w"],
       simp add:Abs_Ainteg_inverse)
apply (simp add:mult_ant_def) apply (simp add:Abs_Ainteg_inverse,
       simp add:zag_t_def,
       cut_tac ant_z_in_Ainteg[of "z * w"])
apply (simp add:Abs_Ainteg_inverse)
done

lemma amult_commute: "(x::ant) * y = y * x"
apply (cut_tac mem_ant[of "x"],
       cut_tac mem_ant[of "y"])
apply (erule disjE, erule disjE, simp)
apply (erule disjE, erule exE, simp)
apply (cut_tac x = 0 and y = z in less_linear)
apply (erule disjE, simp)
apply (erule disjE, rotate_tac -1, frule sym, thin_tac "0 = z", simp)
apply (simp add:inf_ant_def ant_def, simp add:minus_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_z_in_Ainteg[of "0"],
       cut_tac ant_z_in_Ainteg[of "-1"],
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (simp add:mult_ant_def, simp add:Abs_Ainteg_inverse,
       simp add:zag_t_def, simp)
apply (simp add:inf_ant_def)
apply (simp add:mult_ant_def minus_ant_def,
        cut_tac ant_inf_in_Ainteg,
        simp add:Abs_Ainteg_inverse,
        cut_tac ant_minf_in_Ainteg,
        simp add:Abs_Ainteg_inverse, simp add:zag_t_def)
apply (erule disjE, erule disjE, simp)
apply (erule exE,
       cut_tac x = 0 and y = z in less_linear)
apply (erule disjE, simp)
apply (erule disjE, rotate_tac -1, thin_tac "0 = z", simp add:mult_ant_def,
      simp add:ant_def inf_ant_def minus_ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac z = z in ant_z_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      simp add:Abs_Ainteg_inverse, simp add:zag_t_def,
      simp)
apply (simp add:inf_ant_def minus_ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac z = z in ant_z_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      simp add:Abs_Ainteg_inverse,
      simp add:mult_ant_def,
      simp add:Abs_Ainteg_inverse, simp add:zag_t_def)
apply ((erule disjE)+, (erule exE)+, simp add:a_z_z)
apply (erule exE,
       cut_tac  x = 0 and y = z in less_linear,
       erule disjE, simp)
apply (erule disjE, rotate_tac -1, frule sym, thin_tac "0 = z", simp,
      simp add:mult_ant_def ant_def inf_ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "0"],
      simp add:Abs_Ainteg_inverse, simp add:zag_t_def,
      simp)
apply (erule disjE, erule exE,
       cut_tac  x = 0 and y = z in less_linear,
       erule disjE, simp,
      erule disjE, rotate_tac -1, frule sym, thin_tac "0 = z", simp,
      simp add:mult_ant_def ant_def inf_ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_z_in_Ainteg[of "0"],
      simp add:Abs_Ainteg_inverse, simp add:zag_t_def,
      simp+)
done

lemma z_le_i[simp]:"(ant x)   "
apply (simp add:le_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "0"],
       cut_tac ant_z_in_Ainteg[of "x"],
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:inf_ant_def,
       simp add:Abs_Ainteg_inverse)
done

lemma z_less_i[simp]:"(ant x) <  "
apply (cut_tac z_le_i[of "x"],
       cut_tac z_neq_inf[of "x"],
       simp add:less_ant_def)
done

lemma m_le_z:"-  (ant x) "
apply (simp add:le_ant_def ant_def,
       cut_tac ant_z_in_Ainteg[of "0"],
       cut_tac ant_z_in_Ainteg[of "x"],
       cut_tac ant_minf_in_Ainteg,
       cut_tac ant_inf_in_Ainteg,
       simp add:Abs_Ainteg_inverse,
       simp add:inf_ant_def,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse)
done

lemma m_less_z[simp]:"- < (ant x)"
apply (cut_tac m_le_z[of "x"],
       cut_tac z_neq_minf[of "x"],
       frule not_sym, thin_tac "ant x  - ",
       simp add:less_ant_def)
done

lemma noninf_mem_Z:"x  Z; x    (z::int). x = ant z"
apply (simp add:aug_inf_def)
apply (cut_tac mem_ant[of "x"], simp)
done

lemma z_mem_Z:"ant z  Z"
by (simp add:aug_inf_def)

lemma inf_ge_any[simp]:"x  "
apply (cut_tac mem_ant[of "x"], erule disjE)
 apply (simp add:inf_ant_def minus_ant_def,
        cut_tac ant_minf_in_Ainteg,
        cut_tac ant_inf_in_Ainteg,
        simp add:Abs_Ainteg_inverse,
        simp add:le_ant_def, simp add:Abs_Ainteg_inverse)
 apply (erule disjE, erule exE, simp)
 apply (simp add:inf_ant_def,
        cut_tac ant_inf_in_Ainteg,
        simp add:le_ant_def, simp add:Abs_Ainteg_inverse)
done

lemma zero_lt_inf:"0 < "
by (simp add:less_ant_def)

lemma minf_le_any[simp]:"-  x"
apply (cut_tac mem_ant[of "x"], erule disjE)
 apply (simp add:inf_ant_def minus_ant_def,
        cut_tac ant_minf_in_Ainteg,
        cut_tac ant_inf_in_Ainteg,
        simp add:Abs_Ainteg_inverse,
        simp add:le_ant_def, simp add:Abs_Ainteg_inverse)
 apply (erule disjE, erule exE, simp)
 apply (simp add:inf_ant_def, simp add:minus_ant_def,
        cut_tac ant_inf_in_Ainteg,
        cut_tac ant_minf_in_Ainteg,
        simp add:le_ant_def, simp add:Abs_Ainteg_inverse)
 apply simp
done

lemma minf_less_0:"- < 0"
by (simp add:less_ant_def)

lemma ale_antisym[simp]:"(x::ant)  y; y  x   x = y"
apply (rule contrapos_pp, simp+)
apply (cut_tac  mem_ant[of "x"], cut_tac  mem_ant[of "y"])
apply (erule disjE, erule disjE, simp)
apply (erule disjE, erule exE, simp, simp add:ant_def,
      simp add:minus_ant_def inf_ant_def,
      cut_tac ant_inf_in_Ainteg,
      cut_tac ant_minf_in_Ainteg,
      cut_tac z = z in ant_z_in_Ainteg, simp add:Abs_Ainteg_inverse,
      simp add:le_ant_def Abs_Ainteg_inverse)
apply (thin_tac "x  y",
       simp add:le_ant_def ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply (erule disjE, erule disjE, erule exE,
       thin_tac "y  x",
       simp add:le_ant_def ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       cut_tac z = z in ant_z_in_Ainteg, simp add:Abs_Ainteg_inverse)
apply (thin_tac "y  x",
       simp add:le_ant_def ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:Abs_Ainteg_inverse)
apply ((erule disjE)+, (erule exE)+,
       cut_tac z = z in ant_z_in_Ainteg,
       cut_tac z = za in ant_z_in_Ainteg,
       simp add:le_ant_def ant_def,
       simp add:Abs_Ainteg_inverse)
apply (erule exE,
        simp add:le_ant_def ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac z = z in ant_z_in_Ainteg, simp add:Abs_Ainteg_inverse)
apply (erule disjE, erule exE, thin_tac "y  x",
       simp add:le_ant_def ant_def minus_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       cut_tac z = z in ant_z_in_Ainteg, simp add:Abs_Ainteg_inverse)
apply simp
done

lemma x_gt_inf[simp]:"  x  x = "
apply (cut_tac inf_ge_any[of "x"],
       rule ale_antisym[of "x" ""], assumption+)
done

lemma Zinf_pOp_closed:"x  Z; y  Z  x + y  Z"
apply (cut_tac  mem_ant[of "x"], cut_tac  mem_ant[of "y"],
       simp add:aug_inf_def,
      (erule disjE)+, (erule exE)+, simp add:a_zpz,
       cut_tac z = "-(z + za)" in z_neq_inf,
       rule contrapos_pp, simp+,
       cut_tac m1 = "z+za" in aminus[THEN sym], simp add:a_minus_minus,
       erule exE, simp, simp add:minf_neq_inf[THEN not_sym],
       erule disjE, erule exE, simp,
       simp add:minf_neq_inf[THEN not_sym],
       simp)
done

lemma Zminf_pOp_closed:"x  Z-; y  Z-  x + y  Z-"
apply (cut_tac  mem_ant[of "x"], cut_tac  mem_ant[of "y"],
       simp add:aug_minf_def,
      (erule disjE)+, simp, erule exE, simp,
       erule disjE, erule exE, simp,
      (erule exE)+, simp add:a_zpz)
done

lemma amult_distrib1:"(ant z)  0 
             (a + b) * (ant z) = a * (ant z) + b * (ant z)"
apply (cut_tac mem_ant[of "a"], cut_tac mem_ant[of "b"],
     (erule disjE)+, simp, cut_tac less_linear[of "z" "0"],
      erule disjE, simp, erule disjE, simp, simp add:ant_0, simp,
      erule disjE, erule exE, simp,
      cut_tac less_linear[of "z" "0"],
      erule disjE, simp add:a_z_z, erule disjE, simp add:ant_0,
      simp add:a_z_z,
      cut_tac less_linear[of "z" "0"], simp,
      erule disjE, simp add:ant_0[THEN sym] a_z_z)
apply (erule disjE, simp add:ant_0[THEN sym],
       simp, simp add:ant_0[THEN sym], simp add:a_z_z,
       (erule disjE)+, (erule exE)+, cut_tac less_linear[of "z" "0"], simp,
       erule disjE, simp add:a_z_z,
       erule disjE, simp add:ant_0, simp add:a_z_z,
       cut_tac less_linear[of "z" "0"],
       erule disjE, simp add:ant_0[THEN sym])
apply (simp add:a_z_z, simp,
       erule disjE, simp add:ant_0, simp add:ant_0[THEN sym] a_z_z,
      (erule disjE)+, (erule exE)+, simp add:a_zpz a_z_z,
       simp add: distrib_right, erule exE, simp add:a_z_z,
       cut_tac less_linear[of "z" "0"], erule disjE, simp,
       erule disjE, simp add:ant_0, simp)
apply (erule disjE, erule exE, simp,
       cut_tac less_linear[of "z" "0"], erule disjE, simp add:a_z_z,
       erule disjE, simp add:ant_0, simp add:a_z_z,
       cut_tac less_linear[of "z" "0"], erule disjE, simp,
       erule disjE, simp add:ant_0, simp)
done

lemma amult_0_r:"(ant z) * 0 = 0"
by (simp add:ant_0[THEN sym] a_z_z)

lemma amult_0_l:"0 * (ant z) = 0"
by (simp add:ant_0[THEN sym] a_z_z)


definition
  asprod :: "[int, ant]  ant" (infixl "*a" 200) where
  "m *a x ==
  if x =  then (if 0 < m then  else (if m < 0 then - else
                 if m = 0 then 0 else undefined))
    else (if x = - then
                    (if 0 < m then - else (if m < 0 then  else
                 if m = 0 then 0 else undefined))
          else (ant m) * x)"

lemma asprod_pos_inf[simp]:"0 < m  m *a  = "
apply (simp add:asprod_def)
done

lemma asprod_neg_inf[simp]:"m < 0  m *a  = -"
apply (simp add:asprod_def)
done

lemma asprod_pos_minf[simp]:"0 < m  m *a (-) = (-)"
apply (simp add:asprod_def)
done

lemma asprod_neg_minf[simp]:"m < 0  m *a (-) = "
apply (simp add:asprod_def)
done

lemma asprod_mult:" m *a (ant n) = ant(m * n)"
apply (cut_tac z_neq_inf[of "n"],
       cut_tac z_neq_minf[of "n"],
       simp add:asprod_def, simp add:a_z_z)
done

lemma asprod_1:"1 *a x = x"
by (cut_tac mem_ant[of "x"], erule disjE, simp,
       erule disjE, erule exE, simp add:asprod_mult, simp)
(** atode asprod_1_x to awaseru **)

lemma agsprod_assoc_a:"m *a (n *a (ant x)) = (m * n) *a (ant x)"
apply (simp add:asprod_mult)
done

lemma agsprod_assoc:"m  0; n  0  m *a (n *a x) = (m * n) *a x"
apply (cut_tac less_linear[of "m" "0"], cut_tac less_linear[of "n" "0"],
       cut_tac mem_ant[of "x"],
      (erule disjE)+, simp,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp)
apply (erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp+,
      erule disjE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp,
      erule disjE, erule exE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp add:asprod_mult,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp)
apply (simp, (erule disjE)+,
      frule zmult_pos_neg[of "m" "n"], assumption+,
      simp,
      erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_pos_neg[of "m" "n"], assumption+, simp)
apply (frule zmult_pos_pos[of "m" "n"], assumption+,
      erule disjE, simp,
      erule disjE, erule exE, simp add:asprod_mult, simp)
done

lemma asprod_distrib1:"m  0  m *a (x + y) = (m *a x) + (m *a y)"
apply (cut_tac mem_ant[of "x"], cut_tac mem_ant[of "y"])
apply (cut_tac less_linear[of "m" "0"],
      erule disjE,
      erule disjE, erule disjE, simp,
      erule disjE, simp add:asprod_def  add_ant_def, simp,
      simp, (erule disjE)+, erule exE, simp add:asprod_mult,
      simp add:Zero_ant_def asprod_mult)
apply (erule disjE, erule exE, simp add:asprod_mult,
      simp add: Zero_ant_def asprod_mult,
      erule disjE, erule disjE, erule disjE, erule exE,
      simp add:asprod_mult,
      simp add:Zero_ant_def asprod_mult,
      erule disjE, erule exE, simp add:asprod_mult,
      simp add:Zero_ant_def asprod_mult)
apply (simp, erule disjE, erule exE, simp,
      (erule disjE)+, erule exE, simp add:asprod_mult,
      simp add:a_zpz, simp add:asprod_mult distrib_left,
      simp add:asprod_mult)
apply (erule disjE, erule exE, simp add:a_zpz asprod_mult,
       simp add: distrib_left, simp add:asprod_mult,
      (erule disjE)+, erule exE, simp add:asprod_mult, simp,
      erule disjE, erule exE, simp add:asprod_mult, simp)
done

lemma asprod_0_x[simp]:"0 *a x = 0"
 apply (simp add:asprod_def, (rule impI)+,
        cut_tac mem_ant[of "x"], simp, erule exE,
        simp add:asprod_def a_z_z, simp add:ant_0)
done

lemma asprod_n_0:"n *a 0 = 0"
apply (simp add:Zero_ant_def asprod_mult)
done

lemma asprod_distrib2:"0 < i; 0 < j  (i + j) *a x = (i *a x) + (j *a x)"
by (cut_tac mem_ant[of "x"], erule disjE, simp,
       erule disjE, erule exE, simp add:asprod_mult,
       simp add: distrib_right a_zpz, simp)

lemma asprod_minus:"x  -  x    - z *a x = z *a (- x)"
apply (cut_tac mem_ant[of "x"], erule disjE, simp+)
apply (erule exE, simp add:asprod_mult aminus)
done

lemma asprod_div_eq:"n  0; n *a x = n *a y  x = y"
apply (cut_tac less_linear[of "n" "0"], simp)
apply (cut_tac mem_ant[of "x"], cut_tac mem_ant[of "y"])
apply ((erule disjE)+, simp,
      erule disjE, erule exE, rule contrapos_pp, simp+,
      simp add:asprod_mult)
apply (cut_tac z1 = "n * z" in z_neq_inf[THEN not_sym], simp+)
apply ((erule disjE)+, erule exE, simp add:asprod_mult,
       cut_tac z = "n * z" in z_neq_inf,
       rule contrapos_pp, simp, simp,
      (erule disjE)+, (erule exE)+, simp add:asprod_mult,
       erule exE, simp add: asprod_mult)
apply (erule disjE, erule exE, simp add:asprod_mult,
      simp add:z_neq_minf[THEN not_sym], simp)
apply ((erule disjE)+, simp,
      erule disjE, erule exE, rule contrapos_pp, simp+,
      simp add:asprod_mult,
      cut_tac z1 = "n * z" in z_neq_minf[THEN not_sym], simp,
      rule contrapos_pp, simp+)
apply ((erule disjE)+, (erule exE)+, simp add:asprod_mult,
      erule exE, simp add:asprod_mult,
      erule disjE, erule exE, simp add:asprod_mult
      z_neq_inf[THEN not_sym], simp)
apply (erule disjE, simp, erule disjE, erule exE, simp add:asprod_mult
        z_neq_inf[THEN not_sym], simp)
done

lemma asprod_0:"z  0; z *a x = 0   x = 0"
by (rule asprod_div_eq[of "z" "x" "0"], assumption, simp add:asprod_n_0)

lemma asp_z_Z:"z *a ant x  Z"
by (simp add:asprod_mult z_in_aug_inf)

lemma tna_ant:" tna (ant z) = z"
apply (cut_tac z_neq_minf[of "z"], cut_tac z_neq_inf[of "z"],
       simp add:ant_def tna_def)
apply (cut_tac ant_z_in_Ainteg[of "z"], simp add:Abs_Ainteg_inverse)
done

lemma ant_tna:"x    x  -   ant (tna x) = x"
apply (cut_tac mem_ant[of "x"], simp, erule exE)
apply (simp add:ant_def tna_def)
apply (cut_tac z = z in ant_z_in_Ainteg, simp add:Abs_Ainteg_inverse)
done

lemma ant_sol:"a  Z; b  Z; c  Z; b  ; a = b + c  a - b = c"
apply (subgoal_tac "-b  Z", simp add:diff_ant_def,
       subgoal_tac "a + (-b) = b + c + (-b)",
       subst aadd_commute[of "b" "c"], subst aadd_assoc_i, assumption+,
       simp add:aadd_minus_r, simp add:aadd_0_r, simp)
apply (cut_tac mem_ant[of "b"], simp add:aug_inf_def,
       erule exE, simp add:aminus)
done

subsection "Ordering of integers and ordering nats"

subsection ‹The ≤› Ordering›

lemma zneq_aneq:"(n  m) = ((ant n)  (ant m))"
apply (rule iffI)
 apply (rule contrapos_pp, simp+)
done

lemma ale:"(n  m) = ((ant n) (ant m))"
apply (rule iffI)
apply (simp add:ant_def le_ant_def,
       cut_tac ant_z_in_Ainteg[of "n"],
       cut_tac ant_z_in_Ainteg[of "m"],
       simp add:Abs_Ainteg_inverse)+
done

lemma aless:"(n < m) = ((ant n) < (ant m))"
apply (simp add:less_ant_def,
       cut_tac ale[of "n" "m"], arith)
done

lemma ale_refl: "w  (w::ant)"
apply (cut_tac mem_ant[of "w"],
       erule disjE, simp,
       erule disjE, erule exE, simp,
       subst ale[THEN sym], simp+)
done

lemma aeq_ale:"(a::ant) = b  a  b"
by (simp add:ale_refl)

lemma ale_trans: " (i::ant)  j; j  k   i  k"
apply (cut_tac mem_ant[of "i"], cut_tac mem_ant[of "j"],
       cut_tac mem_ant[of "k"],
      (erule disjE)+, simp add:ale_refl, erule disjE, erule exE, simp+,
      (erule disjE)+, simp add:ale_refl, simp add:ale_refl)
apply ((erule disjE)+, erule exE, simp+,
  erule exE, simp,
       cut_tac x = "ant z" in minf_le_any,
       frule_tac x = "ant z" in ale_antisym[of _ "-"], assumption+,
       simp+,
       cut_tac minf_le_any[of ""], frule ale_antisym[of "-" ""],
       simp+)
apply (erule disjE, simp,
       (erule disjE)+, (erule exE)+, simp,
       cut_tac x = "ant za" in minf_le_any,
       frule_tac x = "ant za" in ale_antisym[of _ "-"], assumption+,
       simp, erule exE,
       cut_tac x = "ant z" in minf_le_any, simp)
apply (cut_tac minf_le_any[of ""],
       frule_tac ale_antisym[of "-" ""], assumption+,
       simp, erule disjE, erule exE, simp,
       cut_tac x = "ant z" in inf_ge_any,
       frule_tac x = "ant z" in ale_antisym[of _ ""], assumption+,
       simp)
apply (cut_tac minf_le_any[of ""], frule ale_antisym[of "-" ""],
       simp+,
       (erule disjE)+, (erule exE)+, simp add:ale[THEN sym],
       simp, (erule disjE)+, (erule exE)+,
       cut_tac x = "ant za" in inf_ge_any,
       frule_tac x = "ant za" in ale_antisym[of _ ""],
       simp+)
apply (erule disjE, erule exE,
       cut_tac inf_ge_any[of "j"],
       frule ale_antisym[of "j" ""], assumption+,
       cut_tac x = "ant z" in inf_ge_any, simp+)
done

(* Axiom 'order_aless_le_not_le' of class 'order': *)
lemma aless_le_not_le: "((w::ant) < z) = (w  z  ¬ z  w)"
by (auto simp add: less_ant_def)

instance ant :: order
proof qed
 (assumption |
  rule ale_refl ale_trans ale_antisym aless_le_not_le)+

(* Axiom 'linorder_linear' of class 'linorder': *)
lemma ale_linear: "(z::ant)  w  w  z"
apply (cut_tac mem_ant[of "z"], cut_tac mem_ant[of "w"],
       erule disjE, simp,
       erule disjE, simp)
apply ((erule disjE)+, (erule exE)+, simp add:ale[THEN sym],
       simp add:linorder_linear)
apply simp+
done

instance ant :: linorder
proof qed (rule ale_linear)

lemmas aless_linear = less_linear [where 'a = ant]


lemma ant_eq_0_conv [simp]: "(ant n = 0) = (n = 0)"
apply (simp add:Zero_ant_def)
done

lemma aless_zless: "(ant m < ant n) = (m<n)"
by (simp add: ale ant_def linorder_not_le [symmetric])

lemma a0_less_int_conv [simp]: "(0 < ant n) = (0 < n)"
apply (simp add:Zero_ant_def)
apply (simp add:aless[THEN sym])
done

lemma a0_less_1: "0 < (1::ant)"
apply (simp add:Zero_ant_def One_ant_def)
apply (subst aless_zless) apply simp
done

lemma a0_neq_1 [simp]: "0  (1::ant)"
by (simp only:Zero_ant_def One_ant_def, subst zneq_aneq[THEN sym], simp)

lemma ale_zle [simp]: "((ant i)  (ant j)) = (ij)"
by (subst ale[of "i" "j"], simp)

lemma ant_1 [simp]: "ant 1 = 1"
by (simp add: One_ant_def)

lemma zpos_apos:"(0  n) = (0  (ant n))"
apply (simp only:ale[of "0" "n"], simp only:ant_0[THEN sym])
done

lemma zposs_aposss:"(0 < n) = (0 < (ant n))"
apply (rule iffI)
 apply (unfold Zero_ant_def,
        subst aless[THEN sym, of "0" "n"], simp,
        subst aless[of "0" "n"], simp)
done

lemma an_nat_pos[simp]:"0  an n"
by (simp add:ant_0[THEN sym] an_def)

lemma amult_one_l:" 1 * (x::ant) = x"
by (cut_tac mem_ant[of "x"],