src/HOL/Code_Numeral.thy

 (*  Title:      HOL/Code_Numeral.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
 
-section {* Numeric types for code generation onto target language numerals only *}
+section \<open>Numeric types for code generation onto target language numerals only\<close>
 
 theory Code_Numeral
 imports Nat_Transfer Divides Lifting
 begin
 
-subsection {* Type of target language integers *}
+subsection \<open>Type of target language integers\<close>
 
 typedef integer = "UNIV \<Colon> int set"
   morphisms int_of_integer integer_of_int ..
 
 setup_lifting type_definition_integer

 
 lemma integer_of_nat_numeral:
   "integer_of_nat (numeral n) = numeral n"
 by transfer simp
 
-subsection {* Code theorems for target language integers *}
-
-text {* Constructors *}
+subsection \<open>Code theorems for target language integers\<close>
+
+text \<open>Constructors\<close>
 
 definition Pos :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Pos = numeral"
 

   by (simp add: Neg_def [abs_def]) transfer_prover
 
 code_datatype "0::integer" Pos Neg
 
 
-text {* Auxiliary operations *}
+text \<open>Auxiliary operations\<close>
 
 lift_definition dup :: "integer \<Rightarrow> integer"
   is "\<lambda>k::int. k + k"
   .
 

   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+
 
 
-text {* Implementations *}
+text \<open>Implementations\<close>
 
 lemma one_integer_code [code, code_unfold]:
   "1 = Pos Num.One"
   by simp
 

   by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
 
 hide_const (open) Pos Neg sub dup divmod_abs
 
 
-subsection {* Serializer setup for target language integers *}
+subsection \<open>Serializer setup for target language integers\<close>
 
 code_reserved Eval int Integer abs
 
 code_printing
   type_constructor integer \<rightharpoonup>

     (SML) "!(0/ :/ IntInf.int)"
     and (OCaml) "Big'_int.zero'_big'_int"
     and (Haskell) "!(0/ ::/ Integer)"
     and (Scala) "BigInt(0)"
 
-setup {*
+setup \<open>
   fold (fn target =>
     Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
     #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
     ["SML", "OCaml", "Haskell", "Scala"]
-*}
+\<close>
 
 code_printing
   constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
     (SML) "IntInf.+ ((_), (_))"
     and (OCaml) "Big'_int.add'_big'_int"

 
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 
-subsection {* Type of target language naturals *}
+subsection \<open>Type of target language naturals\<close>
 
 typedef natural = "UNIV \<Colon> nat set"
   morphisms nat_of_natural natural_of_nat ..
 
 setup_lifting type_definition_natural

 lemma [measure_function]:
   "is_measure nat_of_natural"
   by (rule is_measure_trivial)
 
 
-subsection {* Inductive representation of target language naturals *}
+subsection \<open>Inductive representation of target language naturals\<close>
 
 lift_definition Suc :: "natural \<Rightarrow> natural"
   is Nat.Suc
   .
 

   by transfer simp
 
 hide_const (open) Suc
 
 
-subsection {* Code refinement for target language naturals *}
+subsection \<open>Code refinement for target language naturals\<close>
 
 lift_definition Nat :: "integer \<Rightarrow> natural"
   is nat
   .