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

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

author	huffman
	Fri, 04 Mar 2005 23:12:36 +0100
changeset 15576	efb95d0d01f7
child 15577	e16da3068ad6
permissions	-rw-r--r--