equal
deleted
inserted
replaced
8 imports Lifting Basic_BNFs |
8 imports Lifting Basic_BNFs |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Relator and predicator properties *} |
11 subsection {* Relator and predicator properties *} |
12 |
12 |
13 abbreviation (input) "sum_pred \<equiv> sum_case" |
13 abbreviation (input) "sum_pred \<equiv> case_sum" |
14 |
14 |
15 lemmas sum_rel_eq[relator_eq] = sum.rel_eq |
15 lemmas sum_rel_eq[relator_eq] = sum.rel_eq |
16 lemmas sum_rel_mono[relator_mono] = sum.rel_mono |
16 lemmas sum_rel_mono[relator_mono] = sum.rel_mono |
17 |
17 |
18 lemma sum_rel_OO[relator_distr]: |
18 lemma sum_rel_OO[relator_distr]: |
78 unfolding fun_rel_def by simp |
78 unfolding fun_rel_def by simp |
79 |
79 |
80 lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" |
80 lemma Inr_transfer [transfer_rule]: "(B ===> sum_rel A B) Inr Inr" |
81 unfolding fun_rel_def by simp |
81 unfolding fun_rel_def by simp |
82 |
82 |
83 lemma sum_case_transfer [transfer_rule]: |
83 lemma case_sum_transfer [transfer_rule]: |
84 "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) sum_case sum_case" |
84 "((A ===> C) ===> (B ===> C) ===> sum_rel A B ===> C) case_sum case_sum" |
85 unfolding fun_rel_def sum_rel_def by (simp split: sum.split) |
85 unfolding fun_rel_def sum_rel_def by (simp split: sum.split) |
86 |
86 |
87 end |
87 end |
88 |
88 |
89 end |
89 end |