changing String.literal to a type instead of a datatype
authorbulwahn
Thu Sep 09 14:38:14 2010 +0200 (2010-09-09)
changeset 39250548a3e5521ab
parent 39249 9c866b248cb1
child 39251 8756b44582e2
child 39252 8f176e575a49
changing String.literal to a type instead of a datatype
NEWS
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Countable.thy
src/HOL/String.thy
src/HOL/Tools/hologic.ML
     1.1 --- a/NEWS	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/NEWS	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -71,6 +71,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* String.literal is a type, but not a datatype. INCOMPATIBILITY.
     1.8 + 
     1.9  * Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
    1.10  
    1.11  * Renamed class eq and constant eq (for code generation) to class equal
     2.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 09 11:10:44 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 09 14:38:14 2010 +0200
     2.3 @@ -30,10 +30,6 @@
     2.4  
     2.5  instance int :: heap ..
     2.6  
     2.7 -instance String.literal :: countable
     2.8 -  by (rule countable_classI [of "String.literal_case to_nat"])
     2.9 -   (auto split: String.literal.splits)
    2.10 -
    2.11  instance String.literal :: heap ..
    2.12  
    2.13  instance typerep :: heap ..
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 11:10:44 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 14:38:14 2010 +0200
     3.3 @@ -402,12 +402,15 @@
     3.4  
     3.5  subsubsection {* Logical intermediate layer *}
     3.6  
     3.7 -primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
     3.8 -  [code del, code_post]: "raise' (STR s) = raise s"
     3.9 +definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
    3.10 +  [code del]: "raise' s = raise (explode s)"
    3.11 +
    3.12 +lemma [code_post]: "raise' (STR s) = raise s"
    3.13 +unfolding raise'_def by (simp add: STR_inverse)
    3.14  
    3.15  lemma raise_raise' [code_inline]:
    3.16    "raise s = raise' (STR s)"
    3.17 -  by simp
    3.18 +  unfolding raise'_def by (simp add: STR_inverse)
    3.19  
    3.20  code_datatype raise' -- {* avoid @{const "Heap"} formally *}
    3.21  
     4.1 --- a/src/HOL/Library/Code_Char.thy	Thu Sep 09 11:10:44 2010 +0200
     4.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Sep 09 14:38:14 2010 +0200
     4.3 @@ -44,14 +44,6 @@
     4.4  definition implode :: "string \<Rightarrow> String.literal" where
     4.5    "implode = STR"
     4.6  
     4.7 -primrec explode :: "String.literal \<Rightarrow> string" where
     4.8 -  "explode (STR s) = s"
     4.9 -
    4.10 -lemma [code]:
    4.11 -  "literal_case f s = f (explode s)"
    4.12 -  "literal_rec f s = f (explode s)"
    4.13 -  by (cases s, simp)+
    4.14 -
    4.15  code_reserved SML String
    4.16  
    4.17  code_const implode
     5.1 --- a/src/HOL/Library/Countable.thy	Thu Sep 09 11:10:44 2010 +0200
     5.2 +++ b/src/HOL/Library/Countable.thy	Thu Sep 09 14:38:14 2010 +0200
     5.3 @@ -100,8 +100,8 @@
     5.4  text {* Further *}
     5.5  
     5.6  instance String.literal :: countable
     5.7 -  by (rule countable_classI [of "String.literal_case to_nat"])
     5.8 -   (auto split: String.literal.splits)
     5.9 +  by (rule countable_classI [of "to_nat o explode"])
    5.10 +    (auto simp add: explode_inject)
    5.11  
    5.12  instantiation typerep :: countable
    5.13  begin
     6.1 --- a/src/HOL/String.thy	Thu Sep 09 11:10:44 2010 +0200
     6.2 +++ b/src/HOL/String.thy	Thu Sep 09 14:38:14 2010 +0200
     6.3 @@ -152,18 +152,36 @@
     6.4    Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
     6.5  
     6.6  
     6.7 -subsection {* Strings as dedicated datatype *}
     6.8 +subsection {* Strings as dedicated type *}
     6.9 +
    6.10 +typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
    6.11 +  morphisms explode STR ..
    6.12 +
    6.13 +code_datatype STR
    6.14  
    6.15 -datatype literal = STR string
    6.16 +instantiation literal :: size
    6.17 +begin
    6.18  
    6.19 -declare literal.cases [code del] literal.recs [code del]
    6.20 +definition size_literal :: "literal \<Rightarrow> nat"
    6.21 +where
    6.22 +  [code]: "size_literal (s\<Colon>literal) = 0"
    6.23  
    6.24 -lemma [code]: "size (s\<Colon>literal) = 0"
    6.25 -  by (cases s) simp_all
    6.26 +instance ..
    6.27 +
    6.28 +end
    6.29 +
    6.30 +instantiation literal :: equal
    6.31 +begin
    6.32  
    6.33 -lemma [code]: "literal_size (s\<Colon>literal) = 0"
    6.34 -  by (cases s) simp_all
    6.35 +definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
    6.36 +where
    6.37 +  "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
    6.38  
    6.39 +instance
    6.40 +proof
    6.41 +qed (auto simp add: equal_literal_def explode_inject)
    6.42 +
    6.43 +end
    6.44  
    6.45  subsection {* Code generator *}
    6.46  
    6.47 @@ -231,4 +249,4 @@
    6.48  code_modulename Haskell
    6.49    String String
    6.50  
    6.51 -end
    6.52 \ No newline at end of file
    6.53 +end
     7.1 --- a/src/HOL/Tools/hologic.ML	Thu Sep 09 11:10:44 2010 +0200
     7.2 +++ b/src/HOL/Tools/hologic.ML	Thu Sep 09 14:38:14 2010 +0200
     7.3 @@ -596,9 +596,9 @@
     7.4  
     7.5  val literalT = Type ("String.literal", []);
     7.6  
     7.7 -fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
     7.8 +fun mk_literal s = Const ("String.STR", stringT --> literalT)
     7.9        $ mk_string s;
    7.10 -fun dest_literal (Const ("String.literal.STR", _) $ t) =
    7.11 +fun dest_literal (Const ("String.STR", _) $ t) =
    7.12        dest_string t
    7.13    | dest_literal t = raise TERM ("dest_literal", [t]);
    7.14