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

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

author	huffman
	Fri, 04 Mar 2005 23:23:47 +0100
changeset 15577	e16da3068ad6
parent 15576	efb95d0d01f7
child 15593	24d770bbc44a
permissions	-rw-r--r--