1 (* Title: HOL/Lifting_Product.thy
2 Author: Brian Huffman and Ondrej Kuncar
5 header {* Setup for Lifting/Transfer for the product type *}
8 imports Lifting Basic_BNFs
11 subsection {* Relator and predicator properties *}
13 definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
14 where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
16 lemma prod_pred_apply [simp]:
17 "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
18 by (simp add: prod_pred_def)
20 lemma prod_rel_eq [relator_eq]:
21 shows "prod_rel (op =) (op =) = (op =)"
22 by (simp add: fun_eq_iff)
24 lemma prod_rel_mono[relator_mono]:
27 shows "(prod_rel A B) \<le> (prod_rel C D)"
28 using assms by (auto simp: prod_rel_def)
30 lemma prod_rel_OO[relator_distr]:
31 "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
32 by (rule ext)+ (auto simp: prod_rel_def OO_def)
34 lemma Domainp_prod[relator_domain]:
35 assumes "Domainp T1 = P1"
36 assumes "Domainp T2 = P2"
37 shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
38 using assms unfolding prod_rel_def prod_pred_def by blast
40 lemma reflp_prod_rel [reflexivity_rule]:
43 shows "reflp (prod_rel R1 R2)"
44 using assms by (auto intro!: reflpI elim: reflpE)
46 lemma left_total_prod_rel [reflexivity_rule]:
47 assumes "left_total R1"
48 assumes "left_total R2"
49 shows "left_total (prod_rel R1 R2)"
50 using assms unfolding left_total_def prod_rel_def by auto
52 lemma left_unique_prod_rel [reflexivity_rule]:
53 assumes "left_unique R1" and "left_unique R2"
54 shows "left_unique (prod_rel R1 R2)"
55 using assms unfolding left_unique_def prod_rel_def by auto
57 lemma right_total_prod_rel [transfer_rule]:
58 assumes "right_total R1" and "right_total R2"
59 shows "right_total (prod_rel R1 R2)"
60 using assms unfolding right_total_def prod_rel_def by auto
62 lemma right_unique_prod_rel [transfer_rule]:
63 assumes "right_unique R1" and "right_unique R2"
64 shows "right_unique (prod_rel R1 R2)"
65 using assms unfolding right_unique_def prod_rel_def by auto
67 lemma bi_total_prod_rel [transfer_rule]:
68 assumes "bi_total R1" and "bi_total R2"
69 shows "bi_total (prod_rel R1 R2)"
70 using assms unfolding bi_total_def prod_rel_def by auto
72 lemma bi_unique_prod_rel [transfer_rule]:
73 assumes "bi_unique R1" and "bi_unique R2"
74 shows "bi_unique (prod_rel R1 R2)"
75 using assms unfolding bi_unique_def prod_rel_def by auto
77 lemma prod_invariant_commute [invariant_commute]:
78 "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
79 by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast
81 subsection {* Quotient theorem for the Lifting package *}
83 lemma Quotient_prod[quot_map]:
84 assumes "Quotient R1 Abs1 Rep1 T1"
85 assumes "Quotient R2 Abs2 Rep2 T2"
86 shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
87 (map_pair Rep1 Rep2) (prod_rel T1 T2)"
88 using assms unfolding Quotient_alt_def by auto
90 subsection {* Transfer rules for the Transfer package *}
94 interpretation lifting_syntax .
96 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
97 unfolding fun_rel_def prod_rel_def by simp
99 lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
100 unfolding fun_rel_def prod_rel_def by simp
102 lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
103 unfolding fun_rel_def prod_rel_def by simp
105 lemma prod_case_transfer [transfer_rule]:
106 "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
107 unfolding fun_rel_def prod_rel_def by simp
109 lemma curry_transfer [transfer_rule]:
110 "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
111 unfolding curry_def by transfer_prover
113 lemma map_pair_transfer [transfer_rule]:
114 "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
116 unfolding map_pair_def [abs_def] by transfer_prover
118 lemma prod_rel_transfer [transfer_rule]:
119 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
120 prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
121 unfolding fun_rel_def by auto