src/HOL/String.thy
changeset 59484 a130ae7a9398
parent 59483 ddb73392356e
child 59621 291934bac95e
     1.1 --- a/src/HOL/String.thy	Thu Feb 05 19:44:13 2015 +0100
     1.2 +++ b/src/HOL/String.thy	Thu Feb 05 19:44:14 2015 +0100
     1.3 @@ -319,6 +319,10 @@
     1.4      by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
     1.5  qed
     1.6  
     1.7 +lemma char_of_nat_nibble_pair [simp]:
     1.8 +  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
     1.9 +  by (simp add: nat_of_char_Char [symmetric])
    1.10 +
    1.11  lemma inj_nat_of_char:
    1.12    "inj nat_of_char"
    1.13    by (rule inj_on_inverseI) (rule char_of_nat_of_char)
    1.14 @@ -355,12 +359,16 @@
    1.15  typedef literal = "UNIV :: string set"
    1.16    morphisms explode STR ..
    1.17  
    1.18 -setup_lifting (no_code) type_definition_literal
    1.19 +setup_lifting type_definition_literal
    1.20 +
    1.21 +lemma STR_inject' [simp]:
    1.22 +  "STR s = STR t \<longleftrightarrow> s = t"
    1.23 +  by transfer rule
    1.24  
    1.25  definition implode :: "string \<Rightarrow> String.literal"
    1.26  where
    1.27 -  "implode = STR"
    1.28 -
    1.29 +  [code del]: "implode = STR"
    1.30 +  
    1.31  instantiation literal :: size
    1.32  begin
    1.33  
    1.34 @@ -388,10 +396,6 @@
    1.35    shows "HOL.equal s s \<longleftrightarrow> True"
    1.36    by (simp add: equal)
    1.37  
    1.38 -lemma STR_inject' [simp]:
    1.39 -  "STR xs = STR ys \<longleftrightarrow> xs = ys"
    1.40 -  by (simp add: STR_inject)
    1.41 -
    1.42  lifting_update literal.lifting
    1.43  lifting_forget literal.lifting
    1.44