78 context |
78 context |
79 begin |
79 begin |
80 interpretation lifting_syntax . |
80 interpretation lifting_syntax . |
81 |
81 |
82 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" |
82 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair" |
83 unfolding fun_rel_def rel_prod_def by simp |
83 unfolding rel_fun_def rel_prod_def by simp |
84 |
84 |
85 lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" |
85 lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst" |
86 unfolding fun_rel_def rel_prod_def by simp |
86 unfolding rel_fun_def rel_prod_def by simp |
87 |
87 |
88 lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" |
88 lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd" |
89 unfolding fun_rel_def rel_prod_def by simp |
89 unfolding rel_fun_def rel_prod_def by simp |
90 |
90 |
91 lemma case_prod_transfer [transfer_rule]: |
91 lemma case_prod_transfer [transfer_rule]: |
92 "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" |
92 "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod" |
93 unfolding fun_rel_def rel_prod_def by simp |
93 unfolding rel_fun_def rel_prod_def by simp |
94 |
94 |
95 lemma curry_transfer [transfer_rule]: |
95 lemma curry_transfer [transfer_rule]: |
96 "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
96 "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" |
97 unfolding curry_def by transfer_prover |
97 unfolding curry_def by transfer_prover |
98 |
98 |
102 unfolding map_prod_def [abs_def] by transfer_prover |
102 unfolding map_prod_def [abs_def] by transfer_prover |
103 |
103 |
104 lemma rel_prod_transfer [transfer_rule]: |
104 lemma rel_prod_transfer [transfer_rule]: |
105 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
105 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
106 rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
106 rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod" |
107 unfolding fun_rel_def by auto |
107 unfolding rel_fun_def by auto |
108 |
108 |
109 end |
109 end |
110 |
110 |
111 end |
111 end |
112 |
112 |