isabelle: src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy@cc19f7ca2ed6 (annotated)

58309 a09ec6daaa19 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf') blanchet parents: 57641 diff changeset	1	(* Title: HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	2	Author: Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	3	Copyright 2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	4
49463 83ac281bcdc2 provide predicator, define relator blanchet parents: 48975 diff changeset	5	Preliminaries.
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	6	*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	7
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	8	section \<open>Preliminaries\<close>
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	10	theory Prelim
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	11	imports "HOL-Library.FSet"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	12	begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	13
57641 dc59f147b27d more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy); wenzelm parents: 55931 diff changeset	14	notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
55091 c43394c2e5ec compile blanchet parents: 55075 diff changeset	15
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	16	declare fset_to_fset[simp]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	17
57641 dc59f147b27d more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy); wenzelm parents: 55931 diff changeset	18	lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	19	apply(rule ext) by (simp add: convol_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	20
49514 45e3e564e306 tuned whitespace blanchet parents: 49510 diff changeset	21	abbreviation sm_abbrev (infix "\<oplus>" 60)
55931 62156e694f3d renamed 'map_sum' to 'sum_map' blanchet parents: 55414 diff changeset	22	where "f \<oplus> g \<equiv> Sum_Type.map_sum f g"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	23
55931 62156e694f3d renamed 'map_sum' to 'sum_map' blanchet parents: 55414 diff changeset	24	lemma map_sum_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	25	by (cases z) auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	26
55931 62156e694f3d renamed 'map_sum' to 'sum_map' blanchet parents: 55414 diff changeset	27	lemma map_sum_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	28	by (cases z) auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	29
55414 eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...' blanchet parents: 55129 diff changeset	30	abbreviation case_sum_abbrev ("[[_,_]]" 800)
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...' blanchet parents: 55129 diff changeset	31	where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	32
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	33	lemma Inl_oplus_elim:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	34	assumes "Inl tr \<in> (id \<oplus> f) ` tns"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	35	shows "Inl tr \<in> tns"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	36	using assms apply clarify by (case_tac x, auto)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	37
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	38	lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	39	using Inl_oplus_elim
55931 62156e694f3d renamed 'map_sum' to 'sum_map' blanchet parents: 55414 diff changeset	40	by (metis id_def image_iff map_sum.simps(1))
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	41
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	42	lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	43	using Inl_oplus_iff unfolding vimage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	44
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	45	lemma Inr_oplus_elim:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	46	assumes "Inr tr \<in> (id \<oplus> f) ` tns"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	47	shows "\<exists> n. Inr n \<in> tns \<and> f n = tr"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	48	using assms apply clarify by (case_tac x, auto)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	49
49514 45e3e564e306 tuned whitespace blanchet parents: 49510 diff changeset	50	lemma Inr_oplus_iff[simp]:
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	51	"Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	52	apply (rule iffI)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	53	apply (metis Inr_oplus_elim)
55931 62156e694f3d renamed 'map_sum' to 'sum_map' blanchet parents: 55414 diff changeset	54	by (metis image_iff map_sum.simps(2))
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	55
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	56	lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	57	using Inr_oplus_iff unfolding vimage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	58
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	59	lemma Inl_Inr_image_cong:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	60	assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	61	shows "A = B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	62	apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	63
62390 842917225d56 more canonical names nipkow parents: 58889 diff changeset	64	end

author	wenzelm
	Fri, 18 Aug 2017 20:47:47 +0200
changeset 66453	cc19f7ca2ed6
parent 63167	0909deb8059b
permissions	-rw-r--r--