kuncar@53012: (* Title: HOL/Lifting_Product.thy kuncar@53012: Author: Brian Huffman and Ondrej Kuncar kuncar@53012: *) kuncar@53012: kuncar@53012: header {* Setup for Lifting/Transfer for the product type *} kuncar@53012: kuncar@53012: theory Lifting_Product kuncar@53012: imports Lifting kuncar@53012: begin kuncar@53012: kuncar@53012: subsection {* Relator and predicator properties *} kuncar@53012: kuncar@53012: definition kuncar@53012: prod_rel :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ 'a \ 'c \ 'b \ 'd \ bool" kuncar@53012: where kuncar@53012: "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" kuncar@53012: kuncar@53012: definition prod_pred :: "('a \ bool) \ ('b \ bool) \ 'a \ 'b \ bool" kuncar@53012: where "prod_pred R1 R2 = (\(a, b). R1 a \ R2 b)" kuncar@53012: kuncar@53012: lemma prod_rel_apply [simp]: kuncar@53012: "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" kuncar@53012: by (simp add: prod_rel_def) kuncar@53012: kuncar@53012: lemma prod_pred_apply [simp]: kuncar@53012: "prod_pred P1 P2 (a, b) \ P1 a \ P2 b" kuncar@53012: by (simp add: prod_pred_def) kuncar@53012: kuncar@53012: lemma prod_rel_eq [relator_eq]: kuncar@53012: shows "prod_rel (op =) (op =) = (op =)" kuncar@53012: by (simp add: fun_eq_iff) kuncar@53012: kuncar@53012: lemma prod_rel_mono[relator_mono]: kuncar@53012: assumes "A \ C" kuncar@53012: assumes "B \ D" kuncar@53012: shows "(prod_rel A B) \ (prod_rel C D)" kuncar@53012: using assms by (auto simp: prod_rel_def) kuncar@53012: kuncar@53012: lemma prod_rel_OO[relator_distr]: kuncar@53012: "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)" kuncar@53012: by (rule ext)+ (auto simp: prod_rel_def OO_def) kuncar@53012: kuncar@53012: lemma Domainp_prod[relator_domain]: kuncar@53012: assumes "Domainp T1 = P1" kuncar@53012: assumes "Domainp T2 = P2" kuncar@53012: shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)" kuncar@53012: using assms unfolding prod_rel_def prod_pred_def by blast kuncar@53012: kuncar@53012: lemma reflp_prod_rel [reflexivity_rule]: kuncar@53012: assumes "reflp R1" kuncar@53012: assumes "reflp R2" kuncar@53012: shows "reflp (prod_rel R1 R2)" kuncar@53012: using assms by (auto intro!: reflpI elim: reflpE) kuncar@53012: kuncar@53012: lemma left_total_prod_rel [reflexivity_rule]: kuncar@53012: assumes "left_total R1" kuncar@53012: assumes "left_total R2" kuncar@53012: shows "left_total (prod_rel R1 R2)" kuncar@53012: using assms unfolding left_total_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma left_unique_prod_rel [reflexivity_rule]: kuncar@53012: assumes "left_unique R1" and "left_unique R2" kuncar@53012: shows "left_unique (prod_rel R1 R2)" kuncar@53012: using assms unfolding left_unique_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma right_total_prod_rel [transfer_rule]: kuncar@53012: assumes "right_total R1" and "right_total R2" kuncar@53012: shows "right_total (prod_rel R1 R2)" kuncar@53012: using assms unfolding right_total_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma right_unique_prod_rel [transfer_rule]: kuncar@53012: assumes "right_unique R1" and "right_unique R2" kuncar@53012: shows "right_unique (prod_rel R1 R2)" kuncar@53012: using assms unfolding right_unique_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma bi_total_prod_rel [transfer_rule]: kuncar@53012: assumes "bi_total R1" and "bi_total R2" kuncar@53012: shows "bi_total (prod_rel R1 R2)" kuncar@53012: using assms unfolding bi_total_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma bi_unique_prod_rel [transfer_rule]: kuncar@53012: assumes "bi_unique R1" and "bi_unique R2" kuncar@53012: shows "bi_unique (prod_rel R1 R2)" kuncar@53012: using assms unfolding bi_unique_def prod_rel_def by auto kuncar@53012: kuncar@53012: lemma prod_invariant_commute [invariant_commute]: kuncar@53012: "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)" kuncar@53012: by (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) blast kuncar@53012: kuncar@53012: subsection {* Quotient theorem for the Lifting package *} kuncar@53012: kuncar@53012: lemma Quotient_prod[quot_map]: kuncar@53012: assumes "Quotient R1 Abs1 Rep1 T1" kuncar@53012: assumes "Quotient R2 Abs2 Rep2 T2" kuncar@53012: shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) kuncar@53012: (map_pair Rep1 Rep2) (prod_rel T1 T2)" kuncar@53012: using assms unfolding Quotient_alt_def by auto kuncar@53012: kuncar@53012: subsection {* Transfer rules for the Transfer package *} kuncar@53012: kuncar@53012: context kuncar@53012: begin kuncar@53012: interpretation lifting_syntax . kuncar@53012: kuncar@53012: lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" kuncar@53012: unfolding fun_rel_def prod_rel_def by simp kuncar@53012: kuncar@53012: lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" kuncar@53012: unfolding fun_rel_def prod_rel_def by simp kuncar@53012: kuncar@53012: lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" kuncar@53012: unfolding fun_rel_def prod_rel_def by simp kuncar@53012: kuncar@53012: lemma prod_case_transfer [transfer_rule]: kuncar@53012: "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" kuncar@53012: unfolding fun_rel_def prod_rel_def by simp kuncar@53012: kuncar@53012: lemma curry_transfer [transfer_rule]: kuncar@53012: "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" kuncar@53012: unfolding curry_def by transfer_prover kuncar@53012: kuncar@53012: lemma map_pair_transfer [transfer_rule]: kuncar@53012: "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) kuncar@53012: map_pair map_pair" kuncar@53012: unfolding map_pair_def [abs_def] by transfer_prover kuncar@53012: kuncar@53012: lemma prod_rel_transfer [transfer_rule]: kuncar@53012: "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> kuncar@53012: prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" kuncar@53012: unfolding fun_rel_def by auto kuncar@53012: kuncar@53012: end kuncar@53012: kuncar@53012: end kuncar@53012: