isabelle: src/HOLCF/Up.thy@d6156cb8dc2e (annotated)

15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	1	(* Title: HOLCF/Up.thy
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	2	ID: $Id$
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	3	Author: Franz Regensburger
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	4	Additions by Brian Huffman
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	5	License: GPL (GNU GENERAL PUBLIC LICENSE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	6
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	7	Lifting.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	8	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	9
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	10	header {* The type of lifted values *}
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	11
15577 e16da3068ad6 fix headers huffman parents: 15576 diff changeset	12	theory Up
e16da3068ad6 fix headers huffman parents: 15576 diff changeset	13	imports Cfun Sum_Type Datatype
e16da3068ad6 fix headers huffman parents: 15576 diff changeset	14	begin
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	15
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	16	defaultsort cpo
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	17
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	18	subsection {* Definition of new type for lifting *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	19
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	20	typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	21
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	22	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	23	Iup :: "'a => ('a)u"
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	24	Ifup :: "('a->'b)=>('a)u => 'b::pcpo"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	25
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	26	defs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	27	Iup_def: "Iup x == Abs_Up(Inr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	28	Ifup_def: "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU \| Inr(z) => f$z"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	29
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	30	lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	31	by (simp add: Up_def Abs_Up_inverse)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	32
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	33	lemma Exh_Up: "z = Abs_Up(Inl ()) \| (? x. z = Iup x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	34	apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	35	apply (rule Rep_Up_inverse [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	36	apply (rule_tac s = "Rep_Up z" in sumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	37	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	38	apply (rule_tac f = "Abs_Up" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	39	apply (rule unit_eq [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	40	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	42	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	apply (rule_tac f = "Abs_Up" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	44	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	45	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	46
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	47	lemma inj_Abs_Up: "inj(Abs_Up)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	48	apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	49	apply (rule Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	50	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	51
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	52	lemma inj_Rep_Up: "inj(Rep_Up)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	53	apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	54	apply (rule Rep_Up_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	55	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	56
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	57	lemma inject_Iup [dest!]: "Iup x=Iup y ==> x=y"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	58	apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	59	apply (rule inj_Inr [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	60	apply (rule inj_Abs_Up [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	61	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	62	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	63
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	64	lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	65	apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	66	apply (rule notI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	67	apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	68	apply (rule Inl_not_Inr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	69	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	70	apply (erule inj_Abs_Up [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	71	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	72
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	73	lemma upE: "[\| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q\|] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	74	apply (rule Exh_Up [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	75	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	76	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	77	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	78	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	79
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	80	lemma Ifup1 [simp]: "Ifup(f)(Abs_Up(Inl ()))=UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	81	apply (unfold Ifup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	82	apply (subst Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	83	apply (subst sum_case_Inl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	84	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	85	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	86
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	87	lemma Ifup2 [simp]: "Ifup(f)(Iup(x))=f$x"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	88	apply (unfold Ifup_def Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	89	apply (subst Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	90	apply (subst sum_case_Inr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	91	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	92	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	93
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	94	subsection {* Ordering on type @{typ "'a u"} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	95
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	96	instance u :: (sq_ord) sq_ord ..
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	97
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	98	defs (overloaded)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	99	less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	100	Inl(y1) => True
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	101	\| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	102	\| Inr(z2) => y2<<z2))"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	103
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	104	lemma less_up1a [iff]:
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	105	"Abs_Up(Inl ())<< z"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	106	by (simp add: less_up_def Abs_Up_inverse2)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	107
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	108	lemma less_up1b [iff]:
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	109	"~(Iup x) << (Abs_Up(Inl ()))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	110	by (simp add: Iup_def less_up_def Abs_Up_inverse2)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	111
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	112	lemma less_up1c [iff]:
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	113	"(Iup x) << (Iup y)=(x<<y)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	114	by (simp add: Iup_def less_up_def Abs_Up_inverse2)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	115
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	116	subsection {* Type @{typ "'a u"} is a partial order *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	117
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	118	lemma refl_less_up: "(p::'a u) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	119	apply (rule_tac p = "p" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	120	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	121	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	122
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	123	lemma antisym_less_up: "[\|(p1::'a u) << p2;p2 << p1\|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	124	apply (rule_tac p = "p1" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	125	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	126	apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	127	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	128	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	129	apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	130	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	131	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	132	apply (drule antisym_less, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	133	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	134	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	135
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	136	lemma trans_less_up: "[\|(p1::'a u) << p2;p2 << p3\|] ==> p1 << p3"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	137	apply (rule_tac p = "p1" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	138	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	139	apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	140	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	141	apply (rule_tac p = "p3" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	142	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	143	apply (blast intro: trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	144	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	145
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	146	instance u :: (cpo) po
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	147	by intro_classes
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	148	(assumption \| rule refl_less_up antisym_less_up trans_less_up)+
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	149
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	150	text {* for compatibility with old HOLCF-Version *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	151	lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	152	Inl(y1) => True
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	153	\| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	154	\| Inr(z2) => y2<<z2))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	155	apply (fold less_up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	156	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	157	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	158
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	159	subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	160
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	161	lemma monofun_Iup: "monofun(Iup)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	162	by (simp add: monofun)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	163
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	164	lemma monofun_Ifup1: "monofun(Ifup)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	165	apply (rule monofunI [rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	166	apply (rule less_fun [THEN iffD2, rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	167	apply (rule_tac p = "xa" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	168	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	169	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	170	apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	171	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	172
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	173	lemma monofun_Ifup2: "monofun(Ifup(f))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	174	apply (rule monofunI [rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	175	apply (rule_tac p = "x" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	176	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	177	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	178	apply (rule_tac p = "y" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	179	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	180	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	181	apply (erule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	182	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	183
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	184	subsection {* Type @{typ "'a u"} is a cpo *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	185
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	186	text {* Some kind of surjectivity lemma *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	187
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	188	lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	189	by simp
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	190
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	191	lemma lub_up1a: "[\|chain(Y);EX i x. Y(i)=Iup(x)\|]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	192	==> range(Y) <<\| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	193	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	194	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	195	apply (rule_tac p = "Y (i) " in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	196	apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	197	apply (erule sym)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	198	apply (rule less_up1a)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	199	apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	200	apply assumption
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	201	apply (rule less_up1c [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	202	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	203	apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	204	apply (rule_tac p = "u" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	205	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	206	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	207	apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	208	apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	209	apply assumption
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	210	apply (rule less_up1b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	211	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	212	apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	213	apply (rule_tac t = "u" in up_lemma1 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	214	apply assumption
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	215	apply (rule less_up1c [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	216	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	217	apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	218	apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	219	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	220
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	221	lemma lub_up1b: "[\|chain(Y); ALL i x. Y(i)~=Iup(x)\|] ==> range(Y) <<\| Abs_Up (Inl ())"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	222	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	223	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	224	apply (rule_tac p = "Y (i) " in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	225	apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	226	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	227	apply (rule refl_less)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	228	apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	229	apply (rule less_up1a)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	230	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	231
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	232	lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	233	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	234	[\| chain ?Y1; EX i x. ?Y1 i = Iup x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	235	lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	236	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	237
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	238	lemmas thelub_up1b = lub_up1b [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	239	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	240	[\| chain ?Y1; ! i x. ?Y1 i ~= Iup x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	241	lub (range ?Y1) = UU_up
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	242	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	243
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	244	text {* New versions where @{typ "'a"} does not have to be a pcpo *}
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	245
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	246	lemma up_lemma1a: "EX x. z=Iup(x) ==> Iup(THE a. Iup a = z) = z"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	247	apply (erule exE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	248	apply (rule theI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	249	apply (erule sym)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	250	apply simp
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	251	apply (erule inject_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	252	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	253
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	254	text {* Now some lemmas about chains of @{typ "'a u"} elements *}
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	255
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	256	lemma up_chain_lemma1:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	257	"[\| chain Y; EX x. Y j = Iup x \|] ==> EX x. Y (i + j) = Iup x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	258	apply (drule_tac x="j" and y="i + j" in chain_mono3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	259	apply (rule le_add2)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	260	apply (rule_tac p="Y (i + j)" in upE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	261	apply auto
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	262	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	263
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	264	lemma up_chain_lemma2:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	265	"[\| chain Y; EX x. Y j = Iup x \|] ==>
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	266	Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	267	apply (drule_tac i=i in up_chain_lemma1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	268	apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	269	apply (erule up_lemma1a)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	270	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	271
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	272	lemma up_chain_lemma3:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	273	"[\| chain Y; EX x. Y j = Iup x \|] ==> chain (%i. THE a. Iup a = Y (i + j))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	274	apply (rule chainI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	275	apply (rule less_up1c [THEN iffD1])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	276	apply (simp only: up_chain_lemma2)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	277	apply (simp add: chainE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	278	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	279
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	280	lemma up_chain_lemma4:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	281	"[\| chain Y; EX x. Y j = Iup x \|] ==>
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	282	(%i. Y (i + j)) = (%i. Iup (THE a. Iup a = Y (i + j)))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	283	apply (rule ext)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	284	apply (rule up_chain_lemma2 [symmetric])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	285	apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	286	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	287
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	288	lemma is_lub_range_shift:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	289	"[\| chain S; range (%i. S (i + j)) <<\| x \|] ==> range S <<\| x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	290	apply (rule is_lubI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	291	apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	292	apply (rule trans_less)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	293	apply (erule chain_mono3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	294	apply (rule le_add1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	295	apply (erule is_ub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	296	apply (erule is_lub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	297	apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	298	apply (erule ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	299	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	300
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	301	lemma is_lub_Iup:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	302	"range S <<\| x \<Longrightarrow> range (%i. Iup (S i)) <<\| Iup x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	303	apply (rule is_lubI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	304	apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	305	apply (subst less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	306	apply (erule is_ub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	307	apply (rule_tac p=u in upE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	308	apply (drule ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	309	apply (simp only: less_up1b)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	310	apply (simp only: less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	311	apply (erule is_lub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	312	apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	313	apply (drule_tac i=i in ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	314	apply (simp only: less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	315	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	316
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	317	lemma lub_up1c: "[\|chain(Y); EX x. Y(j)=Iup(x)\|]
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	318	==> range(Y) <<\| Iup(lub(range(%i. THE a. Iup a = Y(i + j))))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	319	apply (rule_tac j=j in is_lub_range_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	320	apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	321	apply (subst up_chain_lemma4)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	322	apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	323	apply (rule is_lub_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	324	apply (rule thelubE [OF _ refl])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	325	apply (rule up_chain_lemma3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	326	apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	327	done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	328
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	329	lemmas thelub_up1c = lub_up1c [THEN thelubI, standard]
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	330
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	331	lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<\|x"
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	332	apply (case_tac "EX i x. Y i = Iup x")
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	333	apply (erule exE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	334	apply (rule exI)
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	335	apply (erule lub_up1c)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	336	apply assumption
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	337	apply (rule exI)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	338	apply (erule lub_up1b)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	339	apply simp
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	340	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	341
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	342	instance u :: (cpo) cpo
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	343	by intro_classes (rule cpo_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	344
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	345	subsection {* Type @{typ "'a u"} is pointed *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	346
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	347	lemma minimal_up: "Abs_Up(Inl ()) << z"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	348	by (rule less_up1a)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	349
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	350	lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	351
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	352	lemma least_up: "EX x::'a u. ALL y. x<<y"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	353	apply (rule_tac x = "Abs_Up (Inl ())" in exI)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	354	apply (rule minimal_up [THEN allI])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	355	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	356
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	357	instance u :: (cpo) pcpo
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	358	by intro_classes (rule least_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	359
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	360	text {* for compatibility with old HOLCF-Version *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	361	lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	362	by (simp add: UU_def UU_up_def)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	363
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	364	text {* some lemmas restated for class pcpo *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	365
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	366	lemma less_up3b: "~ Iup(x) << UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	367	apply (subst inst_up_pcpo)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	368	apply (rule less_up1b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	369	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	370
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	371	lemma defined_Iup2 [iff]: "Iup(x) ~= UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	372	apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	373	apply (rule defined_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	374	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	375
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	376	subsection {* Continuity of @{term Iup} and @{term Ifup} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	377
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	378	text {* continuity for @{term Iup} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	379
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	380	lemma cont_Iup [iff]: "cont(Iup)"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	381	apply (rule contI [rule_format])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	382	apply (rule is_lub_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	383	apply (erule thelubE [OF _ refl])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	384	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	385
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	386	lemmas contlub_Iup = cont_Iup [THEN cont2contlub]
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	387
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	388	text {* continuity for @{term Ifup} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	389
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	390	lemma contlub_Ifup1: "contlub(Ifup)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	391	apply (rule contlubI [rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	392	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	393	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	394	apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	395	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	396	apply (rule_tac p = "x" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	397	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	398	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	399	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	400	apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	401	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	402
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	403	lemma contlub_Ifup2: "contlub(Ifup(f))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	404	apply (rule contlubI [rule_format])
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	405	apply (case_tac "EX i x. Y i = Iup x")
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	406	apply (erule exE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	407	apply (subst thelub_up1c)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	408	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	409	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	410	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	411	prefer 2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	412	apply (subst thelub_up1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	413	apply assumption
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	414	apply simp
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	415	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	416	apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	417	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	418	apply (rule_tac p = "Y(i)" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	419	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	420	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	421	apply (subst contlub_cfun_arg)
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	422	apply (erule up_chain_lemma3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	423	apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	424	apply (rule trans)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	425	prefer 2
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	426	apply (rule_tac j=i in lub_range_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	427	apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	428	apply (rule lub_equal [rule_format])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	429	apply (rule chain_monofun)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	430	apply (erule up_chain_lemma3)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	431	apply assumption
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	432	apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	433	apply (erule chain_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	434	apply (drule_tac i=k in up_chain_lemma1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	435	apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	436	apply clarify
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	437	apply simp
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	438	apply (subst the_equality)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	439	apply (rule refl)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	440	apply (erule inject_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	441	apply (rule refl)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	442	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	443
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	444	lemma cont_Ifup1: "cont(Ifup)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	445	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	446	apply (rule monofun_Ifup1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	447	apply (rule contlub_Ifup1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	448	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	449
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	450	lemma cont_Ifup2: "cont(Ifup(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	451	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	452	apply (rule monofun_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	453	apply (rule contlub_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	454	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	455
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	456	subsection {* Continuous versions of constants *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	457
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	458	constdefs
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	459	up :: "'a -> ('a)u"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	460	"up == (LAM x. Iup(x))"
15599 10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed huffman parents: 15593 diff changeset	461	fup :: "('a->'c)-> ('a)u -> 'c::pcpo"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	462	"fup == (LAM f p. Ifup(f)(p))"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	463
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	464	translations
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	465	"case l of up$x => t1" == "fup$(LAM x. t1)$l"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	466
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	467	text {* continuous versions of lemmas for @{typ "('a)u"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	468
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	469	lemma Exh_Up1: "z = UU \| (EX x. z = up$x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	470	apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	471	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	472	apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	473	apply (rule Exh_Up)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	474	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	475
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	476	lemma inject_up: "up$x=up$y ==> x=y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	477	apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	478	apply (rule inject_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	479	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	480	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	481
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	482	lemma defined_up [simp]: " up$x ~= UU"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	483	by (simp add: up_def)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	484
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	485	lemma upE1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	486	"[\| p=UU ==> Q; !!x. p=up$x==>Q\|] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	487	apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	488	apply (rule upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	489	apply (simp only: inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	490	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	491	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	492	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	493
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	494	lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	495
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	496	lemma fup1 [simp]: "fup$f$UU=UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	497	apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	498	apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	499	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	500	apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	501	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	502	apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	503	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	504	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	505
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	506	lemma fup2 [simp]: "fup$f$(up$x)=f$x"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	507	apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	508	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	509	apply (rule cont_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	510	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	511	apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	512	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	513	apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	514	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	515	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	516
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	517	lemma less_up4b: "~ up$x << UU"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	518	by (simp add: up_def fup_def less_up3b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	519
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	520	lemma less_up4c: "(up$x << up$y) = (x<<y)"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	521	by (simp add: up_def fup_def)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	522
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	523	lemma thelub_up2a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	524	"[\| chain(Y); EX i x. Y(i) = up$x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	525	lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	526	apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	527	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	528	apply (rule cont_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	529	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	530	apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	531	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	532	apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	533	apply (rule thelub_up1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	534	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	535	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	536	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	537	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	538	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	539	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	540	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	541	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	542	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	543
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	544	lemma thelub_up2b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	545	"[\| chain(Y); ! i x. Y(i) ~= up$x \|] ==> lub(range(Y)) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	546	apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	547	apply (subst inst_up_pcpo)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	548	apply (erule thelub_up1b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	549	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	550	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	551
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	552	lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	553	apply (rule iffI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	554	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	555	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	556	apply (rule_tac p = "z" in upE1)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	557	apply simp
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	558	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	559	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	560
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	561	lemma thelub_up2a_rev:
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	562	"[\| chain(Y); lub(range(Y)) = up$x \|] ==> EX i x. Y(i) = up$x"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	563	apply (rule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	564	apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	565	apply (rule up_lemma2 [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	566	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	567	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	568	apply (rule up_lemma2 [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	569	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	570	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	571
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	572	lemma thelub_up2b_rev:
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	573	"[\| chain(Y); lub(range(Y)) = UU \|] ==> ! i x. Y(i) ~= up$x"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	574	by (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	575
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	576	lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU \|
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	577	lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	578	apply (rule disjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	579	apply (rule_tac [2] disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	580	apply (rule_tac [2] thelub_up2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	581	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	582	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	583	apply (rule_tac [2] disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	584	apply (rule_tac [2] thelub_up2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	585	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	586	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	587	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	588	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	589
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	590	lemma fup3: "fup$up$x=x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	591	apply (rule_tac p = "x" in upE1)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	592	apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	593	apply simp
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	594	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	595
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	596	text {* for backward compatibility *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	597
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	598	lemmas less_up2b = less_up1b
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	599	lemmas less_up2c = less_up1c
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	600
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	601	end

author	kleing
	Sat, 30 Apr 2005 14:18:36 +0200
changeset 15900	d6156cb8dc2e
parent 15599	10cedbd5289e
child 16070	4a83dd540b88
permissions	-rw-r--r--