equal
deleted
inserted
replaced
45 by (cases y rule: option.exhaust) |
45 by (cases y rule: option.exhaust) |
46 (auto simp: Fin_def infinity_enat_def) |
46 (auto simp: Fin_def infinity_enat_def) |
47 qed |
47 qed |
48 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject) |
48 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject) |
49 |
49 |
50 declare [[coercion "Fin :: nat \<Rightarrow> enat"]] |
50 declare [[coercion_enabled]] |
|
51 declare [[coercion "Fin::nat\<Rightarrow>enat"]] |
51 |
52 |
52 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)" |
53 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)" |
53 by (cases x) auto |
54 by (cases x) auto |
54 |
55 |
55 lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)" |
56 lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)" |