src/HOL/Library/Quotient_Sum.thy
changeset 51956 a4d81cdebf8b
parent 51377 7da251a6c16e
child 51994 82cc2aeb7d13
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Mon May 13 12:13:24 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Mon May 13 13:59:04 2013 +0200
     1.3 @@ -24,6 +24,16 @@
     1.4      | _ \<Rightarrow> False)"
     1.5    by (cases x) (cases y, simp_all)+
     1.6  
     1.7 +fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     1.8 +where
     1.9 +  "sum_pred P1 P2 (Inl a) = P1 a"
    1.10 +| "sum_pred P1 P2 (Inr a) = P2 a"
    1.11 +
    1.12 +lemma sum_pred_unfold:
    1.13 +  "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x
    1.14 +    | Inr x \<Rightarrow> P2 x)"
    1.15 +by (cases x) simp_all
    1.16 +
    1.17  lemma sum_rel_map1:
    1.18    "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    1.19    by (simp add: sum_rel_unfold split: sum.split)
    1.20 @@ -56,6 +66,13 @@
    1.21    "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
    1.22  by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split)
    1.23  
    1.24 +lemma Domainp_sum[relator_domain]:
    1.25 +  assumes "Domainp R1 = P1"
    1.26 +  assumes "Domainp R2 = P2"
    1.27 +  shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)"
    1.28 +using assms
    1.29 +by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
    1.30 +
    1.31  lemma sum_reflp[reflexivity_rule]:
    1.32    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    1.33    unfolding reflp_def split_sum_all sum_rel.simps by fast
    1.34 @@ -116,21 +133,9 @@
    1.35    using assms unfolding Quotient_alt_def
    1.36    by (simp add: split_sum_all)
    1.37  
    1.38 -fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
    1.39 -where
    1.40 -  "sum_pred R1 R2 (Inl a) = R1 a"
    1.41 -| "sum_pred R1 R2 (Inr a) = R2 a"
    1.42 -
    1.43  lemma sum_invariant_commute [invariant_commute]: 
    1.44    "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    1.45 -  apply (simp add: fun_eq_iff Lifting.invariant_def)
    1.46 -  apply (intro allI) 
    1.47 -  apply (case_tac x rule: sum.exhaust)
    1.48 -  apply (case_tac xa rule: sum.exhaust)
    1.49 -  apply auto[2]
    1.50 -  apply (case_tac xa rule: sum.exhaust)
    1.51 -  apply auto
    1.52 -done
    1.53 +  by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split)
    1.54  
    1.55  subsection {* Rules for quotient package *}
    1.56