src/HOL/Codegenerator_Test/RBT_Set_Test.thy
changeset 50996 51ad7b4ac096
parent 49948 744934b818c7
child 51116 0dac0158b8d4
     1.1 --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Jan 25 16:45:09 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Tue Jan 15 12:13:27 2013 +0100
     1.3 @@ -46,6 +46,27 @@
     1.4    or implemented for RBT trees.
     1.5  *)
     1.6  
     1.7 -export_code _ checking SML OCaml? Haskell? Scala?
     1.8 +export_code _ checking SML OCaml? Haskell?
     1.9 +
    1.10 +(* Extra setup to make Scala happy *)
    1.11 +(* If the compilation fails with an error "ambiguous implicit values",
    1.12 +   read \<section>7.1 in the Code Generation Manual *)
    1.13 +
    1.14 +class ccpo_linorder = ccpo + linorder
    1.15 +
    1.16 +lemma [code]:
    1.17 +  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    1.18 +    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    1.19 +unfolding admissible_def by blast
    1.20 +
    1.21 +lemma [code]:
    1.22 +  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    1.23 +unfolding gfp_def by blast
    1.24 +
    1.25 +lemma [code]:
    1.26 +  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    1.27 +unfolding lfp_def by blast
    1.28 +
    1.29 +export_code _ checking Scala?
    1.30  
    1.31  end