isabelle: src/HOL/Library/Quotient_Option.thy@9c1f21365326 (annotated)

47455 26315a545e26 updated headers; wenzelm parents: 47308 diff changeset	1	(* Title: HOL/Library/Quotient_Option.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: 35222 diff changeset	4
f1deaca15ca3 observe standard header format; wenzelm parents: 35222 diff changeset	5	header {* Quotient infrastructure for the option 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_Option
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: 40542 diff changeset	13	lemma option_rel_map1:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	14	"option_rel R (Option.map f x) y \<longleftrightarrow> option_rel (\<lambda>x. R (f 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: option_rel_def split: option.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	16
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	17	lemma option_rel_map2:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	18	"option_rel R x (Option.map f y) \<longleftrightarrow> option_rel (\<lambda>x y. R x (f 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: option_rel_def split: option.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	20
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	21	lemma option_map_id [id_simps]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	22	"Option.map id = id"
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	23	by (simp add: id_def Option.map.identity fun_eq_iff)
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	24
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: 53010 diff changeset	25	lemma option_rel_eq [id_simps]:
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	26	"option_rel (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: option_rel_def fun_eq_iff split: option.split)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	28
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	29	lemma option_symp:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	30	"symp R \<Longrightarrow> symp (option_rel R)"
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	31	unfolding symp_def split_option_all option_rel_simps by fast
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	32
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	33	lemma option_transp:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	34	"transp R \<Longrightarrow> transp (option_rel R)"
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 transp_def split_option_all option_rel_simps by fast
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	36
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	37	lemma option_equivp [quot_equiv]:
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	38	"equivp R \<Longrightarrow> equivp (option_rel R)"
51994 82cc2aeb7d13 stronger reflexivity prover kuncar parents: 51956 diff changeset	39	by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	40
fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	41	lemma option_quotient [quot_thm]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	42	assumes "Quotient3 R Abs Rep"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	43	shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	44	apply (rule Quotient3I)
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	45	apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	46	using Quotient3_rel [OF assms]
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	47	apply (simp add: option_rel_def split: option.split)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	48	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	49
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	50	declare [[mapQ3 option = (option_rel, option_quotient)]]
47094 1a7ad2601cb5 store the relational theorem for every relator kuncar parents: 45802 diff changeset	51
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	52	lemma option_None_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	53	assumes q: "Quotient3 R Abs Rep"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	54	shows "option_rel R None None"
47624 16d433895d2e add new transfer rules and setup for lifting package huffman parents: 47455 diff changeset	55	by (rule None_transfer)
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	56
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	57	lemma option_Some_rsp [quot_respect]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	58	assumes q: "Quotient3 R Abs Rep"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	59	shows "(R ===> option_rel R) Some Some"
47624 16d433895d2e add new transfer rules and setup for lifting package huffman parents: 47455 diff changeset	60	by (rule Some_transfer)
35222 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: 40542 diff changeset	62	lemma option_None_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	63	assumes q: "Quotient3 R Abs Rep"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	64	shows "Option.map Abs None = None"
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	65	by simp
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	66
40820 fd9c98ead9a9 more systematic and compact proofs on type relation operators using natural deduction rules haftmann parents: 40542 diff changeset	67	lemma option_Some_prs [quot_preserve]:
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	68	assumes q: "Quotient3 R Abs Rep"
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	69	shows "(Rep ---> Option.map Abs) Some = Some"
39302 d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI nipkow parents: 39198 diff changeset	70	apply(simp add: fun_eq_iff)
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47094 diff changeset	71	apply(simp add: Quotient3_abs_rep[OF q])
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	72	done
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	73
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: diff changeset	74	end

author	wenzelm
	Sat, 09 Nov 2013 18:00:36 +0100
changeset 54381	9c1f21365326
parent 53026	e1a548c11845
child 55466	786edc984c98
permissions	-rw-r--r--