equal
deleted
inserted
replaced
5 Copyright 2015, 2016 |
5 Copyright 2015, 2016 |
6 |
6 |
7 Generalized corecursor sugar ("corec" and friends). |
7 Generalized corecursor sugar ("corec" and friends). |
8 *) |
8 *) |
9 |
9 |
10 chapter {* Generalized Corecursor Sugar (corec and friends) *} |
10 section \<open>Generalized Corecursor Sugar (corec and friends)\<close> |
11 |
11 |
12 theory BNF_Corec |
12 theory BNF_Corec |
13 imports Main |
13 imports Main |
14 keywords |
14 keywords |
15 "corec" :: thy_decl and |
15 "corec" :: thy_decl and |
59 |
59 |
60 lemma if_distrib_fun: "(if c then f else g) x = (if c then f x else g x)" |
60 lemma if_distrib_fun: "(if c then f else g) x = (if c then f x else g x)" |
61 by simp |
61 by simp |
62 |
62 |
63 |
63 |
64 section \<open>Coinduction\<close> |
64 subsection \<open>Coinduction\<close> |
65 |
65 |
66 lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)" |
66 lemma eq_comp_compI: "a o b = f o x \<Longrightarrow> x o c = id \<Longrightarrow> f = a o (b o c)" |
67 unfolding fun_eq_iff by simp |
67 unfolding fun_eq_iff by simp |
68 |
68 |
69 lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \<le> inf a b \<Longrightarrow> a \<le> b" |
69 lemma self_bounded_weaken_left: "(a :: 'a :: semilattice_inf) \<le> inf a b \<Longrightarrow> a \<le> b" |