src/HOL/ZF/HOLZF.thy
changeset 32989 c28279b29ff1
parent 32962 69916a850301
parent 32988 d1d4d7a08a66
child 33057 764547b68538
equal deleted inserted replaced
32987:eac0ff83005e 32989:c28279b29ff1
   624 lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n"
   624 lemma Nat2nat_nat2Nat[simp]: "Nat2nat (nat2Nat n) = n"
   625   by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat])
   625   by (simp add: Nat2nat_def inv_f_f[OF inj_nat2Nat])
   626 
   626 
   627 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   627 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
   628   apply (simp add: Nat2nat_def)
   628   apply (simp add: Nat2nat_def)
   629   apply (rule_tac f_inv_f)
   629   apply (rule_tac f_inv_onto_f)
   630   apply (auto simp add: image_def Nat_def Sep)
   630   apply (auto simp add: image_def Nat_def Sep)
   631   done
   631   done
   632 
   632 
   633 lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)"
   633 lemma Nat2nat_SucNat: "Elem N Nat \<Longrightarrow> Nat2nat (SucNat N) = Suc (Nat2nat N)"
   634   apply (auto simp add: Nat_def Sep Nat2nat_def)
   634   apply (auto simp add: Nat_def Sep Nat2nat_def)