equal
deleted
inserted
replaced
51 |
51 |
52 (* Extra setup to make Scala happy *) |
52 (* Extra setup to make Scala happy *) |
53 (* If the compilation fails with an error "ambiguous implicit values", |
53 (* If the compilation fails with an error "ambiguous implicit values", |
54 read \<section>7.1 in the Code Generation Manual *) |
54 read \<section>7.1 in the Code Generation Manual *) |
55 |
55 |
56 class ccpo_linorder = ccpo + linorder |
|
57 |
|
58 lemma [code]: |
|
59 "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = |
|
60 (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))" |
|
61 unfolding admissible_def by blast |
|
62 |
|
63 lemma [code]: |
56 lemma [code]: |
64 "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}" |
57 "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}" |
65 unfolding gfp_def by blast |
58 unfolding gfp_def by blast |
66 |
59 |
67 lemma [code]: |
60 lemma [code]: |