equal
deleted
inserted
replaced
68 context |
68 context |
69 begin |
69 begin |
70 interpretation lifting_syntax . |
70 interpretation lifting_syntax . |
71 |
71 |
72 lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" |
72 lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl" |
73 unfolding fun_rel_def by simp |
73 unfolding rel_fun_def by simp |
74 |
74 |
75 lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" |
75 lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr" |
76 unfolding fun_rel_def by simp |
76 unfolding rel_fun_def by simp |
77 |
77 |
78 lemma case_sum_transfer [transfer_rule]: |
78 lemma case_sum_transfer [transfer_rule]: |
79 "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" |
79 "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum" |
80 unfolding fun_rel_def rel_sum_def by (simp split: sum.split) |
80 unfolding rel_fun_def rel_sum_def by (simp split: sum.split) |
81 |
81 |
82 end |
82 end |
83 |
83 |
84 end |
84 end |