isabelle: src/HOLCF/Ssum.thy@efb95d0d01f7 (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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	11	theory Ssum = Cfun:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	12
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	13	constdefs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	14	Sinl_Rep :: "['a,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	15	"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	16	Sinr_Rep :: "['b,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	17	"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	18
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	19	typedef (Ssum) ('a, 'b) "++" (infixr 10) =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	20	"{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	21	by auto
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	syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	24	"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	25	syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	26	"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	27
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	28	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	29	Isinl :: "'a => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	30	Isinr :: "'b => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	31	Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	32
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	33	defs (defining the abstract constants)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	34	Isinl_def: "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	35	Isinr_def: "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	36
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	37	Iwhen_def: "Iwhen(f)(g)(s) == @z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	38	(s=Isinl(UU) --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	39	&(!a. a~=UU & s=Isinl(a) --> z=f$a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	40	&(!b. b~=UU & s=Isinr(b) --> z=g$b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	41
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	42	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	43	(* A non-emptyness result for Sssum *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	44	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	45
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	46	lemma SsumIl: "Sinl_Rep(a):Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	47	apply (unfold Ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	48	apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	49	done
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"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	52	apply (unfold Ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	53	apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	54	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	55
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	56	lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	57	apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	58	apply (erule Abs_Ssum_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	59	done
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	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	62	(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	63	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	64
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	65	lemma strict_SinlSinr_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	66	"Sinl_Rep(UU) = Sinr_Rep(UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	67	apply (unfold Sinr_Rep_def Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	68	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	69	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	70	apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	71	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	72	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	73
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	74	lemma strict_IsinlIsinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	75	"Isinl(UU) = Isinr(UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	76	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	77	apply (rule strict_SinlSinr_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	78	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	79
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	80
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	81	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	82	(* distinctness of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	83	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	84
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	85	lemma noteq_SinlSinr_Rep:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	86	"(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	87	apply (unfold Sinl_Rep_def Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	88	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	89	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	90
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 noteq_IsinlIsinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	93	"Isinl(a)=Isinr(b) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	94	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	95	apply (rule noteq_SinlSinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	96	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	97	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	98	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	99	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	100
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	101
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	102
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	103	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	104	(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	105	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	106
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	107	lemma 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	108	apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	109	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	110	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	111
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	112	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	113	apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	114	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	115	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	116
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	117	lemma inject_Sinl_Rep2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	118	"[\| 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	119	apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	120	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	121	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	122
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	123	lemma inject_Sinr_Rep2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	124	"[\|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	125	apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	126	apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	127	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	128
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	129	lemma 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	130	apply (case_tac "a1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	131	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	132	apply (rule inject_Sinl_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	133	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	134	apply (case_tac "a2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	135	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	136	apply (drule inject_Sinl_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	137	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	138	apply (erule inject_Sinl_Rep2)
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	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	141	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	142
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	143	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	144	apply (case_tac "b1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	145	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	146	apply (rule inject_Sinr_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	147	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	148	apply (case_tac "b2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	149	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	150	apply (drule inject_Sinr_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	151	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	152	apply (erule inject_Sinr_Rep2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	153	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	154	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	155	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	156
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	157	lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	158	apply (unfold Isinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	159	apply (rule inject_Sinl_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	160	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	161	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	162	apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	163	done
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: "Isinr(b1)=Isinr(b2) ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	166	apply (unfold Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	167	apply (rule inject_Sinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	168	apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	169	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	170	apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	171	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	172
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	173	declare inject_Isinl [dest!] inject_Isinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	174
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	175	lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	176	apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	177	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	178
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	179	lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	180	apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	181	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	182
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	183	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	184	(* Exhaustion of the strict sum ++ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	185	(* choice of the bottom representation is arbitrary *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	186	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	187
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	188	lemma Exh_Ssum:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	189	"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	190	apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	191	apply (rule Rep_Ssum[unfolded Ssum_def, THEN CollectE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	192	apply (erule disjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	193	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	194	apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	195	apply (erule disjI1)
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 disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	198	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	199	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	200	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	201	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	202	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	203	apply (erule_tac [2] arg_cong)
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	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	210	apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	211	apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	212	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	213	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	214	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	215	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	216	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	217	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	218	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	219	prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	220	apply (rule strict_SinlSinr_Rep [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	221	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	222	apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	223	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	224	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	225	apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	226	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	227
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	(* elimination rules for the strict sum ++ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	230	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	231
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	232	lemma IssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	233	"[\|p=Isinl(UU) ==> Q ;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	234	!!x.[\|p=Isinl(x); x~=UU \|] ==> Q;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	235	!!y.[\|p=Isinr(y); y~=UU \|] ==> Q\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	236	apply (rule Exh_Ssum [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	237	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	238	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	239
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	240	lemma IssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	241	"[\| !!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	242	apply (rule IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	243	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	244	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	245
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	246
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	247
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	248
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	249	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	250	(* rewrites for Iwhen *)
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 Iwhen1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	254	"Iwhen f g (Isinl UU) = UU"
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	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	258	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	259	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	260	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	261	apply (rule_tac P = "a=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	262	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	263	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	264	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	265	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	266	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	267	apply (rule_tac P = "b=UU" in notE)
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 (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	270	apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	271	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	272	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	273	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	274	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	275
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	276
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	277	lemma Iwhen2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	278	"x~=UU ==> Iwhen f g (Isinl x) = f$x"
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 = "x=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_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	287	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	288	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	289	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	290	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	291	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	292	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	293	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	294	apply (rule_tac P = "Isinl (x) = Isinr (b) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	295	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	296	apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	297	apply (erule_tac [2] noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	298	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	299	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	300
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	301	lemma Iwhen3:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	302	"y~=UU ==> Iwhen f g (Isinr y) = g$y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	303	apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	304	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	305	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	306	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	307	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	308	apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	309	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	310	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	311	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	312	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	313	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	314	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	315	apply (rule_tac P = "Isinr (y) = Isinl (a) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	316	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	317	apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	318	apply (erule_tac [2] sym [THEN noteq_IsinlIsinr])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	319	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	320	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	321	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	322	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	323	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	324	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	325
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	(* instantiate the simplifier *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	328	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	329
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	330	lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	331
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	332	declare Ssum0_ss [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	333
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	334	(* Partial ordering for the strict sum ++ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	335
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	336	instance "++"::(pcpo,pcpo)sq_ord ..
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	337
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	338	defs (overloaded)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	339	less_ssum_def: "(op <<) == (%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	340	(! 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	341	&(! 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	342	&(! 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	343	&(! 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	344
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	345	lemma less_ssum1a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	346	"[\|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	347	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	348	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	349	apply (drule_tac [2] conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	350	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	351	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	352	apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	353	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	354	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	355	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	356	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	357	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	358	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	359	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	360	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	361	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	362	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	363	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	364	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	365	apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	366	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	367	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	368	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	369	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	370	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	371	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	372	apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	373	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	374	apply (rule eq_UU_iff[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	375	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	376	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	377	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	378	apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	379	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	380	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	381
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	382
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	383	lemma less_ssum1b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	384	"[\|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	385	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	386	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	387	apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	388	apply (drule_tac [2] conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	389	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	390	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	391	apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	392	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	393	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	394	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	395	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	396	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	397	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	398	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	399	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	400	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	401	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	402	apply (erule conjE)
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 (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	405	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	406	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	407	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	408	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	409	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	410	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	411	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	412	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	413	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	414	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	415	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	416	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	417	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	418	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	419	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	420	apply (rule eq_UU_iff[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	421	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	422
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	423
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	424	lemma less_ssum1c:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	425	"[\|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	426	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	427	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	428	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	429	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	430	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	431	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	432	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	433	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	434	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	435	apply (rule eq_UU_iff)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	436	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	437	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	438	apply (erule conjE)
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 (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	441	apply (drule inject_Isinr)
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 conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	444	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	445	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	446	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	447	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	448	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	449	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	450	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	451	apply (erule conjE)
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 (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	454	apply (drule noteq_IsinlIsinr)
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 (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	457	apply (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	458	apply (drule conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	459	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	460	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	461	apply (erule mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	462	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	463	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	464
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	465
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	466	lemma less_ssum1d:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	467	"[\|s1=Isinr(x); s2=Isinl(y)\|] ==> s1 << s2 = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	468	apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	469	apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	470	apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	471	apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	472	apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	473	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	474	apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	475	apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	476	prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	477	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	478	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	479	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	480	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	481	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	482	apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	483	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	484	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	485	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	486	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	487	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	488	apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	489	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	490	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	491	apply (rule eq_UU_iff)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	492	apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	493	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	494	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	495	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	496	apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	497	apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	498	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	499	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	500	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	501	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	502	apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	503	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	504	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	505
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	506
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	507	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	508	(* optimize lemmas about less_ssum *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	509	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	510
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	511	lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	512	apply (rule less_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	513	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	514	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	515	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	516
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	517	lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	518	apply (rule less_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	519	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	520	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	521	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	522
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	523	lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	524	apply (rule less_ssum1c)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	525	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	526	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	527	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	528
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	529	lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	530	apply (rule less_ssum1d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	531	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	532	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	533	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	534
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	535
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	536	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	537	(* less_ssum is a partial order on ++ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	538	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	539
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	540	lemma refl_less_ssum: "(p::'a++'b) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	541	apply (rule_tac p = "p" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	542	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	543	apply (rule less_ssum2a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	544	apply (rule refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	545	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	546	apply (rule less_ssum2b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	547	apply (rule refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	548	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	549
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	550	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	551	apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	552	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	553	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	554	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	555	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	556	apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	557	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	558	apply (erule less_ssum2a [THEN iffD1])
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 (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	561	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	562	apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	563	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	564	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	565	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	566	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	567	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	568	apply (rule strict_IsinlIsinr [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	569	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	570	apply (rule_tac f = "Isinr" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	571	apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	572	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	573	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	574	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	575
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	576	lemma 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	577	apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	578	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	579	apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	580	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	581	apply (rule less_ssum2a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	582	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	583	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	584	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	585	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	586	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	587	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	588	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	589	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	590	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	591	apply (rule less_ssum2c [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	592	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	593	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	594	apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	595	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	596	apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	597	apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	598	apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	599	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	600	apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	601	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	602	apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	603	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	604	apply (rule less_ssum2d [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	605	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	606	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	607	apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	608	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	609	apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	610	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	611	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	612	apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	613	apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	614	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	615	apply (rule less_ssum2b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	616	apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	617	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	618	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	619	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	620	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	621	apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	622	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	623	apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	624	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	625
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	626	(* Class Instance ++::(pcpo,pcpo)po *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	627
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	628	instance "++"::(pcpo,pcpo)po
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	629	apply (intro_classes)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	630	apply (rule refl_less_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	631	apply (rule antisym_less_ssum, assumption+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	632	apply (rule trans_less_ssum, assumption+)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	633	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	634
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	635	(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	636	lemma inst_ssum_po: "(op <<)=(%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	637	(! 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	638	&(! 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	639	&(! 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	640	&(! 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	641	apply (fold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	642	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	643	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	644
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	645	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	646	(* access to less_ssum in class po *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	647	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	648
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	649	lemma less_ssum3a: "Isinl x << Isinl y = x << y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	650	apply (simp (no_asm) add: less_ssum2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	651	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	652
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	653	lemma less_ssum3b: "Isinr x << Isinr y = x << y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	654	apply (simp (no_asm) add: less_ssum2b)
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 less_ssum3c: "Isinl x << Isinr y = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	658	apply (simp (no_asm) add: less_ssum2c)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	659	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	660
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	661	lemma less_ssum3d: "Isinr x << Isinl y = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	662	apply (simp (no_asm) add: less_ssum2d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	663	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	664
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	665	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	666	(* type ssum ++ is pointed *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	667	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	668
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	669	lemma minimal_ssum: "Isinl UU << s"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	670	apply (rule_tac p = "s" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	671	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	672	apply (rule less_ssum3a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	673	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	674	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	675	apply (subst strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	676	apply (rule less_ssum3b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	677	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	678	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	679
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	680	lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	681
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	682	lemma least_ssum: "? x::'a++'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	683	apply (rule_tac x = "Isinl UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	684	apply (rule minimal_ssum [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	685	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	686
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	687	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	688	(* Isinl, Isinr are monotone *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	689	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	690
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	691	lemma monofun_Isinl: "monofun(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	692	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	693	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	694	apply (erule less_ssum3a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	695	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	696
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	697	lemma monofun_Isinr: "monofun(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	698	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	699	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	700	apply (erule less_ssum3b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	701	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	702
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	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	705	(* Iwhen is monotone in all arguments *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	706	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	707
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	708
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	709	lemma monofun_Iwhen1: "monofun(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	710	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	711	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	712	apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	713	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	714	apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	715	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	716	apply (rule_tac p = "xb" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	717	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	718	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	719	apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	720	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	721	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	722
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	723	lemma monofun_Iwhen2: "monofun(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	724	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	725	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	726	apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	727	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	728	apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	729	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	730	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	731	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	732	apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	733	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	734
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	735	lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	736	apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	737	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	738	apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	739	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	740	apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	741	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	742	apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	743	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	744	apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	745	apply (rule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	746	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	747	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	748	apply (rule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	749	apply (erule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	750	apply (simp del: Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	751	apply (rule_tac s = "UU" and t = "xa" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	752	apply (erule less_ssum3c [THEN iffD1, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	753	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	754	apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	755	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	756	apply (simp only: less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	757	apply (simp only: less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	758	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	759	apply (rule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	760	apply (erule less_ssum3b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	761	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	762
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	763
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	764	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	765	(* some kind of exhaustion rules for chains in 'a ++ 'b *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	766	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	767
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	768	lemma ssum_lemma1: "[\|~(!i.? x. Y(i::nat)=Isinl(x))\|] ==> (? i.! x. Y(i)~=Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	769	apply fast
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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	772	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	773	==> (? 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	774	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	775	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	776	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	777	apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	778	apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	779	apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	780	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	781	done
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
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	784	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	785	==> (!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	786	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	787	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	788	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	789	apply (rule_tac p = "Y (ia) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	790	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	791	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	792	apply (rule_tac [2] strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	793	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	794	apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	795	apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	796	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	797	prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	798	apply (rule exI, rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	799	apply (erule_tac P = "x=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	800	apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	801	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	802	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	803	apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	804	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	805	apply (erule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	806	apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	807	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	808	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	809	apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	810	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	811	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	812
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	813	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	814	apply (rule case_split_thm)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	815	apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	816	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	817	apply (erule ssum_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	818	apply (rule ssum_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	819	apply (erule ssum_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	820	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	821
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	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	824	(* restricted surjectivity of Isinl *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	825	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	826
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	827	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	828	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	829	apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	830	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	831	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	832	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	833
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	834	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	835	(* restricted surjectivity of Isinr *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	836	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	837
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	838	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	839	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	840	apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	841	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	842	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	843	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	844
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	845	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	846	(* technical lemmas *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	847	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	848
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	849	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	850	apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	851	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	852	apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	853	apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	854	apply (erule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	855	apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	856	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	857	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	858	apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	859	apply (erule_tac [2] less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	860	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	861	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	862
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	863	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	864	apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	865	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	866	apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	867	apply (erule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	868	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	869	apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	870	apply (erule_tac [2] less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	871	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	872	apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	873	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	874
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	875	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	876	(* the type 'a ++ 'b is a cpo in three steps *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	877	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	878
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	879	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	880	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	881	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	882	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	883	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	884	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	885	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	886	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	887	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	888	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	889	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	890	apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	891	apply (rule_tac t = "u" in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	892	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	893	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	894	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	895	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	896	apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	897	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	898	apply (rule less_ssum3c [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	899	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	900	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	901	apply (rule_tac p = "Y (i) " in IssumE)
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 simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	904	apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	905	apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	906	apply (rule_tac t = "Isinl (x) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	907	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	908	apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	909	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	910	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	911
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	912
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	913	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	914	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	915	apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	916	apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	917	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	918	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	919	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	920	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	921	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	922	apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	923	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	924	apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	925	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	926	apply (rule less_ssum3d [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	927	apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	928	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	929	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	930	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	931	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	932	apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	933	apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	934	apply (rule_tac t = "Isinr (y) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	935	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	936	apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	937	apply (rule_tac t = "u" in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	938	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	939	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	940	apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	941	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	942	apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	943	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	944
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	945
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	946	lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	947	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	948	[\| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	949	lub (range ?Y1) = Isinl
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	950	(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	951	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	952
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	953	lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	954	(*
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	955	[\| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	956	lub (range ?Y1) = Isinr
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	957	(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	958	*)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	959
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	960	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	961	apply (rule ssum_lemma4 [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	962	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	963	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	964	apply (erule lub_ssum1a)
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 exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	967	apply (erule lub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	968	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	969	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	970
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	971	(* Class instance of ++ for class pcpo *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	972
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	973	instance "++" :: (pcpo,pcpo)pcpo
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	974	apply (intro_classes)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	975	apply (erule cpo_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	976	apply (rule least_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	977	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	978
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	979	consts
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	980	sinl :: "'a -> ('a++'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	981	sinr :: "'b -> ('a++'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	982	sscase :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	983
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	984	defs
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	985
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	986	sinl_def: "sinl == (LAM x. Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	987	sinr_def: "sinr == (LAM x. Isinr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	988	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	989
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	990	translations
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	991	"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	992
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	993	(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	994	lemma inst_ssum_pcpo: "UU = Isinl UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	995	apply (simp add: UU_def UU_ssum_def)
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	declare inst_ssum_pcpo [symmetric, simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	999
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1000	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1001	(* continuity for Isinl and Isinr *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1002	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1003
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1004	lemma contlub_Isinl: "contlub(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1005	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1006	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1007	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1008	apply (rule_tac [2] thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1009	apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1010	apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1011	apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1012	apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1013	apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1014	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	1015	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1016	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1017	apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1018	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1019	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	1020	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1021	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1022	apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1023	apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1024	apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1025	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1026	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1027	apply (erule monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1028	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1029	apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1030	apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1031	apply (rule Iwhen1[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1032	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1033	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1034
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1035	lemma contlub_Isinr: "contlub(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1036	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1037	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1038	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1039	apply (rule_tac [2] thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1040	apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1041	apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1042	apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1043	apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1044	apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1045	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	1046	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1047	apply (rule arg_cong, rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1048	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1049	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	1050	apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1051	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1052	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1053	apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1054	apply (rule arg_cong, rule lub_equal)
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 (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1057	apply (erule monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1058	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1059	apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1060	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1061	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1062	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1063
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1064	lemma cont_Isinl: "cont(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1065	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1066	apply (rule monofun_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1067	apply (rule contlub_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1068	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1069
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1070	lemma cont_Isinr: "cont(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1071	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1072	apply (rule monofun_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1073	apply (rule contlub_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1074	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1075
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1076	declare cont_Isinl [iff] cont_Isinr [iff]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1077
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1078
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1079	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1080	(* continuity for Iwhen in the firts two arguments *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1081	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1082
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1083	lemma contlub_Iwhen1: "contlub(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1084	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1085	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1086	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1087	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1088	apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1089	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1090	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1091	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1092	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1093	apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1094	apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1095	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1096	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1097	apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1098	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1099	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1100	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1101	apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1102	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1103	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1104	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1105
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1106	lemma contlub_Iwhen2: "contlub(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1107	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1108	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1109	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1110	apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1111	apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1112	apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1113	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1114	apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1115	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1116	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1117	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1118	apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1119	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1120	apply (erule contlub_cfun_fun)
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	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1124	(* continuity for Iwhen in its third argument *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1125	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1126
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1127	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1128	(* first 5 ugly lemmas *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1129	(* ------------------------------------------------------------------------ *)
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 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	1132	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1133	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1134	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1135	apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1136	apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1137	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1138	apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1139	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1140	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1141	apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1142	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1143
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1144
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1145	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	1146	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1147	apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1148	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1149	apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1150	apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1151	apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1152	apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1153	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1154	apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1155	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1156	apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1157	apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1158	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1159
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1160	lemma ssum_lemma11: "[\| chain(Y); lub(range(Y)) = Isinl(UU) \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1161	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	1162	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1163	apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1164	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1165	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	1166	apply (rule inst_ssum_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1167	apply (rule chain_UU_I [THEN spec, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1168	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1169	apply (erule inst_ssum_pcpo [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1170	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1171	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1172
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1173	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	1174	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	1175	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1176	apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1177	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1178	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1179	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1180	apply (rule thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1181	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1182	apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1183	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1184	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1185	apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1186	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1187	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1188	apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1189	apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1190	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1191	apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1192	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1193	apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1194	apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1195	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1196	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1197	apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1198	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1199	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1200	apply (rule ssum_lemma9 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1201	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1202	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1203	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1204	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1205	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1206	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1207	apply (rule Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1208	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1209	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1210	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1211	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1212	apply (subst Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1213	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1214	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1215	apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1216	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1217	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1218	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1219
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1220
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1221	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	1222	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	1223	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1224	apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1225	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1226	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1227	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1228	apply (rule thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1229	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1230	apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1231	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1232	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1233	apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1234	apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1235	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1236	apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1237	apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1238	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1239	apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1240	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1241	apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1242	apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1243	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1244	apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1245	apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1246	apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1247	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1248	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1249	apply (rule ssum_lemma10 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1250	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1251	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1252	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1253	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1254	apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1255	apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1256	apply (rule Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1257	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1258	apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1259	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1260	apply (subst Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1261	apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1262	apply (rule_tac t = "Y (i) " in ssubst)
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 simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1265	apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1266	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1267	apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1268	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1269
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1270
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1271	lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1272	apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1273	apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1274	apply (rule_tac p = "lub (range (Y))" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1275	apply (erule ssum_lemma11)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1276	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1277	apply (erule ssum_lemma12)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1278	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1279	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1280	apply (erule ssum_lemma13)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1281	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1282	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1283	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1284
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1285	lemma cont_Iwhen1: "cont(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1286	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1287	apply (rule monofun_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1288	apply (rule contlub_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1289	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1290
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1291	lemma cont_Iwhen2: "cont(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1292	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1293	apply (rule monofun_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1294	apply (rule contlub_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1295	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1296
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1297	lemma cont_Iwhen3: "cont(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1298	apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1299	apply (rule monofun_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1300	apply (rule contlub_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1301	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1302
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	(* continuous versions of lemmas for 'a ++ 'b *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1305	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1306
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1307	lemma strict_sinl [simp]: "sinl$UU =UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1308	apply (unfold sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1309	apply (simp add: cont_Isinl)
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 strict_sinr [simp]: "sinr$UU=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1313	apply (unfold sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1314	apply (simp add: cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1315	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1316
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1317	lemma noteq_sinlsinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1318	"sinl$a=sinr$b ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1319	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1320	apply (auto dest!: noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1321	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1322
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1323	lemma inject_sinl:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1324	"sinl$a1=sinl$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1325	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1326	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1327	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1328
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1329	lemma inject_sinr:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1330	"sinr$a1=sinr$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1331	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1332	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1333	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1334
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1335	declare inject_sinl [dest!] inject_sinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1336
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1337	lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1338	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1339	apply (rule inject_sinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1340	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1341	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1342
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1343	lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1344	apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1345	apply (rule inject_sinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1346	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1347	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1348
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1349	lemma Exh_Ssum1:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1350	"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	1351	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1352	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1353	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1354	apply (rule Exh_Ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1355	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1356
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1357
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1358	lemma ssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1359	assumes major: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1360	assumes prem2: "!!x.[\|p=sinl$x; x~=UU \|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1361	assumes prem3: "!!y.[\|p=sinr$y; y~=UU \|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1362	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1363	apply (rule major [THEN IssumE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1364	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1365	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1366	apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1367	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1368	apply (simp add: sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1369	apply (rule prem3)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1370	prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1371	apply (simp add: sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1372	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1373
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1374
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1375	lemma ssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1376	assumes preml: "!!x.[\|p=sinl$x\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1377	assumes premr: "!!y.[\|p=sinr$y\|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1378	shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1379	apply (rule IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1380	apply (rule preml)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1381	apply (rule_tac [2] premr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1382	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1383	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1384	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1385
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1386	lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1387	cont_Iwhen3 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1388
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1389	lemma sscase1 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1390	"sscase$f$g$UU = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1391	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1392	apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1393	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1394	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1395	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1396	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1397	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1398	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1399	apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1400	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1401
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1402	lemma sscase2 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1403	"x~=UU==> sscase$f$g$(sinl$x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1404	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1405	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1406	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1407	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1408	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1409	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1410	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1411	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1412	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1413	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1414	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1415
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1416	lemma sscase3 [simp]:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1417	"x~=UU==> sscase$f$g$(sinr$x) = g$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1418	apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1419	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1420	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1421	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1422	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1423	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1424	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1425	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1426	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1427	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1428	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1429
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1430	lemma less_ssum4a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1431	"(sinl$x << sinl$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1432	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1433	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1434	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1435	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1436	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1437	apply (rule less_ssum3a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1438	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1439
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1440	lemma less_ssum4b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1441	"(sinr$x << sinr$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1442	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1443	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1444	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1445	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1446	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1447	apply (rule less_ssum3b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1448	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1449
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1450	lemma less_ssum4c:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1451	"(sinl$x << sinr$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1452	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1453	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1454	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1455	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1456	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1457	apply (rule less_ssum3c)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1458	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1459
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1460	lemma less_ssum4d:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1461	"(sinr$x << sinl$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1462	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1463	apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1464	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1465	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1466	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1467	apply (rule less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1468	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1469
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1470	lemma ssum_chainE:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1471	"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	1472	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1473	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1474	apply (erule ssum_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1475	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1476
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1477	lemma thelub_ssum2a:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1478	"[\| chain(Y); !i.? x. Y(i) = sinl$x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1479	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	1480	apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1481	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1482	apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1483	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1484	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1485	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1486	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1487	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1488	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1489	apply (rule thelub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1490	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1491	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1492	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1493	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1494	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1495	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1496	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1497	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1498	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1499
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1500	lemma thelub_ssum2b:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1501	"[\| chain(Y); !i.? x. Y(i) = sinr$x \|] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1502	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	1503	apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1504	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1505	apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1506	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1507	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1508	apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1509	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1510	apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1511	apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1512	apply (rule thelub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1513	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1514	apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1515	apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1516	apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1517	apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1518	apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1519	apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1520	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1521	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1522
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1523	lemma thelub_ssum2a_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1524	"[\| 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	1525	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1526	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1527	apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1528	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1529	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1530
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1531	lemma thelub_ssum2b_rev:
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1532	"[\| 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	1533	apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1534	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1535	apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1536	apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1537	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1538
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1539	lemma thelub_ssum3: "chain(Y) ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1540	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	1541	\| 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	1542	apply (rule ssum_chainE [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1543	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1544	apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1545	apply (erule thelub_ssum2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1546	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1547	apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1548	apply (erule thelub_ssum2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1549	apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1550	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1551
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1552	lemma sscase4: "sscase$sinl$sinr$z=z"
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1553	apply (rule_tac p = "z" in ssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1554	apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1555	done
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1556
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1557
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1558	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1559	(* install simplifier for Ssum *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1560	(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1561
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1562	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	1563	sscase1 sscase2 sscase3
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1564
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: diff changeset	1565	end

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