src/HOL/String.thy
changeset 39250 548a3e5521ab
parent 39198 f967a16dfcdd
child 39272 0b61951d2682
     1.1 --- a/src/HOL/String.thy	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -152,18 +152,36 @@
     1.4    Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
     1.5  
     1.6  
     1.7 -subsection {* Strings as dedicated datatype *}
     1.8 +subsection {* Strings as dedicated type *}
     1.9 +
    1.10 +typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
    1.11 +  morphisms explode STR ..
    1.12 +
    1.13 +code_datatype STR
    1.14  
    1.15 -datatype literal = STR string
    1.16 +instantiation literal :: size
    1.17 +begin
    1.18  
    1.19 -declare literal.cases [code del] literal.recs [code del]
    1.20 +definition size_literal :: "literal \<Rightarrow> nat"
    1.21 +where
    1.22 +  [code]: "size_literal (s\<Colon>literal) = 0"
    1.23  
    1.24 -lemma [code]: "size (s\<Colon>literal) = 0"
    1.25 -  by (cases s) simp_all
    1.26 +instance ..
    1.27 +
    1.28 +end
    1.29 +
    1.30 +instantiation literal :: equal
    1.31 +begin
    1.32  
    1.33 -lemma [code]: "literal_size (s\<Colon>literal) = 0"
    1.34 -  by (cases s) simp_all
    1.35 +definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
    1.36 +where
    1.37 +  "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
    1.38  
    1.39 +instance
    1.40 +proof
    1.41 +qed (auto simp add: equal_literal_def explode_inject)
    1.42 +
    1.43 +end
    1.44  
    1.45  subsection {* Code generator *}
    1.46  
    1.47 @@ -231,4 +249,4 @@
    1.48  code_modulename Haskell
    1.49    String String
    1.50  
    1.51 -end
    1.52 \ No newline at end of file
    1.53 +end