isabelle: src/HOL/Library/Quotient_Product.thy@9caab698dbe4 (annotated)

47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	1	(* Title: HOL/Library/Quotient3_Product.thy
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	2	Author: Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	3	*)
35788 f1deaca15ca3 observe standard header format; wenzelm parents: 35222 diff changeset	4
f1deaca15ca3 observe standard header format; wenzelm parents: 35222 diff changeset	5	header {* Quotient infrastructure for the product type *}
f1deaca15ca3 observe standard header format; wenzelm parents: 35222 diff changeset	6
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	theory Quotient_Product
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	8	imports Main Quotient_Syntax
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	9	begin
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	10
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	11	definition
40541 7850b4cc1507 re-generalized type of prod_rel (accident from 2989f9f3aa10) haftmann parents: 40465 diff changeset	12	prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	13	where
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	14	"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	15
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	16	lemma prod_rel_apply [simp]:
2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	17	"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	18	by (simp add: prod_rel_def)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	19
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	20	lemma map_pair_id [id_simps]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	21	shows "map_pair id id = id"
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	22	by (simp add: fun_eq_iff)
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	23
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	24	lemma prod_rel_eq [id_simps]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	25	shows "prod_rel (op =) (op =) = (op =)"
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	26	by (simp add: fun_eq_iff)
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	27
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	28	lemma prod_equivp [quot_equiv]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	29	assumes "equivp R1"
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	30	assumes "equivp R2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	31	shows "equivp (prod_rel R1 R2)"
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	32	using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	33
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	34	lemma prod_quotient [quot_thm]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	35	assumes "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	36	assumes "Quotient3 R2 Abs2 Rep2"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	37	shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	38	apply (rule Quotient3I)
41372 551eb49a6e91 tuned type_lifting declarations haftmann parents: 40820 diff changeset	39	apply (simp add: map_pair.compositionality comp_def map_pair.identity
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	40	Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	41	apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	42	using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	43	apply (auto simp add: split_paired_all)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	44	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	45
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	46	declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
47094 1a7ad2601cb5 store the relational theorem for every relator kuncar parents: 45802 diff changeset	47
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	48	lemma Pair_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	49	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	50	assumes q2: "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	51	shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	52	by (auto simp add: prod_rel_def)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	53
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	54	lemma Pair_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	55	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	56	assumes q2: "Quotient3 R2 Abs2 Rep2"
40607 30d512bf47a7 map_pair replaces prod_fun haftmann parents: 40541 diff changeset	57	shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
39302 d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI nipkow parents: 39198 diff changeset	58	apply(simp add: fun_eq_iff)
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	59	apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	60	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	62	lemma fst_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	63	assumes "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	64	assumes "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	shows "(prod_rel R1 R2 ===> R1) fst fst"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	66	by auto
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	67
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	68	lemma fst_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	69	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	70	assumes q2: "Quotient3 R2 Abs2 Rep2"
40607 30d512bf47a7 map_pair replaces prod_fun haftmann parents: 40541 diff changeset	71	shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	72	by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	74	lemma snd_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	75	assumes "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	76	assumes "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77	shows "(prod_rel R1 R2 ===> R2) snd snd"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	78	by auto
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	79
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	80	lemma snd_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	81	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	82	assumes q2: "Quotient3 R2 Abs2 Rep2"
40607 30d512bf47a7 map_pair replaces prod_fun haftmann parents: 40541 diff changeset	83	shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	84	by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	85
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	86	lemma split_rsp [quot_respect]:
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	87	shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
47301 ca743eafa1dd tuned proof in order to avoid warning message Christian Urban <urbanc@in.tum.de> parents: 47094 diff changeset	88	unfolding prod_rel_def fun_rel_def
ca743eafa1dd tuned proof in order to avoid warning message Christian Urban <urbanc@in.tum.de> parents: 47094 diff changeset	89	by auto
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	90
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40607 diff changeset	91	lemma split_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	92	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	93	and q2: "Quotient3 R2 Abs2 Rep2"
40607 30d512bf47a7 map_pair replaces prod_fun haftmann parents: 40541 diff changeset	94	shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	95	by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	96
36695 b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	97	lemma [quot_respect]:
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	98	shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	99	prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	100	by (auto simp add: fun_rel_def)
36695 b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	101
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	102	lemma [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	103	assumes q1: "Quotient3 R1 abs1 rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	104	and q2: "Quotient3 R2 abs2 rep2"
36695 b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	105	shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
40607 30d512bf47a7 map_pair replaces prod_fun haftmann parents: 40541 diff changeset	106	map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47301 diff changeset	107	by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
36695 b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	108
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	109	lemma [quot_preserve]:
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	110	shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	111	(l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	112	by simp
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	113
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	114	declare Pair_eq[quot_preserve]
b434506fb0d4 respectfullness and preservation of prod_rel Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35788 diff changeset	115
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	116	end

author	kuncar
	Tue, 03 Apr 2012 16:26:48 +0200
changeset 47308	9caab698dbe4
parent 47301	ca743eafa1dd
child 47455	26315a545e26
permissions	-rw-r--r--