src/HOL/Lifting_Sum.thy
author kuncar
Thu, 10 Apr 2014 17:48:32 +0200
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 56526 58ac520db7ae
permissions -rw-r--r--
simplify and fix theories thanks to 356a5efdb278

(*  Title:      HOL/Lifting_Sum.thy
    Author:     Brian Huffman and Ondrej Kuncar
*)

header {* Setup for Lifting/Transfer for the sum type *}

theory Lifting_Sum
imports Lifting Basic_BNFs
begin

subsection {* Transfer rules for the Transfer package *}

context
begin
interpretation lifting_syntax .

lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
  unfolding rel_fun_def by simp

lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
  unfolding rel_fun_def by simp

lemma case_sum_transfer [transfer_rule]:
  "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)

end

end