# HG changeset patch
# User kuncar
# Date 1358248407 -3600
# Node ID 51ad7b4ac0967f44a2df503ce656207749f8a190
# Parent  3371f5ee4aceb05136d7afefa27e248fe7837009
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual

diff -r 3371f5ee4ace -r 51ad7b4ac096 src/HOL/Codegenerator_Test/RBT_Set_Test.thy
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Jan 25 16:45:09 2013 +0100
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Tue Jan 15 12:13:27 2013 +0100
@@ -46,6 +46,27 @@
   or implemented for RBT trees.
 *)
 
-export_code _ checking SML OCaml? Haskell? Scala?
+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
diff -r 3371f5ee4ace -r 51ad7b4ac096 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Fri Jan 25 16:45:09 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Tue Jan 15 12:13:27 2013 +0100
@@ -63,8 +63,6 @@
 lemma [code, code del]:
   "Bex = Bex" ..
 
-term can_select
-
 lemma [code, code del]:
   "can_select = can_select" ..
 
@@ -526,6 +524,8 @@
 
 code_datatype Set Coset
 
+declare set.simps[code]
+
 lemma empty_Set [code]:
   "Set.empty = Set RBT.empty"
 by (auto simp: Set_def)