fiddling with the correct setup for String.literal
authorbulwahn
Fri Sep 10 10:59:09 2010 +0200 (2010-09-10)
changeset 39274b17ffa965223
parent 39273 92aa2a0f7399
child 39275 dd84daec5d3c
fiddling with the correct setup for String.literal
src/HOL/Code_Evaluation.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Sep 10 10:59:07 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Sep 10 10:59:09 2010 +0200
     1.3 @@ -159,6 +159,18 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +instantiation String.literal :: term_of
     1.8 +begin
     1.9 +
    1.10 +definition
    1.11 +  "term_of s = App (Const (STR ''STR'')
    1.12 +    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
    1.13 +      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
    1.14 +
    1.15 +instance ..
    1.16 +
    1.17 +end
    1.18 +
    1.19  subsubsection {* Code generator setup *}
    1.20  
    1.21  lemmas [code del] = term.recs term.cases term.size
     2.1 --- a/src/HOL/String.thy	Fri Sep 10 10:59:07 2010 +0200
     2.2 +++ b/src/HOL/String.thy	Fri Sep 10 10:59:09 2010 +0200
     2.3 @@ -157,8 +157,6 @@
     2.4  typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
     2.5    morphisms explode STR ..
     2.6  
     2.7 -code_datatype STR
     2.8 -
     2.9  instantiation literal :: size
    2.10  begin
    2.11  
    2.12 @@ -183,6 +181,10 @@
    2.13  
    2.14  end
    2.15  
    2.16 +lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
    2.17 +by(simp add: STR_inject)
    2.18 +
    2.19 +
    2.20  subsection {* Code generator *}
    2.21  
    2.22  use "Tools/string_code.ML"