author | kuncar |
Fri, 23 Mar 2012 14:20:09 +0100 | |
changeset 47964 | 1a7ad2601cb5 |
parent 46673 | b16f976db515 |
child 48146 | ca743eafa1dd |
permissions | -rw-r--r-- |
wenzelm@35788 | 1 |
(* Title: HOL/Library/Quotient_Product.thy |
kaliszyk@35222 | 2 |
Author: Cezary Kaliszyk and Christian Urban |
kaliszyk@35222 | 3 |
*) |
wenzelm@35788 | 4 |
|
wenzelm@35788 | 5 |
header {* Quotient infrastructure for the product type *} |
wenzelm@35788 | 6 |
|
kaliszyk@35222 | 7 |
theory Quotient_Product |
kaliszyk@35222 | 8 |
imports Main Quotient_Syntax |
kaliszyk@35222 | 9 |
begin |
kaliszyk@35222 | 10 |
|
haftmann@40698 | 11 |
definition |
haftmann@40784 | 12 |
prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" |
kaliszyk@35222 | 13 |
where |
kaliszyk@35222 | 14 |
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
kaliszyk@35222 | 15 |
|
haftmann@40698 | 16 |
lemma prod_rel_apply [simp]: |
haftmann@40698 | 17 |
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d" |
haftmann@40698 | 18 |
by (simp add: prod_rel_def) |
kaliszyk@35222 | 19 |
|
haftmann@41068 | 20 |
lemma map_pair_id [id_simps]: |
haftmann@41068 | 21 |
shows "map_pair id id = id" |
haftmann@41068 | 22 |
by (simp add: fun_eq_iff) |
haftmann@41068 | 23 |
|
haftmann@41068 | 24 |
lemma prod_rel_eq [id_simps]: |
haftmann@41068 | 25 |
shows "prod_rel (op =) (op =) = (op =)" |
haftmann@41068 | 26 |
by (simp add: fun_eq_iff) |
haftmann@41068 | 27 |
|
haftmann@41068 | 28 |
lemma prod_equivp [quot_equiv]: |
haftmann@41068 | 29 |
assumes "equivp R1" |
haftmann@41068 | 30 |
assumes "equivp R2" |
kaliszyk@35222 | 31 |
shows "equivp (prod_rel R1 R2)" |
haftmann@41068 | 32 |
using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) |
haftmann@41068 | 33 |
|
haftmann@41068 | 34 |
lemma prod_quotient [quot_thm]: |
haftmann@41068 | 35 |
assumes "Quotient R1 Abs1 Rep1" |
haftmann@41068 | 36 |
assumes "Quotient R2 Abs2 Rep2" |
haftmann@41068 | 37 |
shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" |
haftmann@41068 | 38 |
apply (rule QuotientI) |
haftmann@41620 | 39 |
apply (simp add: map_pair.compositionality comp_def map_pair.identity |
haftmann@41068 | 40 |
Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)]) |
haftmann@41068 | 41 |
apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)]) |
haftmann@41068 | 42 |
using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)] |
haftmann@41068 | 43 |
apply (auto simp add: split_paired_all) |
kaliszyk@35222 | 44 |
done |
kaliszyk@35222 | 45 |
|
kuncar@47964 | 46 |
declare [[map prod = (prod_rel, prod_quotient)]] |
kuncar@47964 | 47 |
|
haftmann@41068 | 48 |
lemma Pair_rsp [quot_respect]: |
kaliszyk@35222 | 49 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 50 |
assumes q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 51 |
shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
haftmann@40698 | 52 |
by (auto simp add: prod_rel_def) |
kaliszyk@35222 | 53 |
|
haftmann@41068 | 54 |
lemma Pair_prs [quot_preserve]: |
kaliszyk@35222 | 55 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 56 |
assumes q2: "Quotient R2 Abs2 Rep2" |
haftmann@40855 | 57 |
shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" |
nipkow@39535 | 58 |
apply(simp add: fun_eq_iff) |
kaliszyk@35222 | 59 |
apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
kaliszyk@35222 | 60 |
done |
kaliszyk@35222 | 61 |
|
haftmann@41068 | 62 |
lemma fst_rsp [quot_respect]: |
kaliszyk@35222 | 63 |
assumes "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 64 |
assumes "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 65 |
shows "(prod_rel R1 R2 ===> R1) fst fst" |
haftmann@40698 | 66 |
by auto |
kaliszyk@35222 | 67 |
|
haftmann@41068 | 68 |
lemma fst_prs [quot_preserve]: |
kaliszyk@35222 | 69 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 70 |
assumes q2: "Quotient R2 Abs2 Rep2" |
haftmann@40855 | 71 |
shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst" |
haftmann@40698 | 72 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1]) |
kaliszyk@35222 | 73 |
|
haftmann@41068 | 74 |
lemma snd_rsp [quot_respect]: |
kaliszyk@35222 | 75 |
assumes "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 76 |
assumes "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 77 |
shows "(prod_rel R1 R2 ===> R2) snd snd" |
haftmann@40698 | 78 |
by auto |
kaliszyk@35222 | 79 |
|
haftmann@41068 | 80 |
lemma snd_prs [quot_preserve]: |
kaliszyk@35222 | 81 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 82 |
assumes q2: "Quotient R2 Abs2 Rep2" |
haftmann@40855 | 83 |
shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" |
haftmann@40698 | 84 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF q2]) |
kaliszyk@35222 | 85 |
|
haftmann@41068 | 86 |
lemma split_rsp [quot_respect]: |
kaliszyk@35222 | 87 |
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
haftmann@40698 | 88 |
by (auto intro!: fun_relI elim!: fun_relE) |
kaliszyk@35222 | 89 |
|
haftmann@41068 | 90 |
lemma split_prs [quot_preserve]: |
kaliszyk@35222 | 91 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 92 |
and q2: "Quotient R2 Abs2 Rep2" |
haftmann@40855 | 93 |
shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" |
nipkow@39535 | 94 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
kaliszyk@35222 | 95 |
|
kaliszyk@36680 | 96 |
lemma [quot_respect]: |
kaliszyk@36680 | 97 |
shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> |
kaliszyk@36680 | 98 |
prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" |
haftmann@40698 | 99 |
by (auto simp add: fun_rel_def) |
kaliszyk@36680 | 100 |
|
kaliszyk@36680 | 101 |
lemma [quot_preserve]: |
kaliszyk@36680 | 102 |
assumes q1: "Quotient R1 abs1 rep1" |
kaliszyk@36680 | 103 |
and q2: "Quotient R2 abs2 rep2" |
kaliszyk@36680 | 104 |
shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> |
haftmann@40855 | 105 |
map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel" |
nipkow@39535 | 106 |
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
kaliszyk@36680 | 107 |
|
kaliszyk@36680 | 108 |
lemma [quot_preserve]: |
kaliszyk@36680 | 109 |
shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) |
kaliszyk@36680 | 110 |
(l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))" |
kaliszyk@36680 | 111 |
by simp |
kaliszyk@36680 | 112 |
|
kaliszyk@36680 | 113 |
declare Pair_eq[quot_preserve] |
kaliszyk@36680 | 114 |
|
kaliszyk@35222 | 115 |
end |