isabelle: src/HOLCF/Sprod.thy@1fb24e545f88 (annotated)

15600 a59f07556a8d fixed filename in header huffman parents: 15591 diff changeset	1	(* Title: HOLCF/Sprod.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
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	Strict product with typedef.
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 strict products *}
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	10
15577 e16da3068ad6 fix headers huffman parents: 15576 diff changeset	11	theory Sprod
e16da3068ad6 fix headers huffman parents: 15576 diff changeset	12	imports Cfun
e16da3068ad6 fix headers huffman parents: 15576 diff changeset	13	begin
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	14
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	15	subsection {* Definition of strict product type *}
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	16
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	17	constdefs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	18	Spair_Rep :: "['a,'b] => ['a,'b] => bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	19	"Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	20
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	21	typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	22	by auto
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	syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	25	"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	26	syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	27	"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	28
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	29	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	30	Ispair :: "['a,'b] => ('a ** 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	31	Isfst :: "('a ** 'b) => 'a"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	32	Issnd :: "('a ** 'b) => 'b"
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	defs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	35	(defining the abstract constants)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	36
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	37	Ispair_def: "Ispair a b == Abs_Sprod(Spair_Rep a b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	38
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	39	Isfst_def: "Isfst(p) == @z. (p=Ispair UU UU --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	40	&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	42	Issnd_def: "Issnd(p) == @z. (p=Ispair UU UU --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	44
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	45	text {* A non-emptiness result for Sprod *}
15576 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 SprodI: "(Spair_Rep a b):Sprod"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	48	apply (unfold Sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	49	apply (rule CollectI, rule exI, rule exI, rule refl)
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_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
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 (erule Abs_Sprod_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
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	57	text {* Strictness and definedness of @{term Spair_Rep} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	58
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	59	lemma strict_Spair_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	60	"(a=UU \| b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	61	apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	62	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	63	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	64	apply (rule iffI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	65	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	66	apply fast
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	lemma defined_Spair_Rep_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	70	"(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU \| b=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	71	apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	72	apply (case_tac "a=UU\|b=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	73	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	74	apply (fast dest: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	75	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	76
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	77	text {* injectivity of @{term Spair_Rep} and @{term Ispair} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	78
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	79	lemma inject_Spair_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	80	"[\|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba \|] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	81
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	82	apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	83	apply (drule fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	84	apply (drule fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	85	apply (erule iffD1 [THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	86	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	87	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	88
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	89	lemma inject_Ispair:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	90	"[\|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba \|] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	91	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	92	apply (erule inject_Spair_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	93	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	94	apply (erule inj_on_Abs_Sprod [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	95	apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	96	apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	97	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	98
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	99	text {* strictness and definedness of @{term Ispair} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	100
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	101	lemma strict_Ispair:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	102	"(a=UU \| b=UU) ==> Ispair a b = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	103	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	104	apply (erule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	105	done
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 strict_Ispair1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	108	"Ispair UU b = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	109	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	110	apply (rule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	111	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	112	apply (rule refl)
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 strict_Ispair2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	116	"Ispair a UU = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	117	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	118	apply (rule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	119	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	120	apply (rule refl)
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 strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	124	apply (rule de_Morgan_disj [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	125	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	126	apply (erule strict_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	127	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	128
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	129	lemma defined_Ispair_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	130	"Ispair a b = Ispair UU UU ==> (a = UU \| b = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	131	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	132	apply (rule defined_Spair_Rep_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	133	apply (rule inj_on_Abs_Sprod [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	134	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	135	apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	136	apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	137	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	138
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	139	lemma defined_Ispair: "[\|a~=UU; b~=UU\|] ==> (Ispair a b) ~= (Ispair UU UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	140	apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	141	apply (erule_tac [2] defined_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	142	apply (rule de_Morgan_disj [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	143	apply (erule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	144	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	145	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	146
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	147	text {* Exhaustion of the strict product @{typ "'a ** 'b"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	148
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	149	lemma Exh_Sprod:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	150	"z=Ispair UU UU \| (? a b. z=Ispair a b & a~=UU & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	151	apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	152	apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	153	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	154	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	155	apply (rule excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	156	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	157	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	158	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	159	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	160	apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	161	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	162	apply (rule de_Morgan_disj [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	163	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	164	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	165	apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	166	apply (rule_tac f = "Abs_Sprod" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	167	apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	168	apply (erule strict_Spair_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	169	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	170
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	171	text {* general elimination rule for strict product *}
15576 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 IsprodE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	174	assumes prem1: "p=Ispair UU UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	175	assumes prem2: "!!x y. [\|p=Ispair x y; x~=UU ; y~=UU\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	176	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	177	apply (rule Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	178	apply (erule prem1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	179	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	180	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	181	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	182	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	183	apply (erule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	184	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	185	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	186	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	187
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	188	text {* some results about the selectors @{term Isfst}, @{term Issnd} *}
15576 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 strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	191	apply (unfold Isfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	192	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	193	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	194	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	195	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	196	apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	197	apply (rule not_sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	198	apply (rule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	199	apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	200	done
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	lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	203	apply (subst strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	204	apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	205	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	206	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	207
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	208	lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	209	apply (subst strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	210	apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	211	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	212	done
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	lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	215	apply (unfold Issnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	216	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	217	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	218	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	219	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	220	apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	221	apply (rule not_sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	222	apply (rule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	223	apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	224	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	225
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	226	lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	227	apply (subst strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	228	apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	229	apply (rule refl)
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	lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	233	apply (subst strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	234	apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	235	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	236	done
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	lemma Isfst: "[\|x~=UU ;y~=UU \|] ==> Isfst(Ispair x y) = x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	239	apply (unfold Isfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	240	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	241	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	242	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	243	apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	244	apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	245	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	246	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	247	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	248	apply (rule inject_Ispair [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	249	prefer 3 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	250	apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	251	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	252
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	253	lemma Issnd: "[\|x~=UU ;y~=UU \|] ==> Issnd(Ispair x y) = y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	254	apply (unfold Issnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	255	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	256	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	257	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	258	apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	259	apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	260	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	261	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	262	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	263	apply (rule inject_Ispair [THEN conjunct2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	264	prefer 3 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	265	apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	266	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	267
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	268	lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	269	apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	270	apply (erule Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	271	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	272	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	273	apply (rule strict_Isfst1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	274	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	275
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	276	lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	277	apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	278	apply (erule Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	279	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	280	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	281	apply (rule strict_Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	282	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	283
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	284
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	285	text {* instantiate the simplifier *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	286
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	287	lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	288	Isfst2 Issnd2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	289
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	290	declare Isfst2 [simp] Issnd2 [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	291
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	292	lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	293	apply (rule_tac p = "p" in IsprodE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	294	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	295	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	296	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	297	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	298	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	299	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	300
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	301
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	302	text {* Surjective pairing: equivalent to @{thm [source] Exh_Sprod} *}
15576 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	lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	305	apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	306	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	307	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	308	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	309	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	310	done
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	lemma Sel_injective_Sprod: "[\|Isfst x = Isfst y; Issnd x = Issnd y\|] ==> x = y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	313	apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	314	apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	315	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	316	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	317
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	318	subsection {* Type @{typ "'a ** 'b"} is a partial order *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	319
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	320	instance "**" :: (sq_ord, sq_ord) sq_ord ..
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	321
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	322	defs (overloaded)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	323	less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	324
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	325	lemma refl_less_sprod: "(p::'a ** 'b) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	326	apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	327	apply (fast intro: refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	328	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	329
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	330	lemma antisym_less_sprod:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	331	"[\|(p1::'a ** 'b) << p2;p2 << p1\|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	332	apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	333	apply (rule Sel_injective_Sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	334	apply (fast intro: antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	335	apply (fast intro: antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	336	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	337
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	338	lemma trans_less_sprod:
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	339	"[\|(p1::'a ** 'b) << p2;p2 << p3\|] ==> p1 << p3"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	340	apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	341	apply (blast intro: trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	342	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	343
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	344	instance "**" :: (pcpo, pcpo) po
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	345	by intro_classes
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	346	(assumption \| rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	347
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	348	text {* for compatibility with old HOLCF-Version *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	349	lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	350	apply (fold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	351	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	352	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	353
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	354	subsection {* Monotonicity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	355
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	356	text {* @{term Ispair} is monotone in both arguments *}
15576 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 monofun_Ispair1: "monofun(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	359	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	360	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	361	apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	362	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	363	apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	364	apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	365	apply (frule notUU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	366	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	367	apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	368	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	369
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	370	lemma monofun_Ispair2: "monofun(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	371	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	372	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	373	apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	374	apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	375	apply (frule notUU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	376	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	377	apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	378	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	379
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	380	lemma monofun_Ispair: "[\|x1<<x2; y1<<y2\|] ==> Ispair x1 y1 << Ispair x2 y2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	381	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	382	apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	383	prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	384	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	385	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	386	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	387
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	388	text {* @{term Isfst} and @{term Issnd} are monotone *}
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 monofun_Isfst: "monofun(Isfst)"
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	391	by (simp add: monofun inst_sprod_po)
15576 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	lemma monofun_Issnd: "monofun(Issnd)"
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	394	by (simp add: monofun inst_sprod_po)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	395
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	396	subsection {* Type @{typ "'a ** 'b"} is a cpo *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	397
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	398	lemma lub_sprod:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	399	"[\|chain(S)\|] ==> range(S) <<\|
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	400	Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	401	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	402	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	403	apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	404	apply (rule monofun_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	405	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	406	apply (erule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	407	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	408	apply (erule monofun_Issnd [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	409	apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	410	apply (rule monofun_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	411	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	412	apply (erule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	413	apply (erule monofun_Isfst [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	414	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	415	apply (erule monofun_Issnd [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	416	apply (erule monofun_Issnd [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	417	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	418
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	419	lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	420
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	421	lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<\| x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	422	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	423	apply (erule lub_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	424	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	425
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	426	instance "**" :: (pcpo, pcpo) cpo
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	427	by intro_classes (rule cpo_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	428
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	429	subsection {* Type @{typ "'a ** 'b"} is pointed *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	430
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	431	lemma minimal_sprod: "Ispair UU UU << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	432	apply (simp add: inst_sprod_po minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	433	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	434
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	435	lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	436
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	437	lemma least_sprod: "? x::'a**'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	438	apply (rule_tac x = "Ispair UU UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	439	apply (rule minimal_sprod [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	440	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	441
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	442	instance "**" :: (pcpo, pcpo) pcpo
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	443	by intro_classes (rule least_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	444
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	445	text {* for compatibility with old HOLCF-Version *}
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	446	lemma inst_sprod_pcpo: "UU = Ispair UU UU"
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	447	by (simp add: UU_def UU_sprod_def)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	448
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	449	declare inst_sprod_pcpo [symmetric, simp]
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	450
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	451	subsection {* Continuous versions of constants *}
15576 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	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	454	spair :: "'a -> 'b -> ('a*'b)" ( continuous strict pairing *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	455	sfst :: "('a**'b)->'a"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	456	ssnd :: "('a**'b)->'b"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	457	ssplit :: "('a->'b->'c)->('a**'b)->'c"
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	syntax
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	460	"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	461
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	462	translations
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	463	"(:x, y, z:)" == "(:x, (:y, z:):)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	464	"(:x, y:)" == "spair$x$y"
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	defs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	467	spair_def: "spair == (LAM x y. Ispair x y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	468	sfst_def: "sfst == (LAM p. Isfst p)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	469	ssnd_def: "ssnd == (LAM p. Issnd p)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	470	ssplit_def: "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	471
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	472	subsection {* Continuity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	473
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	474	lemma sprod3_lemma1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	475	"[\| chain(Y); x~= UU; lub(range(Y))~= UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	476	Ispair (lub(range Y)) x =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	477	Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	478	(lub(range(%i. Issnd(Ispair(Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	479	apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	480	apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	481	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	482	apply (rule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	483	apply (rule ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	484	apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	485	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	486	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	487	apply (simp (no_asm_simp))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	488	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	489	apply (drule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	490	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	491	apply (rule lub_chain_maxelem)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	492	apply (erule Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	493	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	494	apply (rename_tac "j")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	495	apply (case_tac "Y (j) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	496	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	497	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	498
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	499	lemma sprod3_lemma2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	500	"[\| chain(Y); x ~= UU; lub(range(Y)) = UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	501	Ispair (lub(range Y)) x =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	502	Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	503	(lub(range(%i. Issnd(Ispair(Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	504	apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	505	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	506	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	507	apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	508	apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	509	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	510	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	511	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	512	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	513	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	514	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	515
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 sprod3_lemma3:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	518	"[\| chain(Y); x = UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	519	Ispair (lub(range Y)) x =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	520	Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	521	(lub(range(%i. Issnd(Ispair (Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	522	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	523	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	524	apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	525	apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	526	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	527	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	528	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	529	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	530	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	531
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	532	lemma contlub_Ispair1: "contlub(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	533	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	534	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	535	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	536	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	537	apply (subst lub_fun [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	538	apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	539	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	540	apply (rule_tac [2] thelub_sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	541	apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	542	apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	543	apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	544	apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	545	apply (erule sprod3_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	546	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	547	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	548	apply (erule sprod3_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	549	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	550	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	551	apply (erule sprod3_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	552	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	553	done
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	lemma sprod3_lemma4:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	556	"[\| chain(Y); x ~= UU; lub(range(Y)) ~= UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	557	Ispair x (lub(range Y)) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	558	Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	559	(lub(range(%i. Issnd (Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	560	apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	561	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	562	apply (drule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	563	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	564	apply (rule lub_chain_maxelem)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	565	apply (erule Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	566	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	567	apply (rename_tac "j")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	568	apply (case_tac "Y (j) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	569	apply auto
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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	572	lemma sprod3_lemma5:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	573	"[\| chain(Y); x ~= UU; lub(range(Y)) = UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	574	Ispair x (lub(range Y)) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	575	Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	576	(lub(range(%i. Issnd(Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	577	apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	578	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	579	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	580	apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	581	apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	582	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	583	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	584	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	585	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	586	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	587	apply assumption
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 sprod3_lemma6:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	591	"[\| chain(Y); x = UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	592	Ispair x (lub(range Y)) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	593	Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	594	(lub(range(%i. Issnd (Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	595	apply (rule_tac s = "UU" and t = "x" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	596	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	597	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	598	apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	599	apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	600	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	601	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	602	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	603	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	604	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	605
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	606	lemma contlub_Ispair2: "contlub(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	607	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	608	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	609	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	610	apply (rule_tac [2] thelub_sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	611	apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	612	apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	613	apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	614	apply (erule sprod3_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	615	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	616	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	617	apply (erule sprod3_lemma5)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	618	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	619	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	620	apply (erule sprod3_lemma6)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	621	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	622	done
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	lemma cont_Ispair1: "cont(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	625	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	626	apply (rule monofun_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	627	apply (rule contlub_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	628	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	629
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	630	lemma cont_Ispair2: "cont(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	631	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	632	apply (rule monofun_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	633	apply (rule contlub_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	634	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	635
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	636	lemma contlub_Isfst: "contlub(Isfst)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	637	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	638	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	639	apply (subst lub_sprod [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	640	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	641	apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	642	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	643	apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	644	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	645	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	646	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	647	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	648	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	649	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	650	apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	651	apply (rule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	652	apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	653	apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	654	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	655
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	656	lemma contlub_Issnd: "contlub(Issnd)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	657	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	658	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	659	apply (subst lub_sprod [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	660	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	661	apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	662	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	663	apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	664	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	665	apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	666	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	667	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	668	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	669	apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	670	apply (rule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	671	apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	672	apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	673	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	674
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	675	lemma cont_Isfst: "cont(Isfst)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	676	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	677	apply (rule monofun_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	678	apply (rule contlub_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	679	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	680
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	681	lemma cont_Issnd: "cont(Issnd)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	682	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	683	apply (rule monofun_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	684	apply (rule contlub_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	685	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	686
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	687	lemma spair_eq: "[\|x1=x2;y1=y2\|] ==> (:x1,y1:) = (:x2,y2:)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	688	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	689	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	690
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	691	text {* convert all lemmas to the continuous versions *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	692
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	693	lemma beta_cfun_sprod [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	694	"(LAM x y. Ispair x y)$a$b = Ispair a b"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	695	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	696	apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	697	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	698	apply (rule cont_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	699	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	700	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	701
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	702	lemma inject_spair:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	703	"[\| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) \|] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	704	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	705	apply (erule inject_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	706	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	707	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	708	apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	709	apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	710	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	711
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	712	lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	713	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	714	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	715	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	716	apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	717	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	718	apply (rule inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	719	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	720
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	721	lemma strict_spair:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	722	"(a=UU \| b=UU) ==> (:a,b:)=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	723	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	724	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	725	apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	726	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	727	apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	728	apply (erule strict_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	729	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	730
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	731	lemma strict_spair1: "(:UU,b:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	732	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	733	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	734	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	735	apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	736	apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	737	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	738
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	739	lemma strict_spair2: "(:a,UU:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	740	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	741	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	742	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	743	apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	744	apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	745	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	746
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	747	declare strict_spair1 [simp] strict_spair2 [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	748
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	749	lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	750	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	751	apply (rule strict_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	752	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	753	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	754
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	755	lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU \| b = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	756	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	757	apply (rule defined_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	758	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	759	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	760
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	761	lemma defined_spair [simp]:
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	762	"[\|a~=UU; b~=UU\|] ==> (:a,b:) ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	763	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	764	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	765	apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	766	apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	767	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	768	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	769
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	770	lemma Exh_Sprod2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	771	"z=UU \| (? a b. z=(:a,b:) & a~=UU & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	772	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	773	apply (rule Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	774	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	775	apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	776	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	777	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	778	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	779	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	780	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	781	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	782	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	783	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	784	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	785	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	786	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	787
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	788	lemma sprodE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	789	assumes prem1: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	790	assumes prem2: "!!x y. [\| p=(:x,y:); x~=UU; y~=UU\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	791	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	792	apply (rule IsprodE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	793	apply (rule prem1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	794	apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	795	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	796	apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	797	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	798	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	799	apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	800	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	801	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	802	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	803
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	804	lemma strict_sfst: "p=UU==>sfst$p=UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	805	apply (unfold sfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	806	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	807	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	808	apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	809	apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	810	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	811	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	812
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	813	lemma strict_sfst1 [simp]: "sfst$(:UU,y:) = UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	814	apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	815	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	816	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	817	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	818	apply (rule strict_Isfst1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	819	done
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	820
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	821	lemma strict_sfst2 [simp]: "sfst$(:x,UU:) = UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	822	apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	823	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	824	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	825	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	826	apply (rule strict_Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	827	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	828
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	829	lemma strict_ssnd: "p=UU==>ssnd$p=UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	830	apply (unfold ssnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	831	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	832	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	833	apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	834	apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	835	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	836	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	837
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	838	lemma strict_ssnd1 [simp]: "ssnd$(:UU,y:) = UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	839	apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	840	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	841	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	842	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	843	apply (rule strict_Issnd1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	844	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	845
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	846	lemma strict_ssnd2 [simp]: "ssnd$(:x,UU:) = UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	847	apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	848	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	849	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	850	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	851	apply (rule strict_Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	852	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	853
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	854	lemma sfst2 [simp]: "y~=UU ==>sfst$(:x,y:)=x"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	855	apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	856	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	857	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	858	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	859	apply (erule Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	860	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	861
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	862	lemma ssnd2 [simp]: "x~=UU ==>ssnd$(:x,y:)=y"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	863	apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	864	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	865	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	866	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	867	apply (erule Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	868	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	869
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	870
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	871	lemma defined_sfstssnd: "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	872	apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	873	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	874	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	875	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	876	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	877	apply (rule defined_IsfstIssnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	878	apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	879	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	880	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	881
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	882	lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	883	apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	884	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	885	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	886	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	887	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	888	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	889	apply (rule surjective_pairing_Sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	890	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	891
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	892	lemma lub_sprod2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	893	"chain(S) ==> range(S) <<\|
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	894	(: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	895	apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	896	apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	897	apply (simplesubst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	898	apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	899	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	900	apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	901	apply (erule lub_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	902	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	903
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	904	lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	905	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	906	"chain ?S1 ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	907	lub (range ?S1) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	908	(:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	909	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	910
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	911	lemma ssplit1 [simp]: "ssplit$f$UU=UU"
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	912	by (simp add: ssplit_def)
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	913
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	914	lemma ssplit2 [simp]: "[\|x~=UU;y~=UU\|] ==> ssplit$f$(:x,y:)= f$x$y"
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	915	by (simp add: ssplit_def)
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	916
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	917	lemma ssplit3: "ssplit$spair$z=z"
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	918	apply (simp add: ssplit_def)
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	919	apply (simp add: surjective_pairing_Sprod2)
50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	920	apply (case_tac "z=UU", simp_all)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	921	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	922
15591 50c3384ca6c4 reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	923	text {* install simplifier for Sprod *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	924
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	925	lemmas Sprod_rews = strict_sfst1 strict_sfst2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	926	strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	927	ssplit1 ssplit2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	928
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	929	end

author	huffman
	Thu, 31 Mar 2005 02:44:46 +0200
changeset 15638	1fb24e545f88
parent 15600	a59f07556a8d
child 15930	145651bc64a8
permissions	-rw-r--r--