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.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
```