make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
authorAndreas Lochbihler
Wed Feb 12 08:56:38 2014 +0100 (2014-02-12)
changeset 5542690f2ceed2828
parent 55391 eae296b5ef33
child 55427 ff54d22fe357
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
src/HOL/Library/Char_ord.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Feb 11 12:08:44 2014 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Feb 12 08:56:38 2014 +0100
     1.3 @@ -97,6 +97,7 @@
     1.4  instantiation String.literal :: linorder
     1.5  begin
     1.6  
     1.7 +context includes literal.lifting begin
     1.8  lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
     1.9  lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
    1.10  
    1.11 @@ -109,6 +110,7 @@
    1.12  qed
    1.13  
    1.14  end
    1.15 +end
    1.16  
    1.17  lemma less_literal_code [code]: 
    1.18    "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
    1.19 @@ -118,6 +120,9 @@
    1.20    "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
    1.21  by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.22  
    1.23 +lifting_update literal.lifting
    1.24 +lifting_forget literal.lifting
    1.25 +
    1.26  text {* Legacy aliasses *}
    1.27  
    1.28  lemmas nibble_less_eq_def = less_eq_nibble_def
     2.1 --- a/src/HOL/String.thy	Tue Feb 11 12:08:44 2014 +0100
     2.2 +++ b/src/HOL/String.thy	Wed Feb 12 08:56:38 2014 +0100
     2.3 @@ -391,6 +391,9 @@
     2.4    "STR xs = STR ys \<longleftrightarrow> xs = ys"
     2.5    by (simp add: STR_inject)
     2.6  
     2.7 +lifting_update literal.lifting
     2.8 +lifting_forget literal.lifting
     2.9 +
    2.10  subsection {* Code generator *}
    2.11  
    2.12  ML_file "Tools/string_code.ML"