3 *) |
3 *) |
4 |
4 |
5 header {* Setup for Lifting/Transfer for the sum type *} |
5 header {* Setup for Lifting/Transfer for the sum type *} |
6 |
6 |
7 theory Lifting_Sum |
7 theory Lifting_Sum |
8 imports Lifting FunDef |
8 imports Lifting |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Relator and predicator properties *} |
11 subsection {* Relator and predicator properties *} |
12 |
12 |
13 fun |
13 definition |
14 sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" |
14 sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool" |
15 where |
15 where |
|
16 "sum_rel R1 R2 x y = |
|
17 (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y |
|
18 | (Inr x, Inr y) \<Rightarrow> R2 x y |
|
19 | _ \<Rightarrow> False)" |
|
20 |
|
21 lemma sum_rel_simps[simp]: |
16 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
22 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
17 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
23 "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
18 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
24 "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
19 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
25 "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
|
26 unfolding sum_rel_def by simp_all |
20 |
27 |
21 lemma sum_rel_unfold: |
28 abbreviation (input) "sum_pred \<equiv> sum_case" |
22 "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y |
|
23 | (Inr x, Inr y) \<Rightarrow> R2 x y |
|
24 | _ \<Rightarrow> False)" |
|
25 by (cases x) (cases y, simp_all)+ |
|
26 |
|
27 fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool" |
|
28 where |
|
29 "sum_pred P1 P2 (Inl a) = P1 a" |
|
30 | "sum_pred P1 P2 (Inr a) = P2 a" |
|
31 |
|
32 lemma sum_pred_unfold: |
|
33 "sum_pred P1 P2 x = (case x of Inl x \<Rightarrow> P1 x |
|
34 | Inr x \<Rightarrow> P2 x)" |
|
35 by (cases x) simp_all |
|
36 |
29 |
37 lemma sum_rel_eq [relator_eq]: |
30 lemma sum_rel_eq [relator_eq]: |
38 "sum_rel (op =) (op =) = (op =)" |
31 "sum_rel (op =) (op =) = (op =)" |
39 by (simp add: sum_rel_unfold fun_eq_iff split: sum.split) |
32 by (simp add: sum_rel_def fun_eq_iff split: sum.split) |
40 |
33 |
41 lemma sum_rel_mono[relator_mono]: |
34 lemma sum_rel_mono[relator_mono]: |
42 assumes "A \<le> C" |
35 assumes "A \<le> C" |
43 assumes "B \<le> D" |
36 assumes "B \<le> D" |
44 shows "(sum_rel A B) \<le> (sum_rel C D)" |
37 shows "(sum_rel A B) \<le> (sum_rel C D)" |
45 using assms by (auto simp: sum_rel_unfold split: sum.splits) |
38 using assms by (auto simp: sum_rel_def split: sum.splits) |
46 |
39 |
47 lemma sum_rel_OO[relator_distr]: |
40 lemma sum_rel_OO[relator_distr]: |
48 "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" |
41 "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)" |
49 by (rule ext)+ (auto simp add: sum_rel_unfold OO_def split_sum_ex split: sum.split) |
42 by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split) |
50 |
43 |
51 lemma Domainp_sum[relator_domain]: |
44 lemma Domainp_sum[relator_domain]: |
52 assumes "Domainp R1 = P1" |
45 assumes "Domainp R1 = P1" |
53 assumes "Domainp R2 = P2" |
46 assumes "Domainp R2 = P2" |
54 shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" |
47 shows "Domainp (sum_rel R1 R2) = (sum_pred P1 P2)" |
55 using assms |
48 using assms |
56 by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split) |
49 by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split) |
57 |
50 |
58 lemma reflp_sum_rel[reflexivity_rule]: |
51 lemma reflp_sum_rel[reflexivity_rule]: |
59 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" |
52 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)" |
60 unfolding reflp_def split_sum_all sum_rel.simps by fast |
53 unfolding reflp_def split_sum_all sum_rel_simps by fast |
61 |
54 |
62 lemma left_total_sum_rel[reflexivity_rule]: |
55 lemma left_total_sum_rel[reflexivity_rule]: |
63 "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)" |
56 "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)" |
64 using assms unfolding left_total_def split_sum_all split_sum_ex by simp |
57 using assms unfolding left_total_def split_sum_all split_sum_ex by simp |
65 |
58 |
83 "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)" |
76 "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (sum_rel R1 R2)" |
84 using assms unfolding bi_unique_def split_sum_all by simp |
77 using assms unfolding bi_unique_def split_sum_all by simp |
85 |
78 |
86 lemma sum_invariant_commute [invariant_commute]: |
79 lemma sum_invariant_commute [invariant_commute]: |
87 "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" |
80 "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)" |
88 by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_unfold sum_pred_unfold split: sum.split) |
81 by (auto simp add: fun_eq_iff Lifting.invariant_def sum_rel_def split: sum.split) |
89 |
82 |
90 subsection {* Quotient theorem for the Lifting package *} |
83 subsection {* Quotient theorem for the Lifting package *} |
91 |
84 |
92 lemma Quotient_sum[quot_map]: |
85 lemma Quotient_sum[quot_map]: |
93 assumes "Quotient R1 Abs1 Rep1 T1" |
86 assumes "Quotient R1 Abs1 Rep1 T1" |