--- a/src/HOL/Library/Quotient_Product.thy Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Tue Aug 13 15:59:22 2013 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Library/Quotient_Product.thy
- Author: Cezary Kaliszyk, Christian Urban and Brian Huffman
+ Author: Cezary Kaliszyk and Christian Urban
*)
header {* Quotient infrastructure for the product type *}
@@ -8,137 +8,22 @@
imports Main Quotient_Syntax
begin
-subsection {* Relator for product type *}
-
-definition
- prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
-where
- "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-
-definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
-
-lemma prod_rel_apply [simp]:
- "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
- by (simp add: prod_rel_def)
-
-lemma prod_pred_apply [simp]:
- "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
- by (simp add: prod_pred_def)
+subsection {* Rules for the Quotient package *}
lemma map_pair_id [id_simps]:
shows "map_pair id id = id"
by (simp add: fun_eq_iff)
-lemma prod_rel_eq [id_simps, relator_eq]:
+lemma prod_rel_eq [id_simps]:
shows "prod_rel (op =) (op =) = (op =)"
by (simp add: fun_eq_iff)
-lemma prod_rel_mono[relator_mono]:
- assumes "A \<le> C"
- assumes "B \<le> D"
- shows "(prod_rel A B) \<le> (prod_rel C D)"
-using assms by (auto simp: prod_rel_def)
-
-lemma prod_rel_OO[relator_distr]:
- "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
-by (rule ext)+ (auto simp: prod_rel_def OO_def)
-
-lemma Domainp_prod[relator_domain]:
- assumes "Domainp T1 = P1"
- assumes "Domainp T2 = P2"
- shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
-using assms unfolding prod_rel_def prod_pred_def by blast
-
-lemma reflp_prod_rel [reflexivity_rule]:
- assumes "reflp R1"
- assumes "reflp R2"
- shows "reflp (prod_rel R1 R2)"
-using assms by (auto intro!: reflpI elim: reflpE)
-
-lemma left_total_prod_rel [reflexivity_rule]:
- assumes "left_total R1"
- assumes "left_total R2"
- shows "left_total (prod_rel R1 R2)"
- using assms unfolding left_total_def prod_rel_def by auto
-
-lemma left_unique_prod_rel [reflexivity_rule]:
- assumes "left_unique R1" and "left_unique R2"
- shows "left_unique (prod_rel R1 R2)"
- using assms unfolding left_unique_def prod_rel_def by auto
-
lemma prod_equivp [quot_equiv]:
assumes "equivp R1"
assumes "equivp R2"
shows "equivp (prod_rel R1 R2)"
using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
-lemma right_total_prod_rel [transfer_rule]:
- assumes "right_total R1" and "right_total R2"
- shows "right_total (prod_rel R1 R2)"
- using assms unfolding right_total_def prod_rel_def by auto
-
-lemma right_unique_prod_rel [transfer_rule]:
- assumes "right_unique R1" and "right_unique R2"
- shows "right_unique (prod_rel R1 R2)"
- using assms unfolding right_unique_def prod_rel_def by auto
-
-lemma bi_total_prod_rel [transfer_rule]:
- assumes "bi_total R1" and "bi_total R2"
- shows "bi_total (prod_rel R1 R2)"
- using assms unfolding bi_total_def prod_rel_def by auto
-
-lemma bi_unique_prod_rel [transfer_rule]:
- assumes "bi_unique R1" and "bi_unique R2"
- shows "bi_unique (prod_rel R1 R2)"
- using assms unfolding bi_unique_def prod_rel_def by auto
-
-subsection {* Transfer rules for transfer package *}
-
-lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair"
- unfolding fun_rel_def prod_rel_def by simp
-
-lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst"
- unfolding fun_rel_def prod_rel_def by simp
-
-lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd"
- unfolding fun_rel_def prod_rel_def by simp
-
-lemma prod_case_transfer [transfer_rule]:
- "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case"
- unfolding fun_rel_def prod_rel_def by simp
-
-lemma curry_transfer [transfer_rule]:
- "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
- unfolding curry_def by transfer_prover
-
-lemma map_pair_transfer [transfer_rule]:
- "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
- map_pair map_pair"
- unfolding map_pair_def [abs_def] by transfer_prover
-
-lemma prod_rel_transfer [transfer_rule]:
- "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
- prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel"
- unfolding fun_rel_def by auto
-
-subsection {* Setup for lifting package *}
-
-lemma Quotient_prod[quot_map]:
- assumes "Quotient R1 Abs1 Rep1 T1"
- assumes "Quotient R2 Abs2 Rep2 T2"
- shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
- (map_pair Rep1 Rep2) (prod_rel T1 T2)"
- using assms unfolding Quotient_alt_def by auto
-
-lemma prod_invariant_commute [invariant_commute]:
- "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
- apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def)
- apply blast
-done
-
-subsection {* Rules for quotient package *}
-
lemma prod_quotient [quot_thm]:
assumes "Quotient3 R1 Abs1 Rep1"
assumes "Quotient3 R2 Abs2 Rep2"