isabelle: src/HOLCF/Ssum1.thy@41bfe19eabe2 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1479 diff changeset	1	(* Title: HOLCF/Ssum1.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1168 diff changeset	3	Author: Franz Regensburger
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Partial ordering for the strict sum ++
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	9	theory Ssum1 = Ssum0:
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	11	instance "++"::(pcpo,pcpo)sq_ord ..
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	12
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	13	defs (overloaded)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	14	less_ssum_def: "(op <<) == (%s1 s2.@z.
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	15	(! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	16	&(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	17	&(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	18	&(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19
15568 41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	20	(* Title: HOLCF/Ssum1.ML
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	21	ID: $Id$
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	22	Author: Franz Regensburger
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	23	License: GPL (GNU GENERAL PUBLIC LICENSE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	24
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	25	Partial ordering for the strict sum ++
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	26	*)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	27
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	28	lemma less_ssum1a:
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	29	"[\|s1=Isinl(x::'a); s2=Isinl(y::'a)\|] ==> s1 << s2 = (x << y)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	30	apply (unfold less_ssum_def)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	31	apply (rule some_equality)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	32	apply (drule_tac [2] conjunct1)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	33	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	34	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	35	apply (erule_tac [2] mp)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	36	prefer 2 apply fast
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	37	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	38	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	39	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	40	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	41	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	42	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	43	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	44	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	45	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	46	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	47	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	48	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	49	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	50	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	51	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	52	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	53	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	54	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	55	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	56	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	57	apply (rule eq_UU_iff[symmetric])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	58	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	59	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	60	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	61	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	62	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	63	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	64
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	65
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	66	lemma less_ssum1b:
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	67	"[\|s1=Isinr(x::'b); s2=Isinr(y::'b)\|] ==> s1 << s2 = (x << y)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	68
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	69	apply (unfold less_ssum_def)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	70	apply (rule some_equality)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	71	apply (drule_tac [2] conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	72	apply (drule_tac [2] conjunct1)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	73	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	74	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	75	apply (erule_tac [2] mp)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	76	prefer 2 apply fast
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	77	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	78	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	79	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	80	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	81	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	82	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	83	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	84	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	85	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	86	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	87	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	88	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	89	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	90	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	91	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	92	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	93	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	94	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	95	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	96	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	97	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	98	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	99	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	100	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	101	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	102	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	103	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	104	apply (rule eq_UU_iff[symmetric])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	105	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	106
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	107
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	108	lemma less_ssum1c:
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	109	"[\|s1=Isinl(x::'a); s2=Isinr(y::'b)\|] ==> s1 << s2 = ((x::'a) = UU)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	110
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	111	apply (unfold less_ssum_def)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	112	apply (rule some_equality)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	113	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	114	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	115	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	116	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	117	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	118	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	119	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	120	apply (rule eq_UU_iff)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	121	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	122	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	123	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	124	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	125	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	126	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	127	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	128	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	129	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	130	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	131	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	132	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	133	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	134	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	135	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	136	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	137	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	138	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	139	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	140	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	141	apply (drule conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	142	apply (drule conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	143	apply (drule conjunct1)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	144	apply (drule spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	145	apply (drule spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	146	apply (erule mp)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	147	apply fast
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	148	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	149
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	150
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	151	lemma less_ssum1d:
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	152	"[\|s1=Isinr(x); s2=Isinl(y)\|] ==> s1 << s2 = (x = UU)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	153
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	154	apply (unfold less_ssum_def)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	155	apply (rule some_equality)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	156	apply (drule_tac [2] conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	157	apply (drule_tac [2] conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	158	apply (drule_tac [2] conjunct2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	159	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	160	apply (drule_tac [2] spec)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	161	apply (erule_tac [2] mp)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	162	prefer 2 apply fast
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	163	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	164	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	165	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	166	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	167	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	168	apply (drule inject_Isinl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	169	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	170	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	171	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	172	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	173	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	174	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	175	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	176	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	177	apply (rule eq_UU_iff)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	178	apply (rule conjI)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	179	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	180	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	181	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	182	apply (drule noteq_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	183	apply (drule noteq_IsinlIsinr[OF sym])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	184	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	185	apply (intro strip)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	186	apply (erule conjE)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	187	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	188	apply (drule inject_Isinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	189	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	190	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	191
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	192
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	193	(* ------------------------------------------------------------------------ *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	194	(* optimize lemmas about less_ssum *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	195	(* ------------------------------------------------------------------------ *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	196
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	197	lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	198	apply (rule less_ssum1a)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	199	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	200	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	201	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	202
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	203	lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	204	apply (rule less_ssum1b)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	205	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	206	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	207	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	208
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	209	lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	210	apply (rule less_ssum1c)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	211	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	212	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	213	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	214
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	215	lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	216	apply (rule less_ssum1d)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	217	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	218	apply (rule refl)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	219	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	220
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	221
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	222	(* ------------------------------------------------------------------------ *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	223	(* less_ssum is a partial order on ++ *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	224	(* ------------------------------------------------------------------------ *)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	225
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	226	lemma refl_less_ssum: "(p::'a++'b) << p"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	227	apply (rule_tac p = "p" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	228	apply (erule ssubst)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	229	apply (rule less_ssum2a [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	230	apply (rule refl_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	231	apply (erule ssubst)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	232	apply (rule less_ssum2b [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	233	apply (rule refl_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	234	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	235
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	236	lemma antisym_less_ssum: "[\|(p1::'a++'b) << p2; p2 << p1\|] ==> p1=p2"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	237	apply (rule_tac p = "p1" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	238	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	239	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	240	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	241	apply (rule_tac f = "Isinl" in arg_cong)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	242	apply (rule antisym_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	243	apply (erule less_ssum2a [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	244	apply (erule less_ssum2a [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	245	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	246	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	247	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	248	apply (rule strict_IsinlIsinr)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	249	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	250	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	251	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	252	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	253	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	254	apply (rule strict_IsinlIsinr [symmetric])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	255	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	256	apply (rule_tac f = "Isinr" in arg_cong)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	257	apply (rule antisym_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	258	apply (erule less_ssum2b [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	259	apply (erule less_ssum2b [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	260	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	261
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	262	lemma trans_less_ssum: "[\|(p1::'a++'b) << p2; p2 << p3\|] ==> p1 << p3"
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	263	apply (rule_tac p = "p1" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	264	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	265	apply (rule_tac p = "p3" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	266	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	267	apply (rule less_ssum2a [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	268	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	269	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	270	apply (rule trans_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	271	apply (erule less_ssum2a [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	272	apply (erule less_ssum2a [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	273	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	274	apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	275	apply (rule minimal)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	276	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	277	apply (rule less_ssum2c [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	278	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	279	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	280	apply (rule UU_I)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	281	apply (rule trans_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	282	apply (erule less_ssum2a [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	283	apply (rule antisym_less_inverse [THEN conjunct1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	284	apply (erule less_ssum2c [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	285	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	286	apply (erule less_ssum2c [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	287	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	288	apply (rule_tac p = "p3" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	289	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	290	apply (rule less_ssum2d [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	291	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	292	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	293	apply (erule less_ssum2d [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	294	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	295	apply (rule UU_I)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	296	apply (rule trans_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	297	apply (erule less_ssum2b [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	298	apply (rule antisym_less_inverse [THEN conjunct1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	299	apply (erule less_ssum2d [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	300	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	301	apply (rule less_ssum2b [THEN iffD2])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	302	apply (rule_tac p = "p2" in IssumE2)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	303	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	304	apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	305	apply (rule minimal)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	306	apply simp
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	307	apply (rule trans_less)
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	308	apply (erule less_ssum2b [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	309	apply (erule less_ssum2b [THEN iffD1])
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	310	done
41bfe19eabe2 converted to new-style theory huffman parents: 14981 diff changeset	311
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	312	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	313
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	314

author	huffman
	Thu, 03 Mar 2005 01:37:32 +0100
changeset 15568	41bfe19eabe2
parent 14981	e73f8140af78
permissions	-rw-r--r--