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
kuncar@53012
     1
(*  Title:      HOL/Lifting_Sum.thy
kuncar@53012
     2
    Author:     Brian Huffman and Ondrej Kuncar
kuncar@53012
     3
*)
kuncar@53012
     4
kuncar@53012
     5
header {* Setup for Lifting/Transfer for the sum type *}
kuncar@53012
     6
kuncar@53012
     7
theory Lifting_Sum
blanchet@55083
     8
imports Lifting Basic_BNFs
kuncar@53012
     9
begin
kuncar@53012
    10
kuncar@56526
    11
(* The following lemma can be deleted when sum is added to FP sugar *)
kuncar@56526
    12
lemma sum_pred_inject [simp]:
kuncar@56526
    13
  "pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
kuncar@56526
    14
  unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
kuncar@56526
    15
kuncar@53012
    16
subsection {* Transfer rules for the Transfer package *}
kuncar@53012
    17
kuncar@53012
    18
context
kuncar@53012
    19
begin
kuncar@53012
    20
interpretation lifting_syntax .
kuncar@53012
    21
blanchet@55943
    22
lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
blanchet@55945
    23
  unfolding rel_fun_def by simp
kuncar@53012
    24
blanchet@55943
    25
lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
blanchet@55945
    26
  unfolding rel_fun_def by simp
kuncar@53012
    27
blanchet@55414
    28
lemma case_sum_transfer [transfer_rule]:
blanchet@55943
    29
  "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
blanchet@55945
    30
  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
kuncar@53012
    31
kuncar@53012
    32
end
kuncar@53012
    33
kuncar@53012
    34
end