more direct construction of integer_of_num;
authorhaftmann
Sat Jun 24 09:17:35 2017 +0200 (24 months ago)
changeset 66190a41435469559
parent 66189 23917e861eaa
child 66191 d91108ba9474
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:33 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Jun 24 09:17:35 2017 +0200
     1.3 @@ -149,24 +149,19 @@
     1.4    "int_of_integer (Num.sub k l) = Num.sub k l"
     1.5    by transfer rule
     1.6  
     1.7 -lift_definition integer_of_num :: "num \<Rightarrow> integer"
     1.8 -  is "numeral :: num \<Rightarrow> int"
     1.9 -  .
    1.10 +definition integer_of_num :: "num \<Rightarrow> integer"
    1.11 +  where [simp]: "integer_of_num = numeral"
    1.12  
    1.13  lemma integer_of_num [code]:
    1.14 -  "integer_of_num num.One = 1"
    1.15 -  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
    1.16 -  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
    1.17 -  by (transfer, simp only: numeral.simps Let_def)+
    1.18 -
    1.19 -lemma numeral_unfold_integer_of_num:
    1.20 -  "numeral = integer_of_num"
    1.21 -  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
    1.22 +  "integer_of_num Num.One = 1"
    1.23 +  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
    1.24 +  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
    1.25 +  by (simp_all only: integer_of_num_def numeral.simps Let_def)
    1.26  
    1.27  lemma integer_of_num_triv:
    1.28    "integer_of_num Num.One = 1"
    1.29    "integer_of_num (Num.Bit0 Num.One) = 2"
    1.30 -  by (transfer, simp)+
    1.31 +  by simp_all
    1.32  
    1.33  instantiation integer :: "{linordered_idom, equal}"
    1.34  begin
    1.35 @@ -301,7 +296,7 @@
    1.36  end
    1.37  
    1.38  declare divmod_algorithm_code [where ?'a = integer,
    1.39 -  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, 
    1.40 +  folded integer_of_num_def, unfolded integer_of_num_triv, 
    1.41    code]
    1.42  
    1.43  lemma integer_of_nat_0: "integer_of_nat 0 = 0"
     2.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:33 2017 +0200
     2.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Jun 24 09:17:35 2017 +0200
     2.3 @@ -59,7 +59,7 @@
     2.4  
     2.5  lemma [code abstract]:
     2.6    "integer_of_nat (nat_of_num n) = integer_of_num n"
     2.7 -  by transfer (simp add: nat_of_num_numeral)
     2.8 +  by (simp add: nat_of_num_numeral integer_of_nat_numeral)
     2.9  
    2.10  lemma [code abstract]:
    2.11    "integer_of_nat 0 = 0"
     3.1 --- a/src/HOL/String.thy	Sat Jun 24 09:17:33 2017 +0200
     3.2 +++ b/src/HOL/String.thy	Sat Jun 24 09:17:35 2017 +0200
     3.3 @@ -160,35 +160,10 @@
     3.4    by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
     3.5      id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
     3.6  
     3.7 -lemma less_256_integer_of_char_Char:
     3.8 -  assumes "numeral k < (256 :: integer)"
     3.9 -  shows "integer_of_char (Char k) = numeral k"
    3.10 -proof -
    3.11 -  have "numeral k mod 256 = (numeral k :: integer)"
    3.12 -    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
    3.13 -  then show ?thesis using integer_of_char_Char [of k]
    3.14 -    by (simp only:)
    3.15 -qed
    3.16 -
    3.17 -setup \<open>
    3.18 -let
    3.19 -  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
    3.20 -  val simpset =
    3.21 -    put_simpset HOL_ss @{context}
    3.22 -      addsimps @{thms numeral_less_iff less_num_simps};
    3.23 -  fun mk_code_eqn ct =
    3.24 -    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
    3.25 -    |> full_simplify simpset;
    3.26 -  val code_eqns = map mk_code_eqn chars;
    3.27 -in
    3.28 -  Global_Theory.note_thmss ""
    3.29 -    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
    3.30 -  #> snd
    3.31 -end
    3.32 -\<close>
    3.33 -
    3.34 -declare integer_of_char_simps [code]
    3.35 -
    3.36 +lemma integer_of_char_Char_code [code]:
    3.37 +  "integer_of_char (Char k) = integer_of_num k mod 256"
    3.38 +  by simp
    3.39 +  
    3.40  lemma nat_of_char_code [code]:
    3.41    "nat_of_char = nat_of_integer \<circ> integer_of_char"
    3.42    by (simp add: integer_of_char_def fun_eq_iff)