Theory Nat_Miscellanea

theory Nat_Miscellanea imports ZF begin

section‹Auxiliary results›

lemmas nat_succI =  Ord_succ_mem_iff [THEN iffD2,OF nat_into_Ord]

lemma nat_succD : "m ∈ nat ⟹  succ(n) ∈ succ(m) ⟹ n ∈ m"
  by (drule_tac j="succ(m)" in ltI,auto elim:ltD)
    
lemmas zero_in =  ltD [OF nat_0_le]

lemma in_n_in_nat :  "m ∈ nat ⟹ n ∈ m ⟹ n ∈ nat"
  by(drule ltI[of "n"],auto simp add: lt_nat_in_nat)
    
lemma in_succ_in_nat : "m ∈ nat ⟹ n ∈ succ(m) ⟹ n ∈ nat"
  by(auto simp add:in_n_in_nat)
  
lemma ltI_neg : "x ∈ nat ⟹ j ≤ x ⟹ j ≠ x ⟹ j < x"
  by (simp add: le_iff)
    
lemma succ_pred_eq  :  "m ∈ nat ⟹ m ≠ 0  ⟹ succ(pred(m)) = m"
 by (auto elim: natE)
    
lemma succ_ltI : "n ∈ nat ⟹ succ(j) < n ⟹ j < n"
  apply (rule_tac j="succ(j)" in lt_trans,rule le_refl,rule Ord_succD)
  apply (rule nat_into_Ord,erule in_n_in_nat,erule ltD,simp)
done
      
lemma succ_In : "n ∈ nat ⟹ succ(j) ∈ n ⟹ j ∈ n"
 by (rule succ_ltI[THEN ltD], auto intro: ltI)
    
lemmas succ_leD = succ_leE[OF leI]
    
lemma succpred_leI : "n ∈ nat ⟹  n ≤ succ(pred(n))"
  by (auto elim: natE)

lemma succpred_n0 : "p ∈ nat ⟹  succ(n) ∈ p ⟹ p≠0"
  by (auto elim: natE)


lemma funcI : "f ∈ A → B ⟹ a ∈ A ⟹ b= f ` a ⟹ ⟨a, b⟩ ∈ f"
  by(simp_all add: apply_Pair)

lemmas natEin = natE [OF lt_nat_in_nat]

lemma succ_in : "succ(x) ≤ y  ⟹ x ∈ y"
 by (auto dest:ltD) 
  
lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

lemma pred_le2 : "n∈ nat ⟹ m ∈ nat ⟹ pred(n) ≤ m ⟹ n ≤ succ(m)"
  by(subgoal_tac "n∈nat",rule_tac n="n" in natE,auto)
    
lemma pred_le : "n∈ nat ⟹ m ∈ nat ⟹ n ≤ succ(m) ⟹ pred(n) ≤ m"
  by(subgoal_tac "pred(n)∈nat",rule_tac n="n" in natE,auto)
    
lemma un_leD1 : "i ∈ nat ⟹ j∈ nat ⟹ k ∈ nat ⟹  i ∪ j ≤ k ⟹ i ≤ k"   
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)
  
lemma un_leD2 : "i ∈ nat ⟹ j∈ nat ⟹ k ∈ nat ⟹  i ∪ j ≤k ⟹ j ≤ k"   
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma gt1 : "n ∈ nat ⟹ i ∈ n ⟹ i ≠ 0 ⟹ i ≠ 1 ⟹ 1<i"
  by(rule_tac n="i" in natE,erule in_n_in_nat,auto intro: Ord_0_lt)

lemma pred_mono : "m ∈ nat ⟹ n ≤ m ⟹ pred(n) ≤ pred(m)"
  by(rule_tac n="n" in natE,auto simp add:le_in_nat,erule_tac n="m" in natE,auto)
    
lemma pred2_Un: 
  assumes "j ∈ nat" "m ≤ j" "n ≤ j" 
  shows "pred(pred(m ∪ n)) ≤ pred(pred(j))" 
  using assms pred_mono[of "j"] le_in_nat Un_least_lt pred_mono by simp

lemma nat_union_abs1 : 
  "⟦ Ord(i) ; Ord(j) ; i ≤ j ⟧ ⟹ i ∪ j = j"
  by (rule Un_absorb1,erule le_imp_subset)

lemma nat_union_abs2 : 
  "⟦ Ord(i) ; Ord(j) ; i ≤ j ⟧ ⟹ j ∪ i = j"
  by (rule Un_absorb2,erule le_imp_subset)
    
lemma nat_un_max : "i ∈ nat ⟹ j ∈ nat ⟹ i ∪ j = max(i,j)"
  apply(auto simp add:max_def nat_union_abs1)
  apply(auto simp add:  not_lt_iff_le leI nat_union_abs2)
done

lemma nat_un_ty : "i∈nat ⟹j∈nat ⟹ i∪j ∈ nat"
  by simp  

lemma nat_max_ty : "i∈nat ⟹j∈nat ⟹ max(i,j) ∈ nat"
  unfolding max_def by simp

lemmas nat_simp_union = nat_un_max nat_un_ty nat_max_ty max_def

end