src/HOL/Lifting_Sum.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 56526 58ac520db7ae
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      HOL/Lifting_Sum.thy
     2     Author:     Brian Huffman and Ondrej Kuncar
     3 *)
     4 
     5 section {* 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