# 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:"⟦∀y∈A. P x y ⟶ ¬ Q y; ∀y∈A. Q y ∨ R y⟧ ⟹
∀y∈A. (¬ P x y) ∨ R y"
by blast

lemma forball_contra1:"⟦∀y∈A. P x y ⟶ Q y; ∀y∈A. ¬ Q y⟧ ⟹ ∀y∈A. ¬ 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 (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"
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+)
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+,
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+)
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+,
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)
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+)
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 (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+)
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'"
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 ⟹ ∃y∈A. y = x"
by simp

lemma inEx_rev:" ∃y∈A. 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 ⟹ ∀b∈A. 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:"{x∈A. P x} ⊆ A"
by blast

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

lemma sets_not_eq:"⟦A ≠ B; B ⊆ A⟧ ⟹ ∃a∈A. 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 ⟹ ∃y∈A. 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:"∃X∈C. A ⊆ X ⟹ A ⊆ ⋃ C"
by blast

lemma family_subset_Un_sub:"∀A∈C. 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. a∈A ∧ 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 = (λx∈A. x)"

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

definition
invfun :: "['a set, 'b set, 'a ⇒ 'b] ⇒ ('b ⇒ 'a)" where
"invfun A B (f :: 'a ⇒ 'b) = (λy∈B.(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"

lemma cmp_fun_image:"⟦f ∈ A → B; g ∈ B → C ⟧ ⟹
(cmp g f)  A =  g  (f  A)"
apply (rule equalityI)
apply (erule bexE, simp add:cmp_def, blast)
apply (rule subsetI, simp add:image_def[of g])
apply (erule bexE, simp)
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 (erule bexE, simp add:cmp_def, blast)
apply (rule subsetI, simp add:image_def[of g])
apply (erule bexE, simp)
apply blast
done

lemma restrict_fun_eq:"∀x∈A. f x = g x ⟹ (λx∈A. f x) = (λx∈A. g x)"
done

lemma funcset_mem: "⟦f ∈ A → B; x ∈ A⟧ ⟹ f x ∈ B"
done

lemma img_subset:"f ∈ A → B ⟹ f  A ⊆ B"
apply (rule subsetI)
apply (simp add:image_def, erule bexE, simp)
done

lemma funcset_mem1:"⟦∀l∈A. f l ∈ B; x ∈ A⟧ ⟹ f x ∈ B"
apply simp
done

lemma func_to_img:"f ∈ A → B ⟹ f ∈ A → f  A"

lemma funcset_eq:"⟦ f ∈ extensional A; g ∈ extensional A; ∀x∈A. f x = g x ⟧ ⟹  f = g"
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 (rule ballI) apply simp
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 "∀x∈A1. x ∈ A")
apply (rule ballI) apply (simp add:subsetD)
done

lemma mem_in_image:"⟦ f ∈ A → B; a ∈ A⟧ ⟹ f a ∈ f  A "
apply blast
done

lemma mem_in_image1:"⟦ ∀l∈A. 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"

lemma elem_in_image2: "⟦ f ∈ A → B; A1 ⊆ A; x ∈ A1⟧ ⟹ f x ∈ f A1"
apply blast
done

lemma funcs_nonempty:"⟦ A ≠ {}; B ≠ {} ⟧ ⟹ (A → B) ≠ {}"
apply (subgoal_tac "constmap A B ∈ A → B") apply (simp add:nonempty)
apply (rule allI) apply (rule impI)
apply (frule nonempty_ex[of "B"])
apply (rule someI2_ex) apply assumption+
done

lemma idmap_funcs: "idmap A ∈ A → A"
done

lemma l_idmap_comp: "⟦f ∈ extensional A; f ∈ A → B⟧ ⟹
compose A (idmap B) f = f"
apply (rule funcset_eq[of _ "A"])
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 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 (rule allI) apply (rule impI)
done

lemma restrict_fun: "⟦ f ∈ A → B; A1 ⊆ A ⟧ ⟹ restrict f A1 ∈ A1 → B"
apply (rule allI) apply (rule impI)
done

lemma set_of_hom: "∀x ∈ A. f x ∈ B ⟹ restrict f A ∈ A → B"
done

lemma composition : "⟦ f ∈ A →  B; g ∈ B → C⟧ ⟹ (compose A g f) ∈ A →  C"
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 (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"
done

lemma restrict_inj:"⟦inj_on f A; A1 ⊆ A⟧ ⟹ inj_on f A1"
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+)
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 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 (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+)
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"
done

lemma bivar_fun: "⟦ f ∈ A → (B → C); a ∈ A ⟧ ⟹ f a ∈ B → C"

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:"⟦∀a∈A. ∀b∈B. f a b = g a b ⟧ ⟹
(λx∈A. λy∈B. f x y) =  (λx∈A. λy∈B. g x y)"
apply (subgoal_tac "∀x∈A. (λy∈B. f x y) = (λy∈B. g x y)")
apply (rule funcset_eq [of _ "A"])
apply (rule ballI)
apply simp
apply (rule ballI)
apply (rule funcset_eq [of _ "B"])
apply (rule ballI) apply simp
done

lemma set_image: "⟦ f ∈ A → B; A1 ⊆ A; A2 ⊆ A ⟧ ⟹
f(A1 ∩ A2) ⊆ (f A1) ∩ (f A2)"
apply auto
done

lemma image_sub: "⟦f ∈ A → B; A1 ⊆ A ⟧ ⟹ (fA1) ⊆ B"

lemma image_sub0: "f ∈ A → B ⟹ (fA) ⊆ 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"],

lemma im_set_mono: "⟦f ∈A → B; A1 ⊆ A2; A2 ⊆ A ⟧ ⟹ (f  A1) ⊆ (f  A2)"
apply auto
done

lemma im_set_un:"⟦ f∈A → B; A1 ⊆ A; A2 ⊆ A ⟧ ⟹
f(A1 ∪ A2) = (fA1) ∪ (fA2)"
apply auto
done

lemma im_set_un1:"⟦∀l∈A. 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. x∈A ∧ f x ∈ B}"

lemma invim: "⟦ f:A → B; B1 ⊆ B ⟧ ⟹ invim f A B1 ⊆ A"

lemma setim_cmpfn: "⟦ f:A → B; g:B → C; A1 ⊆ A ⟧ ⟹
(compose A g f) A1 = g(f A1)"
apply auto
done

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

lemma surj_to_test:"⟦ f ∈ A → B; ∀b∈B. ∃a∈A. f a = b ⟧ ⟹
surj_to f A B"

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 ⟧ ⟹ ∀b∈B. ∃a∈A. f a = b"
apply auto
done

lemma surj_to_el1:"⟦ f ∈ A → B; surj_to f A B; b∈B⟧ ⟹ ∃a∈A. f a = b"
done

lemma surj_to_el2:"⟦surj_to f A B; b ∈ B⟧ ⟹ ∃a∈A. f a = b"
apply (frule sym, thin_tac "{y. ∃x∈A. 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 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 ballI, simp add:surj_to_def [of "g"], frule sym,
thin_tac "g  B = C", simp, simp add:image_def,
apply auto
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"
done

lemma inj_onTr1:"⟦inj_on f A; x ∈ A; y ∈ A; f x = f y⟧  ⟹ x = y"
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+)
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 (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: "⟦∀l∈A. f l ∈ B; inj_on f A; ∀k∈B. 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 (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:surj_to_def image_def) apply (frule sym)
apply (thin_tac "{y. ∃x∈A. y = f x} = B") apply simp
apply (thin_tac "B = {y. ∃x∈A. 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 (rule allI) apply (rule impI)
apply (rule invfun_mem) apply (rule funcsetI)
apply simp+
done

lemma invfun_r:"⟦ f∈A → B; inj_on f A; surj_to f A B; b ∈ B ⟧
⟹ f ((invfun A B f) b) = b"
apply (rule someI2_ex)
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 (rule someI2_ex) apply auto
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 (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 (rule conjI)

done

lemma bij_invfun:"⟦f ∈ A → B; bij_to f A B⟧ ⟹
bij_to (invfun A B f) B A"
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 (rule impI)
done

lemma invfun_mem1:"⟦f ∈ A → B; bij_to f A B; b ∈ B⟧ ⟹
(invfun A B f) b ∈ A"
done

lemma invfun_r1:"⟦ f∈A → B; bij_to f A B; b ∈ B ⟧
⟹ f ((invfun A B f) b) = b"
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 (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 (rule ballI)
apply (frule sym, thin_tac "compose B g (invfun A B f) = h", simp)
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 (rule ballI)
apply (frule sym, thin_tac "compose C (invfun A B f) g = h",
apply (frule_tac x = x in funcset_mem[of g C B], assumption)
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)
erule conjE, erule bexE, simp,
frule_tac c = xb in subsetD[of "C" "B"], assumption+)

apply (frule_tac c = x in subsetD[of "C" "B"], assumption+,
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:comp_inj[of "f" "A" "B" "g" "C"])
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}"
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)"

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)
done

lemma Nset_nset_1:"⟦0 < n; i < n⟧ ⟹ {j. j ≤ n} = {j. j ≤ i} ∪
nset (Suc i) n"
apply auto
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}"

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. m∈A ∧ (∀x∈A. x ≤ m))⟧ ⟹
(nasc_seq A a n) ∈ A"
apply (induct n)
apply (subgoal_tac "∃x∈A. (nasc_seq A a n) < x") prefer 2 apply blast
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. m < x)",
rule someI2_ex, blast, simp)
done

lemma nasc_seqn:"⟦(a::nat) ∈ A; ¬ (∃m. m∈A ∧ (∀x∈A. x ≤ m))⟧ ⟹
(nasc_seq A a n) < (nasc_seq A a (Suc n))"
apply (simp,
frule nasc_seq_mem [of "a" "A" "n"], simp)
subgoal_tac "∃x∈A. (nasc_seq A a n) < x") prefer 2 apply simp
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. m < x)",
rule someI2_ex, blast, simp)
done

lemma nasc_seqn1:"⟦(a::nat) ∈ A; ¬ (∃m. m∈A ∧ (∀x∈A. 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. m∈A ∧ (∀x∈A. 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. m∈A ∧ (∀x∈A. 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 "∀x∈A. x ≤ m",
frule_tac x = m in bspec, assumption+,
thin_tac "∀x∈A. 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 ∧ (∀x∈A. x ≤ m))"

lemma n_max:"⟦A ⊆ {i. i ≤ (n::nat)}; A ≠ {}⟧ ⟹
(n_max A) ∈ A ∧ (∀x∈A. x ≤ (n_max A))"
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)+
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"
done

lemma skip_im_Tr0_1:"0 < y ⟹ skip 0 (y - Suc 0) = y"
done

lemma skip_im_Tr1:"⟦ i ∈ {i. i ≤ (Suc n)}; 0 < i; x ≤ i - Suc 0 ⟧ ⟹
skip i x = x"

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])
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"

lemma skip_im_Tr2_1:"⟦i ∈ {i. i ≤ (Suc n)}; i ≤ x⟧ ⟹
skip i x = Suc x"
apply (case_tac "i = 0")
apply (simp, rule skip_im_Tr2, assumption+, simp+)
done

lemma skip_im_Tr3:"x ∈ {i. i ≤ n} ⟹ skip (Suc n) x = x"
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 (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],
apply (cut_tac x = i and n = x in less_le_diff, assumption,
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,

lemma skip_id:"l < i ⟹ skip i l = l"
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"
done

lemma skip_inj:"⟦i ∈ {k. k ≤ n}; j ∈ {k. k ≤ n}; i ≠ j⟧ ⟹
skip k i ≠ skip k j"
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)"

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",
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",
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,
done

lemma slide_hom:"i ≤ j ⟹ (slide i) ∈ {l. l ≤ (j - i)} → nset i j"
apply (rule allI) apply (rule impI)
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 (rule equalityI)
apply (rule subsetI)
apply simp
apply auto
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"

lemma im_jointfunTr1:"(jointfun n f m g)  {i. i ≤ n} = f  {i. i ≤ n}"
apply auto

done

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

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 "∀i∈nset (Suc n) (Suc (n+m)). ¬ (i ≤ n) ")
apply simp
apply (thin_tac "∀i∈nset (Suc n) (Suc (n + m)). ¬ i ≤ n")
apply (subgoal_tac "g xa = g (sliden (Suc n) (slide (Suc n) xa))")
apply blast
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)
case_tac "l ≤ n", simp add:Pi_def,
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,
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)
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"])
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)}"

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))"

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 (auto )
done

lemma func_pre:"f ∈ {j. j ≤ (Suc n)} → A ⟹ f ∈ {j. j ≤ n} → A"

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"])
done

definition
Nleast :: "nat set ⇒ nat" where
"Nleast A = (THE a. (a ∈ A ∧ (∀x∈A. a ≤ x)))"

definition
Nlb :: "[nat set, nat] ⇒ bool" where
"Nlb A n ⟷ (∀a∈A. 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. m∈A ∧ (∀x∈A. m ≤ x))⟧ ⟹
(ndec_seq A a n) ∈ A"
apply (induct_tac n)
apply simp apply simp
apply (subgoal_tac "∃x∈A. x < (ndec_seq A a n)") prefer 2 apply blast
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. x < m)")
apply (rule someI2_ex) apply blast
apply simp
done

lemma ndec_seqn:"⟦a ∈ (A::nat set);¬ (∃m. m∈A ∧ (∀x∈A. 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 (subgoal_tac "∃x∈A. x < (ndec_seq A a n)") prefer 2 apply simp
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. x < m)")
apply (rule someI2_ex) apply blast
apply simp
done

lemma ndec_seqn1:"⟦a ∈ (A::nat set); ¬ (∃m. m∈A ∧ (∀x∈A. 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 ∧ (∀x∈A. m ≤ x))")
apply (simp del:ndec_seq_Suc)
done

lemma ex_NleastTr:"⟦a ∈ (A::nat set); ¬ (∃m. m∈A ∧ (∀x∈A. 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. m∈A ∧ (∀x∈A. 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 "∀x∈A. 0 ≤ a", blast,
rule ballI, simp)
apply ((erule conjE)+,
subgoal_tac "m ≤ 0", thin_tac "∀x∈A. m ≤ x",
subgoal_tac "y ≤ 0", thin_tac "∀x∈A. y ≤ x",
simp, blast, blast)
apply (rule ex_ex1I)
prefer 2 apply (erule conjE)+
apply (subgoal_tac "m ≤ y", thin_tac "∀x∈A. m ≤ x",
subgoal_tac "y ≤ m", thin_tac "∀x∈A. 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 ∧ (∀x∈A. 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 ∧ (∀x∈A. (Nleast A) ≤ x)"
apply (frule ex_Nleast [of "A"])
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 (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 ∧ (∀x∈A. a ≤ x)))"

definition
LB :: "[int set, int] ⇒ bool" where
"LB A n = (∀a∈A. 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
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. m∈A ∧ (∀x∈A. m ≤ x))⟧ ⟹
(dec_seq A a n) ∈ A"
apply (induct_tac n)
apply simp apply simp  apply (simp add:not_zle)
apply (subgoal_tac "∃x∈A. x < (dec_seq A a n)") prefer 2 apply blast
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. x < m)")
apply (rule someI2_ex) apply blast
apply simp
done

lemma dec_seqn:"⟦a ∈ A; A ⊆ Zset;¬ (∃m. m∈A ∧ (∀x∈A. 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 (subgoal_tac "∃x∈A. x < (dec_seq A a n)") prefer 2 apply simp
apply (thin_tac "∀m. m ∈ A ⟶ (∃x∈A. x < m)")
apply (rule someI2_ex) apply blast
apply simp
done

lemma dec_seqn1:"⟦a ∈ A; A ⊆ Zset;¬ (∃m. m∈A ∧ (∀x∈A. 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. m∈A ∧ (∀x∈A. 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 ∧ (∀x∈A. 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"
done

lemma lbs_ex_Zleast:"⟦A ≠ {}; A ⊆ Zset; LB A n⟧ ⟹ ∃!m. m∈A ∧ (∀x∈A. 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 "∀x∈A. m ≤ x") apply (thin_tac "∀x∈A. 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 ∧ (∀x∈A. 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 (subgoal_tac "n ≤ dec_seq A a (nat (¦a¦ + ¦n¦ + 1))")
apply (thin_tac "∀a∈A. n ≤ a") apply (simp add:not_zle)
apply blast
done

lemma Zleast:"⟦A ≠ {}; A ⊆ Zset; LB A n⟧ ⟹ Zleast A ∈ A ∧
(∀x∈A. (Zleast A) ≤ x)"
apply (frule lbs_ex_Zleast [of "A" "n"], assumption+)
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
"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"
done

lemma ant_inf_in_Ainteg:"((0::int), 1) ∈ Ainteg"
done

lemma ant_minf_in_Ainteg:"((0::int), -1) ∈ Ainteg"
done

lemma ant_0_in_Ainteg:"((0::int), 0) ∈ Ainteg"
done

lemma an_0[simp]:"an 0 = 0"

lemma an_1[simp]:"an 1 = 1"

lemma mem_ant:"(a::ant) = -∞ ∨ (∃(z::int). a = ant z) ∨ a = ∞"
apply (case_tac "a = -∞ ∨ a = ∞")
apply blast
cut_tac Rep_Ainteg[of "a"],
cut_tac ant_inf_in_Ainteg,
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)",
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)",
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)",
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)",
done

lemma minf:"-∞ = Abs_Ainteg((0,-1))"
cut_tac ant_inf_in_Ainteg,
done

lemma z_neq_inf[simp]:"(ant z) ≠ ∞ "
apply (rule contrapos_pp, simp+)
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,
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 (cut_tac ant_inf_in_Ainteg,
apply (subgoal_tac "- Abs_Ainteg (z, 0) = - 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,
cut_tac ant_minf_in_Ainteg,
apply simp
done

lemma minf_neq_inf[simp]:"-∞ ≠ ∞"
apply (cut_tac ant_inf_in_Ainteg,
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,
apply simp
done

lemma a_ipi[simp]:"∞ + ∞ = ∞"
cut_tac ant_inf_in_Ainteg,
done

lemma a_zpi[simp]:"(ant z) + ∞  = ∞"
cut_tac ant_z_in_Ainteg[of "z"],
cut_tac ant_inf_in_Ainteg,
done

lemma a_ipz[simp]:" ∞ + (ant z) = ∞"
cut_tac ant_z_in_Ainteg[of "z"],
cut_tac ant_inf_in_Ainteg,
done

lemma a_zpz:"(ant m) + (ant n) = ant (m + n)"
cut_tac ant_z_in_Ainteg[of "m"],
cut_tac ant_z_in_Ainteg[of "n"],
done

lemma a_mpi[simp]:"-∞ + ∞  = 0"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
done

lemma a_ipm[simp]:"∞ + (-∞) = 0"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
done

lemma a_mpm[simp]:"-∞ + (-∞) = -∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
done

lemma a_mpz[simp]:"-∞ + (ant m) = -∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_zpm[simp]:"(ant m) + (-∞) = -∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_mdi[simp]:"-∞ - ∞  = - ∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
done

lemma a_zdz:"(ant m) - (ant n) = ant (m - n)"
cut_tac ant_z_in_Ainteg[of "n"],
cut_tac ant_z_in_Ainteg[of "m"],
cut_tac ant_z_in_Ainteg[of "-n"],
done

lemma a_i_i[simp]:"∞ * ∞ = ∞"
cut_tac ant_inf_in_Ainteg,
done

lemma a_0_i[simp]:"0 * ∞ = 0"
cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,

lemma a_i_0[simp]:"∞ * 0 = 0"
cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,

lemma a_0_m[simp]:"0 * (-∞) = 0"
cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,

lemma a_m_0[simp]:"(-∞) * 0 = 0"
cut_tac ant_inf_in_Ainteg, cut_tac ant_0_in_Ainteg,

lemma a_m_i[simp]:"(-∞) * ∞ = -∞"
cut_tac ant_inf_in_Ainteg, cut_tac ant_minf_in_Ainteg,

lemma a_i_m[simp]:"∞ * (-∞) = - ∞"
cut_tac ant_inf_in_Ainteg, cut_tac ant_minf_in_Ainteg,

lemma a_pos_i[simp]:"0 < m ⟹ (ant m) * ∞ = ∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_i_pos[simp]:"0 < m ⟹ ∞ * (ant m) = ∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_neg_i[simp]:"m < 0 ⟹ (ant m) * ∞ = -∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_i_neg[simp]:"m < 0 ⟹ ∞ * (ant m) = -∞"
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma a_z_z:"(ant m) * (ant n) = ant (m*n)"
cut_tac ant_z_in_Ainteg[of "m"],
cut_tac ant_z_in_Ainteg[of "n"],
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"],
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"],
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"],
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"],
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,
done

lemma inj_on_Abs_Ainteg:"inj_on Abs_Ainteg Ainteg"
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",
done

lemma an_Suc:"an (Suc n) = an n + 1"
apply (subst an_1[THEN sym])
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"],
apply simp+
done

lemma aminus:"- ant m = ant (-m)"
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma aminusZero:"- ant 0 = ant 0"
done

lemma  ant_0: "ant 0 = (0::ant)"

lemma inf_neq_0[simp]:"∞ ≠ 0"
apply (cut_tac z_neq_inf[of "0"], frule not_sym)
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)
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"

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

lemma aminus_0: "- (- 0) = (0::ant)"
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, erule exE, simp add:a_z_z,
cut_tac less_linear[of "z" "0"], simp,
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, erule exE, simp,
apply ((erule disjE)+, erule exE,
apply ((erule disjE)+, (erule exE)+, simp add:a_zpz 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⇩∞"
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⇩-⇩∞"

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⇩-⇩∞"
done

lemma Zero_in_aug_minf:"0 ∈ Z⇩-⇩∞"

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"],
(erule disjE)+, (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)
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"],
done

lemma aadd_minus_r: "x + (- x) = (0::ant)"
done

lemma ant_minus_inj:"ant z ≠ ant w ⟹ - ant z ≠ - ant w"

lemma aminus_mult_minus: "(- (ant z)) * (ant w) = - ((ant z) * (ant w))"
cut_tac ant_z_in_Ainteg[of "z"],
cut_tac ant_z_in_Ainteg[of "-z"],
cut_tac ant_z_in_Ainteg[of "w"],
cut_tac ant_z_in_Ainteg[of "z * w"])
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)
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,
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
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,
cut_tac ant_inf_in_Ainteg,
cut_tac z = z in ant_z_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
simp)
cut_tac ant_inf_in_Ainteg,
cut_tac z = z in ant_z_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
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,
cut_tac ant_inf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "0"],
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,
cut_tac ant_inf_in_Ainteg,
cut_tac ant_z_in_Ainteg[of "0"],
simp+)
done

lemma z_le_i[simp]:"(ant x) ≤ ∞ "
cut_tac ant_z_in_Ainteg[of "0"],
cut_tac ant_z_in_Ainteg[of "x"],
cut_tac ant_inf_in_Ainteg,
done

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

lemma m_le_z:"-∞ ≤ (ant x) "
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,
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 ≠ - ∞",
done

lemma noninf_mem_Z:"⟦x ∈ Z⇩∞; x ≠ ∞⟧ ⟹ ∃(z::int). x = ant z"
apply (cut_tac mem_ant[of "x"], simp)
done

lemma z_mem_Z:"ant z ∈ Z⇩∞"

lemma inf_ge_any[simp]:"x ≤ ∞"
apply (cut_tac mem_ant[of "x"], erule disjE)
cut_tac ant_minf_in_Ainteg,
cut_tac ant_inf_in_Ainteg,
apply (erule disjE, erule exE, simp)
cut_tac ant_inf_in_Ainteg,
done

lemma zero_lt_inf:"0 < ∞"

lemma minf_le_any[simp]:"-∞ ≤ x"
apply (cut_tac mem_ant[of "x"], erule disjE)
cut_tac ant_minf_in_Ainteg,
cut_tac ant_inf_in_Ainteg,
apply (erule disjE, erule exE, simp)
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
apply simp
done

lemma minf_less_0:"-∞ < 0"

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,
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 "x ≤ y",
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
apply (erule disjE, erule disjE, erule exE,
thin_tac "y ≤ x",
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",
cut_tac ant_inf_in_Ainteg,
cut_tac ant_minf_in_Ainteg,
apply ((erule disjE)+, (erule exE)+,
cut_tac z = z in ant_z_in_Ainteg,
cut_tac z = za in ant_z_in_Ainteg,
apply (erule exE,
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",
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"],
(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)
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"],
(erule disjE)+, simp, erule exE, simp,
erule disjE, erule exE, simp,
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"],
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],
(erule disjE)+, (erule exE)+, cut_tac less_linear[of "z" "0"], simp,
cut_tac less_linear[of "z" "0"],
(erule disjE)+, (erule exE)+, simp add:a_zpz a_z_z,
cut_tac less_linear[of "z" "0"], erule disjE, simp,
apply (erule disjE, erule exE, simp,
cut_tac less_linear[of "z" "0"], erule disjE, simp add:a_z_z,
cut_tac less_linear[of "z" "0"], erule disjE, simp,
done

lemma amult_0_r:"(ant z) * 0 = 0"

lemma amult_0_l:"0 * (ant z) = 0"

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 ∞ = ∞"
done

lemma asprod_neg_inf[simp]:"m < 0 ⟹ m *⇩a ∞ = -∞"
done

lemma asprod_pos_minf[simp]:"0 < m ⟹ m *⇩a (-∞) = (-∞)"
done

lemma asprod_neg_minf[simp]:"m < 0 ⟹ m *⇩a (-∞) = ∞"
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"],
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)"
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,
simp, (erule disjE)+, erule exE, simp add:asprod_mult,
apply (erule disjE, erule exE, simp add:asprod_mult,
erule disjE, erule disjE, erule disjE, erule exE,
erule disjE, erule exE, simp add:asprod_mult,
apply (simp, erule disjE, erule exE, simp,
(erule disjE)+, erule exE, simp add:asprod_mult,
apply (erule disjE, erule exE, simp add:a_zpz 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"
cut_tac mem_ant[of "x"], simp, erule exE,
done

lemma asprod_n_0:"n *⇩a 0 = 0"
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,

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+,
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,
apply (erule disjE, erule exE, simp add:asprod_mult,
apply ((erule disjE)+, simp,
erule disjE, erule exE, rule contrapos_pp, simp+,
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 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⇩∞"

lemma tna_ant:" tna (ant z) = z"
apply (cut_tac z_neq_minf[of "z"], cut_tac z_neq_inf[of "z"],
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 (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)",
apply (cut_tac mem_ant[of "b"], simp add:aug_inf_def,
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)
cut_tac ant_z_in_Ainteg[of "n"],
cut_tac ant_z_in_Ainteg[of "m"],
done

lemma aless:"(n < m) = ((ant n) < (ant m))"
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"

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+,
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)"

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],
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)"
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)"
done

lemma a0_less_1: "0 < (1::ant)"
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)) = (i≤j)"
by (subst ale[of "i" "j"], simp)

lemma ant_1 [simp]: "ant 1 = 1"

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 (cut_tac mem_ant[of "x"], `