src/HOL/Library/Numeral_Type.thy

 (*  Title:      HOL/Library/Numeral_Type.thy
     Author:     Brian Huffman
 *)
 
-section {* Numeral Syntax for Types *}
+section \<open>Numeral Syntax for Types\<close>
 
 theory Numeral_Type
 imports Cardinality
 begin
 
-subsection {* Numeral Types *}
+subsection \<open>Numeral Types\<close>
 
 typedef num0 = "UNIV :: nat set" ..
 typedef num1 = "UNIV :: unit set" ..
 
 typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}"

     by simp
   show "2 \<le> CARD('a bit1)"
     by simp
 qed
 
-subsection {* Locales for for modular arithmetic subtypes *}
+subsection \<open>Locales for for modular arithmetic subtypes\<close>
 
 locale mod_type =
   fixes n :: int
   and Rep :: "'a::{zero,one,plus,times,uminus,minus} \<Rightarrow> int"
   and Abs :: "int \<Rightarrow> 'a::{zero,one,plus,times,uminus,minus}"

 by (cases x rule: cases) simp
 
 end
 
 
-subsection {* Ring class instances *}
-
-text {*
+subsection \<open>Ring class instances\<close>
+
+text \<open>
   Unfortunately @{text ring_1} instance is not possible for
   @{typ num1}, since 0 and 1 are not distinct.
-*}
+\<close>
 
 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}"
 begin
 
 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"

   mod_ring "int CARD('a::finite bit1)"
            "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
            "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
   ..
 
-text {* Set up cases, induction, and arithmetic *}
+text \<open>Set up cases, induction, and arithmetic\<close>
 
 lemmas bit0_cases [case_names of_int, cases type: bit0] = bit0.cases
 lemmas bit1_cases [case_names of_int, cases type: bit1] = bit1.cases
 
 lemmas bit0_induct [case_names of_int, induct type: bit0] = bit0.induct

 lemmas bit1_iszero_numeral [simp] = bit1.iszero_numeral
 
 lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit0"] for dummy :: "'a::finite"
 lemmas [simp] = eq_numeral_iff_iszero [where 'a="'a bit1"] for dummy :: "'a::finite"
 
-subsection {* Order instances *}
+subsection \<open>Order instances\<close>
 
 instantiation bit0 and bit1 :: (finite) linorder begin
 definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
 definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
 definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"

     by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
   thus "OFCLASS('a bit1, wellorder_class)"
     by(rule wf_wellorderI) intro_classes
 qed
 
-subsection {* Code setup and type classes for code generation *}
-
-text {* Code setup for @{typ num0} and @{typ num1} *}
+subsection \<open>Code setup and type classes for code generation\<close>
+
+text \<open>Code setup for @{typ num0} and @{typ num1}\<close>
 
 definition Num0 :: num0 where "Num0 = Abs_num0 0"
 code_datatype Num0
 
 instantiation num0 :: equal begin

   by intro_classes
      (simp_all add: finite_UNIV_num0_def card_UNIV_num0_def infinite_num0 finite_UNIV_num1_def card_UNIV_num1_def)
 end
 
 
-text {* Code setup for @{typ "'a bit0"} and @{typ "'a bit1"} *}
+text \<open>Code setup for @{typ "'a bit0"} and @{typ "'a bit1"}\<close>
 
 declare
   bit0.Rep_inverse[code abstype]
   bit0.Rep_0[code abstract]
   bit0.Rep_1[code abstract]

 definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
 definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom (card_UNIV :: 'a card_UNIV))"
 instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV)
 end
 
-subsection {* Syntax *}
+subsection \<open>Syntax\<close>
 
 syntax
   "_NumeralType" :: "num_token => type"  ("_")
   "_NumeralType0" :: type ("0")
   "_NumeralType1" :: type ("1")
 
 translations
   (type) "1" == (type) "num1"
   (type) "0" == (type) "num0"
 
-parse_translation {*
+parse_translation \<open>
   let
     fun mk_bintype n =
       let
         fun mk_bit 0 = Syntax.const @{type_syntax bit0}
           | mk_bit 1 = Syntax.const @{type_syntax bit1};

 
     fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
       | numeral_tr ts = raise TERM ("numeral_tr", ts);
 
   in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
-*}
-
-print_translation {*
+\<close>
+
+print_translation \<open>
   let
     fun int_of [] = 0
       | int_of (b :: bs) = b + 2 * int_of bs;
 
     fun bin_of (Const (@{type_syntax num0}, _)) = []

       | bit_tr' b _ = raise Match;
   in
    [(@{type_syntax bit0}, K (bit_tr' 0)),
     (@{type_syntax bit1}, K (bit_tr' 1))]
   end;
-*}
-
-subsection {* Examples *}
+\<close>
+
+subsection \<open>Examples\<close>
 
 lemma "CARD(0) = 0" by simp
 lemma "CARD(17) = 17" by simp
 lemma "8 * 11 ^ 3 - 6 = (2::5)" by simp