attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary

--- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -7,19 +7,19 @@
 imports
   Complex_Main
   "~~/src/HOL/Library/Library"
-  "~~/src/HOL/Library/Sublist"
+  "~~/src/HOL/Library/Sublist_Order"
   "~~/src/HOL/Number_Theory/Primes"
   "~~/src/HOL/ex/Records"
 begin
 
-inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-    empty: "sublist [] xs"
-  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
-  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
+inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  empty: "sublist [] xs"
+| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
+| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
 
 code_pred sublist .
 
-(*avoid popular infix*)
-code_reserved SML upto
+code_reserved SML upto -- {* avoid popular infix *}
 
 end

--- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Generating code using pretty literals and natural number literals  *}
-
-theory Candidates_Pretty
-imports Candidates Code_Char Code_Target_Numeral
-begin
-
-end

--- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -4,11 +4,12 @@
 header {* Pervasive test of code generator *}
 
 theory Generate
-imports Candidates
+imports
+  Candidates
+  "~~/src/HOL/Library/AList_Mapping"
+  "~~/src/HOL/Library/Finite_Lattice"
 begin
 
-subsection {* Check whether generated code compiles *}
-
 text {*
   If any of the checks fails, inspect the code generated
   by a corresponding @{text export_code} command.
@@ -17,3 +18,4 @@
 export_code _ checking SML OCaml? Haskell? Scala
 
 end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -0,0 +1,21 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate_Binary_Nat
+imports
+  Candidates
+  "~~/src/HOL/Library/AList_Mapping"
+  "~~/src/HOL/Library/Finite_Lattice"
+  "~~/src/HOL/Library/Code_Binary_Nat"
+begin
+
+text {*
+  If any of the checks fails, inspect the code generated
+  by a corresponding @{text export_code} command.
+*}
+
+export_code _ checking SML OCaml? Haskell? Scala
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -0,0 +1,73 @@
+
+(* Author: Ondrej Kuncar, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate_Efficient_Datastructures
+imports
+  Candidates
+  "~~/src/HOL/Library/DAList"
+  "~~/src/HOL/Library/RBT_Mapping"
+  "~~/src/HOL/Library/RBT_Set"
+begin
+
+(* 
+   The following code equations have to be deleted because they use 
+   lists to implement sets in the code generetor. 
+*)
+
+lemma [code, code del]:
+  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
+
+lemma [code, code del]:
+  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
+
+lemma [code, code del]:
+  "pred_of_set = pred_of_set" ..
+
+lemma [code, code del]:
+  "acc = acc" ..
+
+lemma [code, code del]:
+  "Cardinality.card' = Cardinality.card'" ..
+
+lemma [code, code del]:
+  "Cardinality.finite' = Cardinality.finite'" ..
+
+lemma [code, code del]:
+  "Cardinality.subset' = Cardinality.subset'" ..
+
+lemma [code, code del]:
+  "Cardinality.eq_set = Cardinality.eq_set" ..
+
+(*
+  If the code generation ends with an exception with the following message:
+  '"List.set" is not a constructor, on left hand side of equation: ...',
+  the code equation in question has to be either deleted (like many others in this file) 
+  or implemented for RBT trees.
+*)
+
+export_code _ checking SML OCaml? Haskell?
+
+(* Extra setup to make Scala happy *)
+(* If the compilation fails with an error "ambiguous implicit values",
+   read \<section>7.1 in the Code Generation Manual *)
+
+class ccpo_linorder = ccpo + linorder
+
+lemma [code]:
+  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
+    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
+unfolding admissible_def by blast
+
+lemma [code]:
+  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
+unfolding gfp_def by blast
+
+lemma [code]:
+  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
+unfolding lfp_def by blast
+
+export_code _ checking Scala?
+
+end

--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Pervasive test of code generator using pretty literals *}
-
-theory Generate_Pretty
-imports Candidates_Pretty
-begin
-
-lemma [code, code del]: "nat_of_char = nat_of_char" ..
-lemma [code, code del]: "char_of_nat = char_of_nat" ..
-
-subsection {* Check whether generated code compiles *}
-
-text {*
-  If any of the checks fails, inspect the code generated
-  by a corresponding @{text export_code} command.
-*}
-
-export_code _ checking SML OCaml? Haskell? Scala
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -0,0 +1,21 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate_Pretty_Char
+imports
+  Candidates
+  "~~/src/HOL/Library/AList_Mapping"
+  "~~/src/HOL/Library/Finite_Lattice"
+  "~~/src/HOL/Library/Code_Char"
+begin
+
+text {*
+  If any of the checks fails, inspect the code generated
+  by a corresponding @{text export_code} command.
+*}
+
+export_code _ checking SML OCaml? Haskell? Scala
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -0,0 +1,21 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate_Target_Nat
+imports
+  Candidates
+  "~~/src/HOL/Library/AList_Mapping"
+  "~~/src/HOL/Library/Finite_Lattice"
+  "~~/src/HOL/Library/Code_Target_Numeral"
+begin
+
+text {*
+  If any of the checks fails, inspect the code generated
+  by a corresponding @{text export_code} command.
+*}
+
+export_code _ checking SML OCaml? Haskell? Scala
+
+end

--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Feb 15 11:47:33 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
-    Author:     Ondrej Kuncar
-*)
-
-header {* Test of the code generator using an implementation of sets by RBT trees *}
-
-theory RBT_Set_Test
-imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
-begin
-
-(* 
-   The following code equations have to be deleted because they use 
-   lists to implement sets in the code generetor. 
-*)
-
-lemma [code, code del]:
-  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
-
-lemma [code, code del]:
-  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
-
-lemma [code, code del]:
-  "pred_of_set = pred_of_set" ..
-
-lemma [code, code del]:
-  "acc = acc" ..
-
-lemma [code, code del]:
-  "Cardinality.card' = Cardinality.card'" ..
-
-lemma [code, code del]:
-  "Cardinality.finite' = Cardinality.finite'" ..
-
-lemma [code, code del]:
-  "Cardinality.subset' = Cardinality.subset'" ..
-
-lemma [code, code del]:
-  "Cardinality.eq_set = Cardinality.eq_set" ..
-
-(*
-  If the code generation ends with an exception with the following message:
-  '"List.set" is not a constructor, on left hand side of equation: ...',
-  the code equation in question has to be either deleted (like many others in this file) 
-  or implemented for RBT trees.
-*)
-
-export_code _ checking SML OCaml? Haskell?
-
-(* Extra setup to make Scala happy *)
-(* If the compilation fails with an error "ambiguous implicit values",
-   read \<section>7.1 in the Code Generation Manual *)
-
-class ccpo_linorder = ccpo + linorder
-
-lemma [code]:
-  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
-    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
-unfolding admissible_def by blast
-
-lemma [code]:
-  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
-unfolding gfp_def by blast
-
-lemma [code]:
-  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
-unfolding lfp_def by blast
-
-export_code _ checking Scala?
-
-end

--- a/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -59,7 +59,7 @@
 proof -
   have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
     by (auto simp add: image_def intro!: bexI)
-  show ?thesis apply transfer 
+  show ?thesis apply transfer
   by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
 qed
 

--- a/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -46,6 +46,26 @@
 code_const IArray
   (SML "Vector.fromList")
 
+lemma [code]:
+"size (as :: 'a iarray) = 0"
+by (cases as) simp
+
+lemma [code]:
+"iarray_size f as = Suc (list_size f (IArray.list_of as))"
+by (cases as) simp
+
+lemma [code]:
+"iarray_rec f as = f (IArray.list_of as)"
+by (cases as) simp
+
+lemma [code]:
+"iarray_case f as = f (IArray.list_of as)"
+by (cases as) simp
+
+lemma [code]:
+"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
+by (cases as, cases bs) (simp add: equal)
+
 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
 "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
 hide_const (open) tabulate

--- a/src/HOL/Library/Library.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/Library.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -2,7 +2,7 @@
 theory Library
 imports
   Abstract_Rat
-  AList_Mapping
+  AList
   BigO
   Binomial
   Bit
@@ -29,6 +29,7 @@
   Indicator_Function
   Infinite_Set
   Inner_Product
+  IArray
   Lattice_Algebras
   Lattice_Syntax
   ListVector
@@ -37,7 +38,6 @@
   Monad_Syntax
   Multiset
   Numeral_Type
-  Old_Recdef
   OptionalSugar
   Option_ord
   Parallel
@@ -56,11 +56,10 @@
   Quotient_Type
   Ramsey
   Reflection
-  RBT_Mapping
-  (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
   Saturated
   Set_Algebras
   State_Monad
+  Sublist
   Sum_of_Squares
   Transitive_Closure_Table
   Univ_Poly

--- a/src/HOL/Library/Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -34,11 +34,13 @@
 lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
   "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" .
 
+
 subsection {* Functorial structure *}
 
 enriched_type map: map
   by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
 
+
 subsection {* Derived operations *}
 
 definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
@@ -67,6 +69,22 @@
 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "map_default k v f m = map_entry k f (default k v m)" 
 
+instantiation mapping :: (type, type) equal
+begin
+
+definition
+  "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
+
+instance proof
+qed (unfold equal_mapping_def, transfer, auto)
+
+end
+
+lemma [transfer_rule]:
+  "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
+  by (unfold equal) transfer_prover
+
+
 subsection {* Properties *}
 
 lemma lookup_update: "lookup (update k v m) k = Some v" 
@@ -258,18 +276,8 @@
 
 code_datatype empty update
 
-instantiation mapping :: (type, type) equal
-begin
-
-lift_definition equal_mapping :: "('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping \<Rightarrow> bool" is "op=" .
-
-instance proof
-qed(transfer, rule)
-
-end
-
-
 hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
   replace default map_entry map_default tabulate bulkload map
 
 end
+

--- a/src/HOL/Library/Multiset.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -5,7 +5,7 @@
 header {* (Finite) multisets *}
 
 theory Multiset
-imports Main DAList
+imports Main DAList (* FIXME too specific dependency for a generic theory *)
 begin
 
 subsection {* The type of multisets *}

--- a/src/HOL/Library/RBT_Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
@@ -73,7 +73,7 @@
 
 lemma equal_Mapping [code]:
   "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
-by (transfer fixing: t1 t2) (simp add: entries_lookup)
+  by (transfer fixing: t1 t2) (simp add: entries_lookup)
 
 lemma [code nbe]:
   "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"

--- a/src/HOL/ROOT	Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/ROOT	Fri Feb 15 11:47:34 2013 +0100
@@ -20,18 +20,25 @@
   description {* Classical Higher-order Logic -- batteries included *}
   theories
     Library
-    Sublist
+    (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order
-    Finite_Lattice
-    Code_Char
     Product_Lexorder
     Product_Order
+    Finite_Lattice
+    (*data refinements and dependent applications*)
+    AList_Mapping
+    Code_Binary_Nat
+    Code_Char
     (* Code_Prolog  FIXME cf. 76965c356d2a *)
     Code_Real_Approx_By_Float
     Code_Target_Numeral
-    IArray
+    DAList
+    RBT_Mapping
+    RBT_Set
+    (*legacy tools*)
     Refute
+    Old_Recdef
   theories [condition = ISABELLE_FULL_TEST]
     Sum_of_Squares_Remote
   files "document/root.bib" "document/root.tex"
@@ -148,7 +155,7 @@
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
-  theories Generate Generate_Pretty RBT_Set_Test
+  theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*