src/HOL/Lifting_Sum.thy
changeset 55083 0a689157e3ce
parent 53026 e1a548c11845
child 55084 8ee9aabb2bca
     1.1 --- a/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -5,26 +5,11 @@
     1.4  header {* Setup for Lifting/Transfer for the sum type *}
     1.5  
     1.6  theory Lifting_Sum
     1.7 -imports Lifting
     1.8 +imports Lifting Basic_BNFs
     1.9  begin
    1.10  
    1.11  subsection {* Relator and predicator properties *}
    1.12  
    1.13 -definition
    1.14 -   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
    1.15 -where
    1.16 -   "sum_rel R1 R2 x y =
    1.17 -     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.18 -     | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.19 -     | _ \<Rightarrow> False)"
    1.20 -
    1.21 -lemma sum_rel_simps[simp]:
    1.22 -  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    1.23 -  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    1.24 -  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    1.25 -  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    1.26 -  unfolding sum_rel_def by simp_all
    1.27 -
    1.28  abbreviation (input) "sum_pred \<equiv> sum_case"
    1.29  
    1.30  lemma sum_rel_eq [relator_eq]: