nominal2: Quot/Quotients.thy@8a1c8dc72b5c (annotated)

0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	theory Quotients
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	imports Main
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	begin
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	4
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	5	(* Other quotients that have not been proved yet *)
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	7	fun
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	8	option_rel
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	where
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	10	"option_rel R None None = True"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	11	\| "option_rel R (Some x) None = False"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	12	\| "option_rel R None (Some x) = False"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	13	\| "option_rel R (Some x) (Some y) = R x y"
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	fun
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	option_map
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	where
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	"option_map f None = None"
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	\| "option_map f (Some x) = Some (f x)"
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	21	fun
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	22	prod_rel
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	where
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	24	"prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	fun
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	prod_map
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	where
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	"prod_map f1 f2 (a,b) = (f1 a, f2 b)"
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	30
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	fun
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	32	sum_rel
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	where
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	34	"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	35	\| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	36	\| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	37	\| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	38
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	fun
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	sum_map
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	where
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	"sum_map f1 f2 (Inl a) = Inl (f1 a)"
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	\| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	44
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	45
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	46
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	47
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	48
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	49	fun
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	50	noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	51	where
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	52	"noption_map f (nSome x) = nSome (f x)"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	53	\| "noption_map f nNone = nNone"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	54
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	55	fun
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	56	noption_rel
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	57	where
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	58	"noption_rel r (nSome x) (nSome y) = r x y"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	59	\| "noption_rel r _ _ = False"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	60
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	61	declare [[map noption = (noption_map, noption_rel)]]
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	62
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	63	lemma "noption_map id = id"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	64	sorry
0 ebe0ea8fe247 initial commit Christian Urban <urbanc@in.tum.de> parents: diff changeset	65
545 95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	66	lemma noption_Quotient:
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	67	assumes q: "Quotient R Abs Rep"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	68	shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)"
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	69	apply (unfold Quotient_def)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	70	apply (auto)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	71	using q
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	72	apply (unfold Quotient_def)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	73	apply (case_tac "a :: 'b noption")
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	74	apply (simp)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	75	apply (simp)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	76	apply (case_tac "a :: 'b noption")
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	77	apply (simp only: option_map.simps)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	78	apply (subst option_rel.simps)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	79	(* Simp starts hanging so don't know how to continue *)
95371a8b17e1 Cleaning the Quotients file Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 538 diff changeset	80	sorry

author	Christian Urban <urbanc@in.tum.de>
	Mon, 07 Dec 2009 14:09:50 +0100
changeset 597	8a1c8dc72b5c
parent 545	Quotients.thy@95371a8b17e1
child 613	018aabbffd08
permissions	-rw-r--r--