# HG changeset patch
# User wenzelm
# Date 1724594459 -7200
# Node ID 72beac575e9c1ab61ea49ad328e92cef5a84f16c
# Parent  1d8ce19d7d71789a6c335e52fcc3fc6dd4edb3bb
use nicer notation, following 783406dd051e;

diff -r 1d8ce19d7d71 -r 72beac575e9c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Aug 25 15:53:03 2024 +0200
+++ b/src/HOL/GCD.thy	Sun Aug 25 16:00:59 2024 +0200
@@ -2851,18 +2851,23 @@
 definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat" 
   where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
 
+syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
+syntax_consts "_type_char" \<rightleftharpoons> semiring_char
+translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
+print_translation \<open>
+  let
+    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>
+
 context semiring_1
 begin
 
-context
-  fixes CHAR :: nat
-  defines "CHAR \<equiv> semiring_char TYPE('a)"
-begin
-
-lemma of_nat_CHAR [simp]: "of_nat CHAR = (0 :: 'a)"
+lemma of_nat_CHAR [simp]: "of_nat CHAR('a) = (0 :: 'a)"
 proof -
-  have "CHAR \<in> {n. of_nat n = (0::'a)}"
-    unfolding CHAR_def semiring_char_def
+  have "CHAR('a) \<in> {n. of_nat n = (0::'a)}"
+    unfolding semiring_char_def
   proof (rule Gcd_in, clarify)
     fix a b :: nat
     assume *: "of_nat a = (0 :: 'a)" "of_nat b = (0 :: 'a)"
@@ -2886,14 +2891,14 @@
     by simp
 qed
 
-lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \<longleftrightarrow> CHAR dvd n"
+lemma of_nat_eq_0_iff_char_dvd: "of_nat n = (0 :: 'a) \<longleftrightarrow> CHAR('a) dvd n"
 proof
   assume "of_nat n = (0 :: 'a)"
-  thus "CHAR dvd n"
-    unfolding CHAR_def semiring_char_def by (intro Gcd_dvd) auto
+  thus "CHAR('a) dvd n"
+    unfolding semiring_char_def by (intro Gcd_dvd) auto
 next
-  assume "CHAR dvd n"
-  then obtain m where "n = CHAR * m"
+  assume "CHAR('a) dvd n"
+  then obtain m where "n = CHAR('a) * m"
     by auto
   thus "of_nat n = (0 :: 'a)"
     by simp
@@ -2902,53 +2907,36 @@
 lemma CHAR_eqI:
   assumes "of_nat c = (0 :: 'a)"
   assumes "\<And>x. of_nat x = (0 :: 'a) \<Longrightarrow> c dvd x"
-  shows   "CHAR = c"
+  shows   "CHAR('a) = c"
   using assms by (intro dvd_antisym) (auto simp: of_nat_eq_0_iff_char_dvd)
 
-lemma CHAR_eq0_iff: "CHAR = 0 \<longleftrightarrow> (\<forall>n>0. of_nat n \<noteq> (0::'a))"
+lemma CHAR_eq0_iff: "CHAR('a) = 0 \<longleftrightarrow> (\<forall>n>0. of_nat n \<noteq> (0::'a))"
   by (auto simp: of_nat_eq_0_iff_char_dvd)
 
-lemma CHAR_pos_iff: "CHAR > 0 \<longleftrightarrow> (\<exists>n>0. of_nat n = (0::'a))"
+lemma CHAR_pos_iff: "CHAR('a) > 0 \<longleftrightarrow> (\<exists>n>0. of_nat n = (0::'a))"
   using CHAR_eq0_iff neq0_conv by blast
 
 lemma CHAR_eq_posI:
   assumes "c > 0" "of_nat c = (0 :: 'a)" "\<And>x. x > 0 \<Longrightarrow> x < c \<Longrightarrow> of_nat x \<noteq> (0 :: 'a)"
-  shows   "CHAR = c"
+  shows   "CHAR('a) = c"
 proof (rule antisym)
-  from assms have "CHAR > 0"
+  from assms have "CHAR('a) > 0"
     by (auto simp: CHAR_pos_iff)
-  from assms(3)[OF this] show "CHAR \<ge> c"
+  from assms(3)[OF this] show "CHAR('a) \<ge> c"
     by force
 next
-  have "CHAR dvd c"
+  have "CHAR('a) dvd c"
     using assms by (auto simp: of_nat_eq_0_iff_char_dvd)
-  thus "CHAR \<le> c"
+  thus "CHAR('a) \<le> c"
     using \<open>c > 0\<close> by (intro dvd_imp_le) auto
 qed
 
 end
-end
 
 lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0"
   by (simp add: CHAR_eq0_iff)
 
 
-(* nicer notation *)
-
-syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
-
-syntax_consts "_type_char" == semiring_char
-
-translations "CHAR('t)" => "CONST semiring_char (CONST Pure.type :: 't itself)"
-
-print_translation \<open>
-  let
-    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)