isabelle: src/HOLCF/Ssum.thy@24d770bbc44a (annotated)

15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1	(* Title: HOLCF/Ssum0.thy
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	2	ID: $Id$
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	3	Author: Franz Regensburger
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	5
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	6	Strict sum 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 sums *}
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 Ssum
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
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	15	subsection {* Definition of strict sum type *}
24d770bbc44a 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	Sinl_Rep :: "['a,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	19	"Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	20	Sinr_Rep :: "['b,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	21	"Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	22
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	23	typedef (Ssum) ('a, 'b) "++" (infixr 10) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	24	"{f.(? a. f=Sinl_Rep(a::'a))\|(? b. f=Sinr_Rep(b::'b))}"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	25	by auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	26
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	27	syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	28	"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	29	syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	30	"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	31
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	32	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	33	Isinl :: "'a => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	34	Isinr :: "'b => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	35	Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	36
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	37	defs -- {defining the abstract constants}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	38	Isinl_def: "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	39	Isinr_def: "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	40
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41	Iwhen_def: "Iwhen(f)(g)(s) == @z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	42	(s=Isinl(UU) --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	&(!a. a~=UU & s=Isinl(a) --> z=f$a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	44	&(!b. b~=UU & s=Isinr(b) --> z=g$b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	45
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	46	text {* A non-emptiness result for Ssum *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	47
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	48	lemma SsumIl: "Sinl_Rep(a):Ssum"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	49	by (unfold Ssum_def) blast
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	50
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	51	lemma SsumIr: "Sinr_Rep(a):Ssum"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	52	by (unfold Ssum_def) blast
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	53
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	54	lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	55	apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	56	apply (erule Abs_Ssum_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	57	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	58
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	59	text {* Strictness of @{term Sinr_Rep}, @{term Sinl_Rep} and @{term Isinl}, @{term Isinr} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	60
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	61	lemma strict_SinlSinr_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	62	"Sinl_Rep(UU) = Sinr_Rep(UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	63	apply (unfold Sinr_Rep_def Sinl_Rep_def)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	64	apply (rule ext)+
15576 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	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	67
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	68	lemma strict_IsinlIsinr: "Isinl(UU) = Isinr(UU)"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	69	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	70	apply (rule strict_SinlSinr_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	71	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	72
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	73	text {* distinctness of @{term Sinl_Rep}, @{term Sinr_Rep} and @{term Isinl}, @{term Isinr} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	74
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	75	lemma noteq_SinlSinr_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	76	"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	77	apply (unfold Sinl_Rep_def Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	78	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	79	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	80
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	81	lemma noteq_IsinlIsinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	82	"Isinl(a)=Isinr(b) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	83	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	84	apply (rule noteq_SinlSinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	85	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	86	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	87	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	88	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	89
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	90	text {* injectivity of @{term Sinl_Rep}, @{term Sinr_Rep} and @{term Isinl}, @{term Isinr} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	91
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	92	lemma inject_Sinl_Rep1: "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	93	apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	94	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	95	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	96
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	97	lemma inject_Sinr_Rep1: "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	98	apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	99	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	100	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	101
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	102	lemma inject_Sinl_Rep2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	103	"[\| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) \|] ==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	104	apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	105	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	106	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	107
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	108	lemma inject_Sinr_Rep2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	109	"[\|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) \|] ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	110	apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	111	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	112	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	113
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	114	lemma inject_Sinl_Rep: "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	115	apply (case_tac "a1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	116	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	117	apply (rule inject_Sinl_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	118	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	119	apply (case_tac "a2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	120	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	121	apply (drule inject_Sinl_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	122	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	123	apply (erule inject_Sinl_Rep2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	124	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	125	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	126	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	127
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	128	lemma inject_Sinr_Rep: "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	129	apply (case_tac "b1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	130	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	131	apply (rule inject_Sinr_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	132	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	133	apply (case_tac "b2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	134	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	135	apply (drule inject_Sinr_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	136	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	137	apply (erule inject_Sinr_Rep2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	138	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	139	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	140	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	141
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	142	lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	143	apply (unfold Isinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	144	apply (rule inject_Sinl_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	145	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	146	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	147	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	148	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	149
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	150	lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	151	apply (unfold Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	152	apply (rule inject_Sinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	153	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	154	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	155	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	156	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	157
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	158	declare inject_Isinl [dest!] inject_Isinr [dest!]
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	159	declare noteq_IsinlIsinr [dest!]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	160	declare noteq_IsinlIsinr [OF sym, dest!]
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	161
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	162	lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	163	by blast
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	164
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	165	lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	166	by blast
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	167
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	168	text {* Exhaustion of the strict sum @{typ "'a ++ 'b"} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	169	text {* choice of the bottom representation is arbitrary *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	170
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	171	lemma Exh_Ssum:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	172	"z=Isinl(UU) \| (? a. z=Isinl(a) & a~=UU) \| (? b. z=Isinr(b) & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	173	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	174	apply (rule Rep_Ssum[unfolded Ssum_def, THEN CollectE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	175	apply (erule disjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	176	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	177	apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	178	apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	179	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	180	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	181	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	182	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	183	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	184	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	185	apply (rule_tac Q = "Sinl_Rep (a) =Sinl_Rep (UU) " in contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	186	apply (erule_tac [2] arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	187	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	188	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	189	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	190	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	191	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	192	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	193	apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	194	apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	195	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	196	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	197	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	198	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	199	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	200	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	201	apply (rule_tac Q = "Sinr_Rep (b) =Sinl_Rep (UU) " in contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	202	prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	203	apply (rule strict_SinlSinr_Rep [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	204	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	205	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	206	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	207	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	208	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	209	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	210
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	211	text {* elimination rules for the strict sum @{typ "'a ++ 'b"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	212
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	213	lemma IssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	214	"[\|p=Isinl(UU) ==> Q ;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	215	!!x.[\|p=Isinl(x); x~=UU \|] ==> Q;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	216	!!y.[\|p=Isinr(y); y~=UU \|] ==> Q\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	217	apply (rule Exh_Ssum [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	218	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	219	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	220
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	221	lemma IssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	222	"[\| !!x. [\| p = Isinl(x) \|] ==> Q; !!y. [\| p = Isinr(y) \|] ==> Q \|] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	223	apply (rule IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	224	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	225	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	226
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	227	text {* rewrites for @{term Iwhen} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	228
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	229	lemma Iwhen1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	230	"Iwhen f g (Isinl UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	231	apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	232	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	233	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	234	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	235	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	236	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	237	apply (rule_tac P = "a=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	238	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	239	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	240	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	241	apply fast
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 = "b=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	244	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	245	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	246	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	247	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	248	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	249	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	250	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	251
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 Iwhen2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	254	"x~=UU ==> Iwhen f g (Isinl x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	255	apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	256	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	257	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	258	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	259	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	260	apply (rule_tac P = "x=UU" in notE)
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 (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	263	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	264	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	265	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	266	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	267	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	268	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	269	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	270	apply (rule_tac P = "Isinl (x) = Isinr (b) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	271	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	272	apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	273	apply (erule_tac [2] noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	274	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	275	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	276
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	277	lemma Iwhen3:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	278	"y~=UU ==> Iwhen f g (Isinr y) = g$y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	279	apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	280	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	281	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	282	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	283	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	284	apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	285	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	286	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	287	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	288	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	289	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	290	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	291	apply (rule_tac P = "Isinr (y) = Isinl (a) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	292	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	293	apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	294	apply (erule_tac [2] sym [THEN noteq_IsinlIsinr])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	295	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	296	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	297	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	298	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	299	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	300	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	301
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	302	text {* instantiate the simplifier *}
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	lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	305
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	306	declare Ssum0_ss [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	307
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	308	subsection {* Ordering for type @{typ "'a ++ 'b"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	309
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	310	instance "++"::(pcpo, pcpo) sq_ord ..
15576 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	defs (overloaded)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	313	less_ssum_def: "(op <<) == (%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	314	(! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	315	&(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	316	&(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	317	&(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	318
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	319	lemma less_ssum1a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	320	"[\|s1=Isinl(x::'a); s2=Isinl(y::'a)\|] ==> s1 << s2 = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	321	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	322	apply (rule some_equality)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	323	prefer 2 apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	324	apply (safe elim!: UU_I)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	325	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	326
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	327	lemma less_ssum1b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	328	"[\|s1=Isinr(x::'b); s2=Isinr(y::'b)\|] ==> s1 << s2 = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	329	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	330	apply (rule some_equality)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	331	prefer 2 apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	332	apply (safe elim!: UU_I)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	333	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	334
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	335	lemma less_ssum1c:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	336	"[\|s1=Isinl(x::'a); s2=Isinr(y::'b)\|] ==> s1 << s2 = ((x::'a) = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	337	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	338	apply (rule some_equality)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	339	prefer 2
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	340	apply (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	341	apply (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	342	apply (drule conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	343	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	344	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	345	apply (erule mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	346	apply fast
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	347	apply (safe elim!: UU_I)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	348	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	349
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	350	lemma less_ssum1d:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	351	"[\|s1=Isinr(x); s2=Isinl(y)\|] ==> s1 << s2 = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	352	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	353	apply (rule some_equality)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	354	prefer 2
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	355	apply (drule conjunct2)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	356	apply (drule conjunct2)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	357	apply (drule conjunct2)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	358	apply (drule spec)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	359	apply (drule spec)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	360	apply (erule mp)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	361	apply fast
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	362	apply (safe elim!: UU_I)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	363	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	364
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	365	text {* optimize lemmas about @{term less_ssum} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	366
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	367	lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	368	apply (rule less_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	369	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	370	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	371	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	372
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	373	lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	374	apply (rule less_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	375	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	376	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	377	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	378
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	379	lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	380	apply (rule less_ssum1c)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	381	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	382	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	383	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	384
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	385	lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	386	apply (rule less_ssum1d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	387	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	388	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	389	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	390
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	391	subsection {* Type @{typ "'a ++ 'b"} is a partial order *}
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 refl_less_ssum: "(p::'a++'b) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	394	apply (rule_tac p = "p" in IssumE2)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	395	apply (simp add: less_ssum2a)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	396	apply (simp add: less_ssum2b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	397	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	398
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	399	lemma antisym_less_ssum: "[\|(p1::'a++'b) << p2; p2 << p1\|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	400	apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	401	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	402	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	403	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	404	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	405	apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	406	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	407	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	408	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	409	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	410	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	411	apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	412	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	413	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	414	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	415	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	416	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	417	apply (rule strict_IsinlIsinr [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	418	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	419	apply (rule_tac f = "Isinr" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	420	apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	421	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	422	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	423	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	424
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	425	lemma trans_less_ssum: "[\|(p1::'a++'b) << p2; p2 << p3\|] ==> p1 << p3"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	426	apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	427	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	428	apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	429	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	430	apply (rule less_ssum2a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	431	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	432	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	433	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	434	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	435	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	436	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	437	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	438	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	439	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	440	apply (rule less_ssum2c [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	441	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	442	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	443	apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	444	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	445	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	446	apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	447	apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	448	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	449	apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	450	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	451	apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	452	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	453	apply (rule less_ssum2d [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	454	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	455	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	456	apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	457	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	458	apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	459	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	460	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	461	apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	462	apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	463	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	464	apply (rule less_ssum2b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	465	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	466	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	467	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	468	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	469	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	470	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	471	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	472	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	473	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	474
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	475	instance "++" :: (pcpo, pcpo) po
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	476	by intro_classes
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	477	(assumption \| rule refl_less_ssum antisym_less_ssum trans_less_ssum)+
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	478
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	479	text {* for compatibility with old HOLCF-Version *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	480	lemma inst_ssum_po: "(op <<)=(%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	481	(! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	482	&(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	483	&(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	484	&(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	485	apply (fold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	486	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	487	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	488
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	489	subsection {* Type @{typ "'a ++ 'b"} is pointed *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	490
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	491	lemma minimal_ssum: "Isinl UU << s"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	492	apply (rule_tac p = "s" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	493	apply simp
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	494	apply (rule less_ssum2a [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	495	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	496	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	497	apply (subst strict_IsinlIsinr)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	498	apply (rule less_ssum2b [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	499	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	500	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	501
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	502	lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	503
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	504	lemma least_ssum: "? x::'a++'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	505	apply (rule_tac x = "Isinl UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	506	apply (rule minimal_ssum [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	507	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	508
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	509	subsection {* Monotonicity of @{term Isinl}, @{term Isinr}, @{term Iwhen} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	510
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	511	text {* @{term Isinl} and @{term Isinr} are monotone *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	512
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	513	lemma monofun_Isinl: "monofun(Isinl)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	514	by (simp add: monofun less_ssum2a)
15576 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	lemma monofun_Isinr: "monofun(Isinr)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	517	by (simp add: monofun less_ssum2b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	518
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	519	text {* @{term Iwhen} is monotone in all arguments *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	520
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	521	lemma monofun_Iwhen1: "monofun(Iwhen)"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	522	apply (rule monofunI [rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	523	apply (rule less_fun [THEN iffD2, rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	524	apply (rule less_fun [THEN iffD2, rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	525	apply (rule_tac p = "xb" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	526	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	527	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	528	apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	529	apply simp
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 monofun_Iwhen2: "monofun(Iwhen(f))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	533	apply (rule monofunI [rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	534	apply (rule less_fun [THEN iffD2, rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	535	apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	536	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	537	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	538	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	539	apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	540	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	541
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	542	lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	543	apply (rule monofunI [rule_format])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	544	apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	545	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	546	apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	547	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	548	apply (rule_tac P = "xa=UU" in notE)
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 (rule UU_I)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	551	apply (rule less_ssum2a [THEN iffD1])
15576 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	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	554	apply (rule monofun_cfun_arg)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	555	apply (erule less_ssum2a [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	556	apply (simp del: Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	557	apply (rule_tac s = "UU" and t = "xa" in subst)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	558	apply (erule less_ssum2c [THEN iffD1, symmetric])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	559	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	560	apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	561	apply simp
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	562	apply (simp only: less_ssum2d)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	563	apply (simp only: less_ssum2d)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	564	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	565	apply (rule monofun_cfun_arg)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	566	apply (erule less_ssum2b [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	567	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	568
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	569	text {* some kind of exhaustion rules for chains in @{typ "'a ++ 'b"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	570
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	571	lemma ssum_lemma1: "[\|~(!i.? x. Y(i::nat)=Isinl(x))\|] ==> (? i.! x. Y(i)~=Isinl(x))"
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	572	by fast
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	573
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	574	lemma ssum_lemma2: "[\|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))\|]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	575	==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	576	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	577	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	578	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	579	apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	580	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	581	apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	582	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	583	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	584
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	585	lemma ssum_lemma3: "[\|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)\|]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	586	==> (!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	587	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	588	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	589	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	590	apply (rule_tac p = "Y (ia) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	591	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	592	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	593	apply (rule_tac [2] strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	594	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	595	apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	596	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	597	apply (rule_tac m = "i" and n = "ia" in nat_less_cases)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	598	prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	599	apply (rule exI, rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	600	apply (erule_tac P = "x=UU" in notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	601	apply (rule less_ssum2d [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	602	apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	603	apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	604	apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	605	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	606	apply (erule_tac P = "xa=UU" in notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	607	apply (rule less_ssum2c [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	608	apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	609	apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	610	apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	611	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	612	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	613
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	614	lemma ssum_lemma4: "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))\|(!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	615	apply (rule case_split_thm)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	616	apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	617	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	618	apply (erule ssum_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	619	apply (rule ssum_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	620	apply (erule ssum_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	621	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	622
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	623	text {* restricted surjectivity of @{term Isinl} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	624
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	625	lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	626	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	627	apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	628	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	629	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	630	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	631
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	632	text {* restricted surjectivity of @{term Isinr} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	633
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	634	lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	635	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	636	apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	637	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	638	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	639	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	640
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	641	text {* technical lemmas *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	642
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	643	lemma ssum_lemma7: "[\|Isinl(x) << z; x~=UU\|] ==> ? y. z=Isinl(y) & y~=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	644	apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	645	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	646	apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	647	apply (rule antisym_less)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	648	apply (erule less_ssum2a [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	649	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	650	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	651	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	652	apply (rule notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	653	apply (erule_tac [2] less_ssum2c [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	654	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	655	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	656
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	657	lemma ssum_lemma8: "[\|Isinr(x) << z; x~=UU\|] ==> ? y. z=Isinr(y) & y~=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	658	apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	659	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	660	apply (erule notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	661	apply (erule less_ssum2d [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	662	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	663	apply (rule notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	664	apply (erule_tac [2] less_ssum2d [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	665	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	666	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	667	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	668
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	669	subsection {* Type @{typ "'a ++ 'b"} is a cpo in three steps *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	670
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	671	lemma lub_ssum1a: "[\|chain(Y);(!i.? x. Y(i)=Isinl(x))\|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	672	range(Y) <<\| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	673	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	674	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	675	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	676	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	677	apply (rule_tac t = "Y (i) " in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	678	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	679	apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	680	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	681	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	682	apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	683	apply (rule_tac t = "u" in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	684	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	685	apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	686	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	687	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	688	apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	689	apply simp
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	690	apply (rule less_ssum2c [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	691	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	692	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	693	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	694	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	695	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	696	apply (erule notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	697	apply (rule less_ssum2c [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	698	apply (rule_tac t = "Isinl (x) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	699	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	700	apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	701	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	702	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	703
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	704	lemma lub_ssum1b: "[\|chain(Y);(!i.? x. Y(i)=Isinr(x))\|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	705	range(Y) <<\| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	706	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	707	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	708	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	709	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	710	apply (rule_tac t = "Y (i) " in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	711	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	712	apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	713	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	714	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	715	apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	716	apply simp
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	717	apply (rule less_ssum2d [THEN iffD2])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	718	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	719	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	720	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	721	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	722	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	723	apply (erule notE)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	724	apply (rule less_ssum2d [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	725	apply (rule_tac t = "Isinr (y) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	726	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	727	apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	728	apply (rule_tac t = "u" in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	729	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	730	apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	731	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	732	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	733	apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	734	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	735
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	736	lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	737	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	738	[\| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	739	lub (range ?Y1) = Isinl
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	740	(lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	741	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	742
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	743	lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	744	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	745	[\| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	746	lub (range ?Y1) = Isinr
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	747	(lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	750	lemma cpo_ssum: "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<\|x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	751	apply (rule ssum_lemma4 [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	752	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	753	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	754	apply (erule lub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	755	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	756	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	757	apply (erule lub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	758	apply assumption
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
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	761	instance "++" :: (pcpo, pcpo) cpo
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	762	by intro_classes (rule cpo_ssum)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	763
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	764	instance "++" :: (pcpo, pcpo) pcpo
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	765	by intro_classes (rule least_ssum)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	766
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	767	text {* for compatibility with old HOLCF-Version *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	768	lemma inst_ssum_pcpo: "UU = Isinl UU"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	769	apply (simp add: UU_def UU_ssum_def)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	770	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	771
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	772	declare inst_ssum_pcpo [symmetric, simp]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	773
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	774	subsection {* Continuous versions of constants *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	775
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	776	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	777	sinl :: "'a -> ('a++'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	778	sinr :: "'b -> ('a++'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	779	sscase :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	780
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	781	defs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	782
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	783	sinl_def: "sinl == (LAM x. Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	784	sinr_def: "sinr == (LAM x. Isinr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	785	sscase_def: "sscase == (LAM f g s. Iwhen(f)(g)(s))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	786
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	787	translations
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	788	"case s of sinl$x => t1 \| sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	789
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	790	text {* continuity for @{term Isinl} and @{term Isinr} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	791
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	792	lemma contlub_Isinl: "contlub(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	793	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	794	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	795	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	796	apply (rule_tac [2] thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	797	apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	798	apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	799	apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	800	apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	801	apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	802	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	803	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	804	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	805	apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	806	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	807	apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	808	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	809	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	810	apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	811	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	812	apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	813	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	814	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	815	apply (erule monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	816	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	817	apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	818	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	819	apply (rule Iwhen1[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	820	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	821	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	822
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	823	lemma contlub_Isinr: "contlub(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	824	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	825	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	826	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	827	apply (rule_tac [2] thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	828	apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	829	apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	830	apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	831	apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	832	apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	833	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	834	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	835	apply (rule arg_cong, rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	836	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	837	apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	838	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	839	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	840	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	841	apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	842	apply (rule arg_cong, rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	843	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	844	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	845	apply (erule monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	846	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	847	apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	848	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	849	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	850	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	851
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	852	lemma cont_Isinl [iff]: "cont(Isinl)"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	853	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	854	apply (rule monofun_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	855	apply (rule contlub_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	856	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	857
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	858	lemma cont_Isinr [iff]: "cont(Isinr)"
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	859	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	860	apply (rule monofun_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	861	apply (rule contlub_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	862	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	863
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	864	text {* continuity for @{term Iwhen} in the first two arguments *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	865
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	866	lemma contlub_Iwhen1: "contlub(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	867	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	868	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	869	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	870	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	871	apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	872	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	873	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	874	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	875	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	876	apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	877	apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	878	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	879	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	880	apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	881	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	882	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	883	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	884	apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	885	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	886	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	887	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	888
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	889	lemma contlub_Iwhen2: "contlub(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	890	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	891	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	892	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	893	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	894	apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	895	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	896	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	897	apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	898	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	899	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	900	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	901	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	902	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	903	apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	904	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	905
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	906	text {* continuity for @{term Iwhen} in its third argument *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	907
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	908	text {* first 5 ugly lemmas *}
15576 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	lemma ssum_lemma9: "[\| chain(Y); lub(range(Y)) = Isinl(x)\|] ==> !i.? x. Y(i)=Isinl(x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	911	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	912	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	913	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	914	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	915	apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	916	apply assumption
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	917	apply (rule less_ssum2d [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	918	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	919	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	920	apply (erule is_ub_thelub)
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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	923	lemma ssum_lemma10: "[\| chain(Y); lub(range(Y)) = Isinr(x)\|] ==> !i.? x. Y(i)=Isinr(x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	924	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	925	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	926	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	927	apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	928	apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	929	apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	930	apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	931	apply assumption
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	932	apply (rule less_ssum2c [THEN iffD1])
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	933	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	934	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	935	apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	936	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	937
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	938	lemma ssum_lemma11: "[\| chain(Y); lub(range(Y)) = Isinl(UU) \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	939	Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	940	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	941	apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	942	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	943	apply (rule_tac s = "Isinl (UU) " and t = "Y (i) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	944	apply (rule inst_ssum_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	945	apply (rule chain_UU_I [THEN spec, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	946	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	947	apply (erule inst_ssum_pcpo [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	948	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	949	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	950
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	951	lemma ssum_lemma12: "[\| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	952	Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	953	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	954	apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	955	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	956	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	957	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	958	apply (rule thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	959	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	960	apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	961	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	962	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	963	apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	964	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	965	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	966	apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	967	apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	968	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	969	apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	970	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	971	apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	972	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	973	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	974	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	975	apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	976	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	977	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	978	apply (rule ssum_lemma9 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	979	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	980	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	981	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	982	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	983	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	984	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	985	apply (rule Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	986	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	987	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	988	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	989	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	990	apply (subst Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	991	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	992	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	993	apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	994	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	995	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	996	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	997
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	998	lemma ssum_lemma13: "[\| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	999	Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1000	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1001	apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1002	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1003	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1004	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1005	apply (rule thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1006	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1007	apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1008	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1009	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1010	apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1011	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1012	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1013	apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1014	apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1015	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1016	apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1017	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1018	apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1019	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1020	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1021	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1022	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1023	apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1024	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1025	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1026	apply (rule ssum_lemma10 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1027	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1028	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1029	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1030	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1031	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1032	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1033	apply (rule Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1034	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1035	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1036	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1037	apply (subst Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1038	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1039	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1040	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1041	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1042	apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1043	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1044	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1045	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1046
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1047	lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1048	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1049	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1050	apply (rule_tac p = "lub (range (Y))" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1051	apply (erule ssum_lemma11)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1052	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1053	apply (erule ssum_lemma12)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1054	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1055	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1056	apply (erule ssum_lemma13)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1057	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1058	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1059	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1060
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1061	lemma cont_Iwhen1: "cont(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1062	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1063	apply (rule monofun_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1064	apply (rule contlub_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1065	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1066
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1067	lemma cont_Iwhen2: "cont(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1068	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1069	apply (rule monofun_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1070	apply (rule contlub_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1071	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1072
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1073	lemma cont_Iwhen3: "cont(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1074	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1075	apply (rule monofun_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1076	apply (rule contlub_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1077	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1078
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1079	text {* continuous versions of lemmas for @{typ "'a ++ 'b"} *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1080
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1081	lemma strict_sinl [simp]: "sinl$UU =UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1082	apply (unfold sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1083	apply (simp add: cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1084	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1085
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1086	lemma strict_sinr [simp]: "sinr$UU=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1087	apply (unfold sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1088	apply (simp add: cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1089	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1090
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1091	lemma noteq_sinlsinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1092	"sinl$a=sinr$b ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1093	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1094	apply (auto dest!: noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1095	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1096
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1097	lemma inject_sinl:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1098	"sinl$a1=sinl$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1099	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1100	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1101	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1102
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1103	lemma inject_sinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1104	"sinr$a1=sinr$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1105	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1106	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1107	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1108
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1109	declare inject_sinl [dest!] inject_sinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1110
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1111	lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1112	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1113	apply (rule inject_sinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1114	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1115	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1116
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1117	lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1118	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1119	apply (rule inject_sinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1120	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1121	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1122
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1123	lemma Exh_Ssum1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1124	"z=UU \| (? a. z=sinl$a & a~=UU) \| (? b. z=sinr$b & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1125	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1126	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1127	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1128	apply (rule Exh_Ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1129	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1130
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1131	lemma ssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1132	assumes major: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1133	assumes prem2: "!!x.[\|p=sinl$x; x~=UU \|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1134	assumes prem3: "!!y.[\|p=sinr$y; y~=UU \|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1135	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1136	apply (rule major [THEN IssumE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1137	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1138	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1139	apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1140	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1141	apply (simp add: sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1142	apply (rule prem3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1143	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1144	apply (simp add: sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1145	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1146
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1147
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1148	lemma ssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1149	assumes preml: "!!x.[\|p=sinl$x\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1150	assumes premr: "!!y.[\|p=sinr$y\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1151	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1152	apply (rule IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1153	apply (rule preml)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1154	apply (rule_tac [2] premr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1155	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1156	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1157	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1158
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1159	lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1160	cont_Iwhen3 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1161
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1162	lemma sscase1 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1163	"sscase$f$g$UU = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1164	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1165	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1166	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1167	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1168	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1169	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1170	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1171	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1172	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1173	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1174
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1175	lemma sscase2 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1176	"x~=UU==> sscase$f$g$(sinl$x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1177	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1178	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1179	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1180	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1181	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1182	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1183	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1184	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1185	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1186	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1187	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1188
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1189	lemma sscase3 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1190	"x~=UU==> sscase$f$g$(sinr$x) = g$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1191	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1192	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1193	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1194	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1195	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1196	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1197	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1198	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1199	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1200	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1201	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1202
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1203	lemma less_ssum4a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1204	"(sinl$x << sinl$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1205	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1206	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1207	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1208	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1209	apply (rule cont_Isinl)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1210	apply (rule less_ssum2a)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1211	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1212
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1213	lemma less_ssum4b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1214	"(sinr$x << sinr$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1215	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1216	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1217	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1218	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1219	apply (rule cont_Isinr)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1220	apply (rule less_ssum2b)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1221	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1222
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1223	lemma less_ssum4c:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1224	"(sinl$x << sinr$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1225	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1226	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1227	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1228	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1229	apply (rule cont_Isinl)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1230	apply (rule less_ssum2c)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1231	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1232
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1233	lemma less_ssum4d:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1234	"(sinr$x << sinl$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1235	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1236	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1237	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1238	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1239	apply (rule cont_Isinr)
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1240	apply (rule less_ssum2d)
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1241	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1242
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1243	lemma ssum_chainE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1244	"chain(Y) ==> (!i.? x.(Y i)=sinl$x)\|(!i.? y.(Y i)=sinr$y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1245	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1246	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1247	apply (erule ssum_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1248	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1249
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1250	lemma thelub_ssum2a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1251	"[\| chain(Y); !i.? x. Y(i) = sinl$x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1252	lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1253	apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1254	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1255	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1256	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1257	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1258	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1259	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1260	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1261	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1262	apply (rule thelub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1263	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1264	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1265	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1266	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1267	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1268	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1269	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1270	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1271	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1272
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1273	lemma thelub_ssum2b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1274	"[\| chain(Y); !i.? x. Y(i) = sinr$x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1275	lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1276	apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1277	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1278	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1279	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1280	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1281	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1282	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1283	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1284	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1285	apply (rule thelub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1286	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1287	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1288	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1289	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1290	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1291	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1292	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1293	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1294	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1295
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1296	lemma thelub_ssum2a_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1297	"[\| chain(Y); lub(range(Y)) = sinl$x\|] ==> !i.? x. Y(i)=sinl$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1298	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1299	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1300	apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1301	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1302	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1303
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1304	lemma thelub_ssum2b_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1305	"[\| chain(Y); lub(range(Y)) = sinr$x\|] ==> !i.? x. Y(i)=sinr$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1306	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1307	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1308	apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1309	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1310	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1311
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1312	lemma thelub_ssum3: "chain(Y) ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1313	lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1314	\| lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1315	apply (rule ssum_chainE [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1316	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1317	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1318	apply (erule thelub_ssum2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1319	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1320	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1321	apply (erule thelub_ssum2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1322	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1323	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1324
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1325	lemma sscase4: "sscase$sinl$sinr$z=z"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1326	apply (rule_tac p = "z" in ssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1327	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1328	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1329
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1330	text {* install simplifier for Ssum *}
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1331
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1332	lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1333	sscase1 sscase2 sscase3
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1334
15593 24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1335	text {* for backward compatibility *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1336
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1337	lemmas less_ssum3a = less_ssum2a
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1338	lemmas less_ssum3b = less_ssum2b
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1339	lemmas less_ssum3c = less_ssum2c
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1340	lemmas less_ssum3d = less_ssum2d
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs huffman parents: 15577 diff changeset	1341
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1342	end

author	huffman
	Tue, 08 Mar 2005 00:32:10 +0100
changeset 15593	24d770bbc44a
parent 15577	e16da3068ad6
child 15600	a59f07556a8d
permissions	-rw-r--r--