theory Number
imports Main Code_Integer
begin

lemma number_of_int:
  "number_of k = (of_int (number_of k) :: 'a::number_ring)"
  by simp

class number_num = number +
  fixes num_of :: "int \<Rightarrow> 'a"
  assumes num_of: "num_of = number_of"

lemma number_of_num_of:
  "number_of k = num_of (number_of k)"
  by (simp add: num_of number_of_is_id)

instantiation nat :: number_num
begin

definition "num_of = nat"

instance proof
qed (simp add: num_of_nat_def nat_number_of_def number_of_is_id expand_fun_eq)

end

setup {*
let
  val rewrite_ring =
    let
      val thm = mk_eq @{thm number_of_int};
      val arg = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) thm;
    in fn ct => Thm.instantiate ([], [(arg, ct)]) thm end;
  val rewrite_num =
    let
      val thm = mk_eq @{thm number_of_num_of};
      val arg = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) thm;
    in fn ct => Thm.instantiate ([], [(arg, ct)]) thm end;
  fun select_rewrite sort = if Sign.subsort @{theory} (sort, @{sort number_ring})
    then SOME rewrite_ring
    else if Sign.subsort @{theory} (sort, @{sort number_num})
      then SOME rewrite_num
      else NONE;
  fun sort_of ct = case (range_type o snd o dest_Const o fst o dest_comb o Thm.term_of) ct
   of T as Type _ => NONE
    | T => SOME (Type.sort_of_atyp T);
  fun rewrite ct = case sort_of ct
   of SOME sort => (case select_rewrite sort
       of SOME f => SOME (f (Thm.dest_arg ct))
        | NONE => NONE)
    | NONE => NONE;
  val simproc = Simplifier.make_simproc { name = "number_of_int",
    lhss = [@{cpat "number_of ?k"}], identifier = [], proc = fn phi => fn ss => rewrite };
in
  Code_Preproc.map_pre (fn ss => ss addsimprocs [simproc])
end
*}

definition "example1 (a :: 'a::number_ring) = 4 * a"

definition "example2 (a :: 'a::{number_num, times}) = 4 * a"

code_thms example1 example2

export_code example1 example2 in Haskell file -

end