equal
deleted
inserted
replaced
808 assumes "\<And>n. m = of_nat n \<Longrightarrow> P" |
808 assumes "\<And>n. m = of_nat n \<Longrightarrow> P" |
809 shows P |
809 shows P |
810 using assms by transfer blast |
810 using assms by transfer blast |
811 |
811 |
812 lemma [simp, code]: |
812 lemma [simp, code]: |
813 "natural_size = nat_of_natural" |
813 "size_natural = nat_of_natural" |
814 proof (rule ext) |
814 proof (rule ext) |
815 fix n |
815 fix n |
816 show "natural_size n = nat_of_natural n" |
816 show "size_natural n = nat_of_natural n" |
817 by (induct n) simp_all |
817 by (induct n) simp_all |
818 qed |
818 qed |
819 |
819 |
820 lemma [simp, code]: |
820 lemma [simp, code]: |
821 "size = nat_of_natural" |
821 "size = nat_of_natural" |