isabelle: src/HOL/Lifting_Sum.thy@c0da3fc313e3 (annotated)

53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	1	(* Title: HOL/Lifting_Sum.thy
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	2	Author: Brian Huffman and Ondrej Kuncar
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	3	*)
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	4
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	5	header {* Setup for Lifting/Transfer for the sum type *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	6
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	7	theory Lifting_Sum
55083 0a689157e3ce move BNF_LFP up the dependency chain blanchet parents: 53026 diff changeset	8	imports Lifting Basic_BNFs
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	9	begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	10
56526 58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons kuncar parents: 56525 diff changeset	11	(* The following lemma can be deleted when sum is added to FP sugar *)
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons kuncar parents: 56525 diff changeset	12	lemma sum_pred_inject [simp]:
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons kuncar parents: 56525 diff changeset	13	"pred_sum P1 P2 (Inl a) = P1 a" and "pred_sum P1 P2 (Inr a) = P2 a"
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons kuncar parents: 56525 diff changeset	14	unfolding pred_sum_def fun_eq_iff sum_set_simps by auto
58ac520db7ae add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons kuncar parents: 56525 diff changeset	15
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	16	subsection {* Transfer rules for the Transfer package *}
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	17
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	18	context
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	19	begin
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	20	interpretation lifting_syntax .
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	21
55943 5c2df04e97d1 renamed 'sum_rel' to 'rel_sum' blanchet parents: 55931 diff changeset	22	lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
55945 e96383acecf9 renamed 'fun_rel' to 'rel_fun' blanchet parents: 55943 diff changeset	23	unfolding rel_fun_def by simp
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	24
55943 5c2df04e97d1 renamed 'sum_rel' to 'rel_sum' blanchet parents: 55931 diff changeset	25	lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
55945 e96383acecf9 renamed 'fun_rel' to 'rel_fun' blanchet parents: 55943 diff changeset	26	unfolding rel_fun_def by simp
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	27
55414 eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...' blanchet parents: 55084 diff changeset	28	lemma case_sum_transfer [transfer_rule]:
55943 5c2df04e97d1 renamed 'sum_rel' to 'rel_sum' blanchet parents: 55931 diff changeset	29	"((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
55945 e96383acecf9 renamed 'fun_rel' to 'rel_fun' blanchet parents: 55943 diff changeset	30	unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
53012 cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	31
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	32	end
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	33
cb82606b8215 move Lifting/Transfer relevant parts of Library/Quotient_* to Main kuncar parents: diff changeset	34	end

author	fleury
	Wed, 30 Jul 2014 14:03:12 +0200
changeset 57704	c0da3fc313e3
parent 56526	58ac520db7ae
child 58889	5b7a9633cfa8
permissions	-rw-r--r--