equal
deleted
inserted
replaced
985 by (simp add: star_of_int_def) |
985 by (simp add: star_of_int_def) |
986 |
986 |
987 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" |
987 lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" |
988 by transfer (rule refl) |
988 by transfer (rule refl) |
989 |
989 |
990 instance star :: (semiring_char_0) semiring_char_0 proof |
990 instance star :: (semiring_char_0) semiring_char_0 |
|
991 proof |
991 have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp |
992 have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp |
992 then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp) |
993 then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp) |
993 then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def) |
994 then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def) |
994 qed |
995 qed |
995 |
996 |