src/HOL/GCD.thy

     fun char_type_tr' ctxt [Const (\<^const_syntax>\<open>Pure.type\<close>, Type (_, [T]))] =
       Syntax.const \<^syntax_const>\<open>_type_char\<close> $ Syntax_Phases.term_of_typ ctxt T
   in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
 \<close>
 
+
+lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \<noteq> Suc 0"
+  by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one)
+
+lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \<noteq> Suc 0"
+  using local.of_nat_CHAR by fastforce
+
 end