# HG changeset patch
# User bulwahn
# Date 1284035894 -7200
# Node ID 548a3e5521ab5611473ea79576221dfac76757a5
# Parent  9c866b248cb1ed6419a0a2bfef401f58364d8e3d
changing String.literal to a type instead of a datatype

diff -r 9c866b248cb1 -r 548a3e5521ab NEWS
--- a/NEWS	Thu Sep 09 11:10:44 2010 +0200
+++ b/NEWS	Thu Sep 09 14:38:14 2010 +0200
@@ -71,6 +71,8 @@
 
 *** HOL ***
 
+* String.literal is a type, but not a datatype. INCOMPATIBILITY.
+ 
 * Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
 
 * Renamed class eq and constant eq (for code generation) to class equal
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -30,10 +30,6 @@
 
 instance int :: heap ..
 
-instance String.literal :: countable
-  by (rule countable_classI [of "String.literal_case to_nat"])
-   (auto split: String.literal.splits)
-
 instance String.literal :: heap ..
 
 instance typerep :: heap ..
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -402,12 +402,15 @@
 
 subsubsection {* Logical intermediate layer *}
 
-primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
-  [code del, code_post]: "raise' (STR s) = raise s"
+definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
+  [code del]: "raise' s = raise (explode s)"
+
+lemma [code_post]: "raise' (STR s) = raise s"
+unfolding raise'_def by (simp add: STR_inverse)
 
 lemma raise_raise' [code_inline]:
   "raise s = raise' (STR s)"
-  by simp
+  unfolding raise'_def by (simp add: STR_inverse)
 
 code_datatype raise' -- {* avoid @{const "Heap"} formally *}
 
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -44,14 +44,6 @@
 definition implode :: "string \<Rightarrow> String.literal" where
   "implode = STR"
 
-primrec explode :: "String.literal \<Rightarrow> string" where
-  "explode (STR s) = s"
-
-lemma [code]:
-  "literal_case f s = f (explode s)"
-  "literal_rec f s = f (explode s)"
-  by (cases s, simp)+
-
 code_reserved SML String
 
 code_const implode
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Library/Countable.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -100,8 +100,8 @@
 text {* Further *}
 
 instance String.literal :: countable
-  by (rule countable_classI [of "String.literal_case to_nat"])
-   (auto split: String.literal.splits)
+  by (rule countable_classI [of "to_nat o explode"])
+    (auto simp add: explode_inject)
 
 instantiation typerep :: countable
 begin
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/String.thy	Thu Sep 09 14:38:14 2010 +0200
@@ -152,18 +152,36 @@
   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
 
 
-subsection {* Strings as dedicated datatype *}
+subsection {* Strings as dedicated type *}
+
+typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
+  morphisms explode STR ..
+
+code_datatype STR
 
-datatype literal = STR string
+instantiation literal :: size
+begin
 
-declare literal.cases [code del] literal.recs [code del]
+definition size_literal :: "literal \<Rightarrow> nat"
+where
+  [code]: "size_literal (s\<Colon>literal) = 0"
 
-lemma [code]: "size (s\<Colon>literal) = 0"
-  by (cases s) simp_all
+instance ..
+
+end
+
+instantiation literal :: equal
+begin
 
-lemma [code]: "literal_size (s\<Colon>literal) = 0"
-  by (cases s) simp_all
+definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
+where
+  "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
 
+instance
+proof
+qed (auto simp add: equal_literal_def explode_inject)
+
+end
 
 subsection {* Code generator *}
 
@@ -231,4 +249,4 @@
 code_modulename Haskell
   String String
 
-end
\ No newline at end of file
+end
diff -r 9c866b248cb1 -r 548a3e5521ab src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Sep 09 11:10:44 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Sep 09 14:38:14 2010 +0200
@@ -596,9 +596,9 @@
 
 val literalT = Type ("String.literal", []);
 
-fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
+fun mk_literal s = Const ("String.STR", stringT --> literalT)
       $ mk_string s;
-fun dest_literal (Const ("String.literal.STR", _) $ t) =
+fun dest_literal (Const ("String.STR", _) $ t) =
       dest_string t
   | dest_literal t = raise TERM ("dest_literal", [t]);