src/HOL/Lifting_Sum.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 56526 58ac520db7ae child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
```     1 (*  Title:      HOL/Lifting_Sum.thy
```
```     2     Author:     Brian Huffman and Ondrej Kuncar
```
```     3 *)
```
```     4
```
```     5 header {* Setup for Lifting/Transfer for the sum type *}
```
```     6
```
```     7 theory Lifting_Sum
```
```     8 imports Lifting Basic_BNFs
```
```     9 begin
```
```    10
```
```    11 (* The following lemma can be deleted when sum is added to FP sugar *)
```
```    12 lemma sum_pred_inject [simp]:
```
```    13   "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
```
```    14   unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
```
```    15
```
```    16 subsection {* Transfer rules for the Transfer package *}
```
```    17
```
```    18 context
```
```    19 begin
```
```    20 interpretation lifting_syntax .
```
```    21
```
```    22 lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
```
```    23   unfolding rel_fun_def by simp
```
```    24
```
```    25 lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
```
```    26   unfolding rel_fun_def by simp
```
```    27
```
```    28 lemma case_sum_transfer [transfer_rule]:
```
```    29   "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
```
```    30   unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
```
```    31
```
```    32 end
```
```    33
```
```    34 end
```