isabelle: src/HOL/Library/Quotient_Sum.thy@df6133adb63f (annotated)

47455 26315a545e26 updated headers; wenzelm parents: 47308 diff changeset	1	(* Title: HOL/Library/Quotient_Sum.thy
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: 53010 diff changeset	2	Author: Cezary Kaliszyk and Christian Urban
35222 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: 35243 diff changeset	4
f1deaca15ca3 observe standard header format; wenzelm parents: 35243 diff changeset	5	header {* Quotient infrastructure for the sum type *}
f1deaca15ca3 observe standard header format; wenzelm parents: 35243 diff changeset	6
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	7	theory Quotient_Sum
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
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: 53010 diff changeset	11	subsection {* Rules for the Quotient package *}
51956 a4d81cdebf8b better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal kuncar parents: 51377 diff changeset	12
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	13	lemma sum_rel_map1:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	14	"sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	15	by (simp add: sum_rel_def split: sum.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	16
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	17	lemma sum_rel_map2:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	18	"sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	19	by (simp add: sum_rel_def split: sum.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	20
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	21	lemma sum_map_id [id_simps]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	22	"sum_map id id = id"
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	23	by (simp add: id_def sum_map.identity fun_eq_iff)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	24
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: 53010 diff changeset	25	lemma sum_rel_eq [id_simps]:
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	26	"sum_rel (op =) (op =) = (op =)"
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	27	by (simp add: sum_rel_def fun_eq_iff split: sum.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	28
55564 e81ee43ab290 delete or move now not necessary reflexivity rules due to 1726f46d2aa8 kuncar parents: 53026 diff changeset	29	lemma reflp_sum_rel:
e81ee43ab290 delete or move now not necessary reflexivity rules due to 1726f46d2aa8 kuncar parents: 53026 diff changeset	30	"reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
e81ee43ab290 delete or move now not necessary reflexivity rules due to 1726f46d2aa8 kuncar parents: 53026 diff changeset	31	unfolding reflp_def split_sum_all sum_rel_simps by fast
e81ee43ab290 delete or move now not necessary reflexivity rules due to 1726f46d2aa8 kuncar parents: 53026 diff changeset	32
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	33	lemma sum_symp:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	34	"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	35	unfolding symp_def split_sum_all sum_rel_simps by fast
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	36
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	37	lemma sum_transp:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	38	"transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (sum_rel R1 R2)"
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	39	unfolding transp_def split_sum_all sum_rel_simps by fast
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	40
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	41	lemma sum_equivp [quot_equiv]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	42	"equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
51994 82cc2aeb7d13 stronger reflexivity prover kuncar parents: 51956 diff changeset	43	by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
47624 16d433895d2e add new transfer rules and setup for lifting package huffman parents: 47455 diff changeset	44
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	45	lemma sum_quotient [quot_thm]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	46	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	47	assumes q2: "Quotient3 R2 Abs2 Rep2"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	48	shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	49	apply (rule Quotient3I)
41372 551eb49a6e91 tuned type_lifting declarations haftmann parents: 40820 diff changeset	50	apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	51	Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	52	using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
53026 e1a548c11845 got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs; traytel parents: 53012 diff changeset	53	apply (simp add: sum_rel_def comp_def split: sum.split)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	55
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	56	declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
47094 1a7ad2601cb5 store the relational theorem for every relator kuncar parents: 45802 diff changeset	57
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	58	lemma sum_Inl_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	59	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	60	assumes q2: "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	61	shows "(R1 ===> sum_rel R1 R2) Inl Inl"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	62	by auto
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	63
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	64	lemma sum_Inr_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	65	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	66	assumes q2: "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	67	shows "(R2 ===> sum_rel R1 R2) Inr Inr"
40465 2989f9f3aa10 more appropriate specification packages; fun_rel_def is no simp rule by default haftmann parents: 39302 diff changeset	68	by auto
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	70	lemma sum_Inl_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	71	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	72	assumes q2: "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73	shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
39302 d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI nipkow parents: 39198 diff changeset	74	apply(simp add: fun_eq_iff)
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	75	apply(simp add: Quotient3_abs_rep[OF q1])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	76	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	77
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40610 diff changeset	78	lemma sum_Inr_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	79	assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	80	assumes q2: "Quotient3 R2 Abs2 Rep2"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	81	shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
39302 d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI nipkow parents: 39198 diff changeset	82	apply(simp add: fun_eq_iff)
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	83	apply(simp add: Quotient3_abs_rep[OF q2])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	84	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	85
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	86	end

author	huffman
	Tue, 04 Mar 2014 14:00:59 -0800
changeset 55909	df6133adb63f
parent 55564	e81ee43ab290
child 55931	62156e694f3d
permissions	-rw-r--r--