# HG changeset patch
# User haftmann
# Date 1192177742 -7200
# Node ID 1ab44e69652fe309a602172a35a36369db1b3ec8
# Parent  1dbe785ed529e59031501aee3e9d3ae8400571a7
removed

diff -r 1dbe785ed529 -r 1ab44e69652f src/HOL/Library/ML_Int.thy
--- a/src/HOL/Library/ML_Int.thy	Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Built-in integers for code generation *}
-
-theory ML_Int
-imports PreList
-begin
-
-subsection {* Datatype of built-in integers *}
-
-datatype ml_int = ml_int_of_int int
-
-lemmas [code func del] = ml_int.recs ml_int.cases
-
-fun
-  int_of_ml_int :: "ml_int \<Rightarrow> int"
-where
-  "int_of_ml_int (ml_int_of_int k) = k"
-lemmas [code func del] = int_of_ml_int.simps
-
-lemma ml_int_id [simp]:
-  "ml_int_of_int (int_of_ml_int k) = k"
-  by (cases k) simp_all
-
-lemma ml_int:
-  "(\<And>k\<Colon>ml_int. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (ml_int_of_int k))"
-proof
-  fix k :: int
-  assume "\<And>k\<Colon>ml_int. PROP P k"
-  then show "PROP P (ml_int_of_int k)" .
-next
-  fix k :: ml_int
-  assume "\<And>k\<Colon>int. PROP P (ml_int_of_int k)"
-  then have "PROP P (ml_int_of_int (int_of_ml_int k))" .
-  then show "PROP P k" by simp
-qed
-
-lemma [code func]: "size (k\<Colon>ml_int) = 0"
-  by (cases k) simp_all
-
-
-subsection {* Built-in integers as datatype on numerals *}
-
-instance ml_int :: number
-  "number_of \<equiv> ml_int_of_int" ..
-
-code_datatype "number_of \<Colon> int \<Rightarrow> ml_int"
-
-lemma number_of_ml_int_id [simp]:
-  "number_of (int_of_ml_int k) = k"
-  unfolding number_of_ml_int_def by simp
-
-lemma number_of_ml_int_shift:
-  "number_of k = ml_int_of_int (number_of k)"
-  by (simp add: number_of_is_id number_of_ml_int_def)
-
-
-subsection {* Basic arithmetic *}
-
-instance ml_int :: zero
-  [simp]: "0 \<equiv> ml_int_of_int 0" ..
-lemmas [code func del] = zero_ml_int_def
-
-instance ml_int :: one
-  [simp]: "1 \<equiv> ml_int_of_int 1" ..
-lemmas [code func del] = one_ml_int_def
-
-instance ml_int :: plus
-  [simp]: "k + l \<equiv> ml_int_of_int (int_of_ml_int k + int_of_ml_int l)" ..
-lemmas [code func del] = plus_ml_int_def
-lemma plus_ml_int_code [code func]:
-  "ml_int_of_int k + ml_int_of_int l = ml_int_of_int (k + l)"
-  unfolding plus_ml_int_def by simp
-
-instance ml_int :: minus
-  [simp]: "- k \<equiv> ml_int_of_int (- int_of_ml_int k)"
-  [simp]: "k - l \<equiv> ml_int_of_int (int_of_ml_int k - int_of_ml_int l)" ..
-lemmas [code func del] = uminus_ml_int_def minus_ml_int_def
-lemma uminus_ml_int_code [code func]:
-  "- ml_int_of_int k \<equiv> ml_int_of_int (- k)"
-  unfolding uminus_ml_int_def by simp
-lemma minus_ml_int_code [code func]:
-  "ml_int_of_int k - ml_int_of_int l = ml_int_of_int (k - l)"
-  unfolding minus_ml_int_def by simp
-
-instance ml_int :: times
-  [simp]: "k * l \<equiv> ml_int_of_int (int_of_ml_int k * int_of_ml_int l)" ..
-lemmas [code func del] = times_ml_int_def
-lemma times_ml_int_code [code func]:
-  "ml_int_of_int k * ml_int_of_int l = ml_int_of_int (k * l)"
-  unfolding times_ml_int_def by simp
-
-instance ml_int :: ord
-  [simp]: "k \<le> l \<equiv> int_of_ml_int k \<le> int_of_ml_int l"
-  [simp]: "k < l \<equiv> int_of_ml_int k < int_of_ml_int l" ..
-lemmas [code func del] = less_eq_ml_int_def less_ml_int_def
-lemma less_eq_ml_int_code [code func]:
-  "ml_int_of_int k \<le> ml_int_of_int l \<longleftrightarrow> k \<le> l"
-  unfolding less_eq_ml_int_def by simp
-lemma less_ml_int_code [code func]:
-  "ml_int_of_int k < ml_int_of_int l \<longleftrightarrow> k < l"
-  unfolding less_ml_int_def by simp
-
-instance ml_int :: ring_1
-  by default (auto simp add: left_distrib right_distrib)
-
-lemma of_nat_ml_int: "of_nat n = ml_int_of_int (of_nat n)"
-proof (induct n)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-  then have "int_of_ml_int (ml_int_of_int (int n))
-    = int_of_ml_int (of_nat n)" by simp
-  then have "int n = int_of_ml_int (of_nat n)" by simp
-  then show ?case by simp
-qed
-
-instance ml_int :: number_ring
-  by default
-    (simp_all add: left_distrib number_of_ml_int_def of_int_of_nat of_nat_ml_int)
-
-lemma zero_ml_int_code [code inline, code func]:
-  "(0\<Colon>ml_int) = Numeral0"
-  by simp
-
-lemma one_ml_int_code [code inline, code func]:
-  "(1\<Colon>ml_int) = Numeral1"
-  by simp
-
-instance ml_int :: abs
-  "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
-
-lemma ml_int_of_int [code func]:
-  "ml_int_of_int k = (if k = 0 then 0
-    else if k = -1 then -1
-    else let (l, m) = divAlg (k, 2) in 2 * ml_int_of_int l +
-      (if m = 0 then 0 else 1))"
-  by (simp add: number_of_ml_int_shift Let_def split_def divAlg_mod_div) arith
-
-
-subsection {* Conversion to and from @{typ nat} *}
-
-definition
-  nat_of_ml_int :: "ml_int \<Rightarrow> nat"
-where
-  [code func del]: "nat_of_ml_int = nat o int_of_ml_int"
-
-definition
-  nat_of_ml_int_aux :: "ml_int \<Rightarrow> nat \<Rightarrow> nat" where
-  [code func del]: "nat_of_ml_int_aux i n = nat_of_ml_int i + n"
-
-lemma nat_of_ml_int_aux_code [code]:
-  "nat_of_ml_int_aux i n = (if i \<le> 0 then n else nat_of_ml_int_aux (i - 1) (Suc n))"
-  by (auto simp add: nat_of_ml_int_aux_def nat_of_ml_int_def)
-
-lemma nat_of_ml_int_code [code]:
-  "nat_of_ml_int i = nat_of_ml_int_aux i 0"
-  by (simp add: nat_of_ml_int_aux_def)
-
-definition
-  ml_int_of_nat :: "nat \<Rightarrow> ml_int"
-where
-  [code func del]: "ml_int_of_nat = ml_int_of_int o of_nat"
-
-lemma ml_int_of_nat [code func]:
-  "ml_int_of_nat 0 = 0"
-  "ml_int_of_nat (Suc n) = ml_int_of_nat n + 1"
-  unfolding ml_int_of_nat_def by simp_all
-
-lemma ml_int_nat_id [simp]:
-  "nat_of_ml_int (ml_int_of_nat n) = n"
-  "ml_int_of_nat (nat_of_ml_int i) = (if i \<le> 0 then 0 else i)"
-  unfolding ml_int_of_nat_def nat_of_ml_int_def by simp_all
-
-
-subsection {* ML interface *}
-
-ML {*
-structure ML_Int =
-struct
-
-fun mk k = @{term ml_int_of_int} $ HOLogic.mk_number @{typ ml_int} k;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type ml_int
-  (SML "int")
-  (OCaml "int")
-  (Haskell "Integer")
-
-code_instance ml_int :: eq
-  (Haskell -)
-
-setup {*
-  fold (fn target => CodeTarget.add_pretty_numeral target true
-    @{const_name number_ml_int_inst.number_of_ml_int}
-    @{const_name Numeral.B0} @{const_name Numeral.B1}
-    @{const_name Numeral.Pls} @{const_name Numeral.Min}
-    @{const_name Numeral.Bit}
-  ) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML int
-code_reserved OCaml int
-
-code_const "op + \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
-  (SML "Int.+ ((_), (_))")
-  (OCaml "Pervasives.+")
-  (Haskell infixl 6 "+")
-
-code_const "uminus \<Colon> ml_int \<Rightarrow> ml_int"
-  (SML "Int.~")
-  (OCaml "Pervasives.~-")
-  (Haskell "negate")
-
-code_const "op - \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
-  (SML "Int.- ((_), (_))")
-  (OCaml "Pervasives.-")
-  (Haskell infixl 6 "-")
-
-code_const "op * \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
-  (SML "Int.* ((_), (_))")
-  (OCaml "Pervasives.*")
-  (Haskell infixl 7 "*")
-
-code_const "op = \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
-  (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : Pervasives.int) = _)")
-  (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
-  (SML "Int.<= ((_), (_))")
-  (OCaml "!((_ : Pervasives.int) <= _)")
-  (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
-  (SML "Int.< ((_), (_))")
-  (OCaml "!((_ : Pervasives.int) < _)")
-  (Haskell infix 4 "<")
-
-code_reserved SML Int
-code_reserved OCaml Pervasives
-
-end
diff -r 1dbe785ed529 -r 1ab44e69652f src/HOL/Library/ML_String.thy
--- a/src/HOL/Library/ML_String.thy	Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,86 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Monolithic strings for ML *}
-
-theory ML_String
-imports List
-begin
-
-subsection {* Motivation *}
-
-text {*
-  Strings are represented in HOL as list of characters.
-  For code generation to Haskell, this is no problem
-  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
-  On the other hand, in ML all strings have to
-  be represented as list of characters which
-  is awkward to read. This theory provides a distinguished
-  datatype for strings which then by convention
-  are serialized as monolithic ML strings.
-*}
-
-
-subsection {* Datatype of monolithic strings *}
-
-datatype ml_string = STR string
-
-lemmas [code func del] = ml_string.recs ml_string.cases
-
-lemma [code func]: "size (s\<Colon>ml_string) = 0"
-  by (cases s) simp_all
-
-subsection {* ML interface *}
-
-ML {*
-structure ML_String =
-struct
-
-fun mk s = @{term STR} $ HOLogic.mk_string s;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type ml_string
-  (SML "string")
-  (OCaml "string")
-  (Haskell "String")
-
-setup {*
-let
-  val charr = @{const_name Char}
-  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
-    @{const_name Nibble2}, @{const_name Nibble3},
-    @{const_name Nibble4}, @{const_name Nibble5},
-    @{const_name Nibble6}, @{const_name Nibble7},
-    @{const_name Nibble8}, @{const_name Nibble9},
-    @{const_name NibbleA}, @{const_name NibbleB},
-    @{const_name NibbleC}, @{const_name NibbleD},
-    @{const_name NibbleE}, @{const_name NibbleF}];
-in
-  CodeTarget.add_pretty_ml_string "SML"
-    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
-  #> CodeTarget.add_pretty_ml_string "OCaml"
-  charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
-end
-*}
-
-code_const STR
-  (Haskell "_")
-
-code_reserved SML string
-code_reserved OCaml string
-
-code_instance ml_string :: eq
-  (Haskell -)
-
-code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
-  (SML "!((_ : string) = _)")
-  (OCaml "!((_ : string) = _)")
-  (Haskell infixl 4 "==")
-
-end
diff -r 1dbe785ed529 -r 1ab44e69652f src/HOL/Library/Pretty_Char.thy
--- a/src/HOL/Library/Pretty_Char.thy	Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(*  Title:      HOL/Library/Pretty_Char.thy
-    ID:         $Id$
-    Author:     Florian Haftmann
-*)
-
-header {* Code generation of pretty characters (and strings) *}
-
-theory Pretty_Char
-imports List
-begin
-
-code_type char
-  (SML "char")
-  (OCaml "char")
-  (Haskell "Char")
-
-setup {*
-let
-  val charr = @{const_name Char}
-  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
-    @{const_name Nibble2}, @{const_name Nibble3},
-    @{const_name Nibble4}, @{const_name Nibble5},
-    @{const_name Nibble6}, @{const_name Nibble7},
-    @{const_name Nibble8}, @{const_name Nibble9},
-    @{const_name NibbleA}, @{const_name NibbleB},
-    @{const_name NibbleC}, @{const_name NibbleD},
-    @{const_name NibbleE}, @{const_name NibbleF}];
-in
-  fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
-    ["SML", "OCaml", "Haskell"]
-  #> CodeTarget.add_pretty_list_string "Haskell"
-    @{const_name Nil} @{const_name Cons} charr nibbles
-end
-*}
-
-code_instance char :: eq
-  (Haskell -)
-
-code_reserved SML
-  char
-
-code_reserved OCaml
-  char
-
-code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
-  (SML "!((_ : char) = _)")
-  (OCaml "!((_ : char) = _)")
-  (Haskell infixl 4 "==")
-
-end
diff -r 1dbe785ed529 -r 1ab44e69652f src/HOL/Library/Pretty_Char_chr.thy
--- a/src/HOL/Library/Pretty_Char_chr.thy	Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(*  Title:      HOL/Library/Pretty_Char_chr.thy
-    ID:         $Id$
-    Author:     Florian Haftmann
-*)
-
-header {* Code generation of pretty characters with character codes *}
-
-theory Pretty_Char_chr
-imports Char_nat Pretty_Char Pretty_Int
-begin
-
-definition
-  "int_of_char = int o nat_of_char"
-
-lemma [code func]:
-  "nat_of_char = nat o int_of_char"
-  unfolding int_of_char_def by (simp add: expand_fun_eq)
-
-definition
-  "char_of_int = char_of_nat o nat"
-
-lemma [code func]:
-  "char_of_nat = char_of_int o int"
-  unfolding char_of_int_def by (simp add: expand_fun_eq)
-
-lemmas [code func del] = char.recs char.cases char.size
-
-lemma [code func, code inline]:
-  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code func, code inline]:
-  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code func]:
-  "size (c\<Colon>char) = 0"
-  by (cases c) auto
-
-code_const int_of_char and char_of_int
-  (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
-  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
-  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
-
-end
\ No newline at end of file
diff -r 1dbe785ed529 -r 1ab44e69652f src/HOL/Library/Pretty_Int.thy
--- a/src/HOL/Library/Pretty_Int.thy	Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(*  Title:      HOL/Library/Pretty_Int.thy
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Pretty integer literals for code generation *}
-
-theory Pretty_Int
-imports IntArith ML_Int
-begin
-
-text {*
-  HOL numeral expressions are mapped to integer literals
-  in target languages, using predefined target language
-  operations for abstract integer operations.
-*}
-
-code_type int
-  (SML "IntInf.int")
-  (OCaml "Big'_int.big'_int")
-  (Haskell "Integer")
-
-code_instance int :: eq
-  (Haskell -)
-
-setup {*
-  fold (fn target => CodeTarget.add_pretty_numeral target true
-    @{const_name number_int_inst.number_of_int}
-    @{const_name Numeral.B0} @{const_name Numeral.B1}
-    @{const_name Numeral.Pls} @{const_name Numeral.Min}
-    @{const_name Numeral.Bit}
-  ) ["SML", "OCaml", "Haskell"]
-*}
-
-code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
-  (SML "raise/ Fail/ \"Pls\""
-     and "raise/ Fail/ \"Min\""
-     and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
-  (OCaml "failwith/ \"Pls\""
-     and "failwith/ \"Min\""
-     and "!((_);/ (_);/ failwith/ \"Bit\")")
-  (Haskell "error/ \"Pls\""
-     and "error/ \"Min\""
-     and "error/ \"Bit\"")
-
-code_const Numeral.pred
-  (SML "IntInf.- ((_), 1)")
-  (OCaml "Big'_int.pred'_big'_int")
-  (Haskell "!(_/ -/ 1)")
-
-code_const Numeral.succ
-  (SML "IntInf.+ ((_), 1)")
-  (OCaml "Big'_int.succ'_big'_int")
-  (Haskell "!(_/ +/ 1)")
-
-code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.+ ((_), (_))")
-  (OCaml "Big'_int.add'_big'_int")
-  (Haskell infixl 6 "+")
-
-code_const "uminus \<Colon> int \<Rightarrow> int"
-  (SML "IntInf.~")
-  (OCaml "Big'_int.minus'_big'_int")
-  (Haskell "negate")
-
-code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.- ((_), (_))")
-  (OCaml "Big'_int.sub'_big'_int")
-  (Haskell infixl 6 "-")
-
-code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.* ((_), (_))")
-  (OCaml "Big'_int.mult'_big'_int")
-  (Haskell infixl 7 "*")
-
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "!((_ : IntInf.int) = _)")
-  (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.<= ((_), (_))")
-  (OCaml "Big'_int.le'_big'_int")
-  (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-  (SML "IntInf.< ((_), (_))")
-  (OCaml "Big'_int.lt'_big'_int")
-  (Haskell infix 4 "<")
-
-code_const ml_int_of_int and int_of_ml_int
-  (SML "IntInf.toInt" and "IntInf.fromInt")
-  (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
-  (Haskell "_" and "_")
-
-code_reserved SML IntInf
-code_reserved OCaml Big_int
-
-end
\ No newline at end of file