isabelle: src/HOLCF/Ssum1.ML@d6017ce6b93e (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	1	(* Title: HOLCF/Ssum1.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	6	Lemmas for theory Ssum1.thy
243 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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	open Ssum1;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	local
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	fun eq_left s1 s2 =
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	14	(
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	15	(res_inst_tac [("s",s1),("t",s2)] (inject_Isinl RS subst) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	16	THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	17	THEN (atac 2)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	18	THEN (etac sym 1));
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20	fun eq_right s1 s2 =
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	21	(
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	22	(res_inst_tac [("s",s1),("t",s2)] (inject_Isinr RS subst) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	23	THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	24	THEN (atac 2)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	25	THEN (etac sym 1));
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27	fun UU_left s1 =
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	28	(
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	29	(res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct1 RS ssubst)1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	30	THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	31	THEN (atac 2)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	32	THEN (etac sym 1));
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	fun UU_right s1 =
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	35	(
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	36	(res_inst_tac [("t",s1)](noteq_IsinlIsinr RS conjunct2 RS ssubst)1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	37	THEN (rtac trans 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	38	THEN (atac 2)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	39	THEN (etac sym 1))
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	in
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	43	val less_ssum1a = prove_goalw thy [less_ssum_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	44	"[\|s1=Isinl(x::'a); s2=Isinl(y::'a)\|] ==> s1 << s2 = (x << y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	46	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	47	(cut_facts_tac prems 1),
4535 f24cebc299e4 added select_equality to the implicit claset oheimb parents: 3323 diff changeset	48	(rtac select_equality 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	49	(dtac conjunct1 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	50	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	51	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	52	(etac mp 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	53	(fast_tac HOL_cs 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	54	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	55	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	56	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	57	(eq_left "x" "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	58	(eq_left "y" "xa"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	59	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	60	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	61	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	62	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	63	(UU_left "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	64	(UU_right "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	65	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	66	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	67	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	68	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	69	(eq_left "x" "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	70	(UU_left "y"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	71	(rtac iffI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	72	(etac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	73	(res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	74	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	75	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	76	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	77	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	78	(UU_left "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	79	(UU_right "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	80	(Simp_tac 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	81	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	82
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	83
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	84	val less_ssum1b = prove_goalw thy [less_ssum_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	85	"[\|s1=Isinr(x::'b); s2=Isinr(y::'b)\|] ==> s1 << s2 = (x << y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	86	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	87	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	88	(cut_facts_tac prems 1),
4535 f24cebc299e4 added select_equality to the implicit claset oheimb parents: 3323 diff changeset	89	(rtac select_equality 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	90	(dtac conjunct2 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	91	(dtac conjunct1 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	92	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	93	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	94	(etac mp 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	95	(fast_tac HOL_cs 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	96	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	97	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	98	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	99	(UU_right "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	100	(UU_left "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	101	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	102	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	103	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	104	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	105	(eq_right "x" "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	106	(eq_right "y" "ya"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	107	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	108	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	109	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	110	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	111	(UU_right "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	112	(UU_left "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	113	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	114	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	115	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	116	(eq_right "x" "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	117	(UU_right "y"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	118	(rtac iffI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	119	(etac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	120	(res_inst_tac [("s","UU::'b"),("t","x")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	121	(etac sym 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	122	(rtac refl_less 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	123	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	124
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	125
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	126	val less_ssum1c = prove_goalw thy [less_ssum_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	127	"[\|s1=Isinl(x::'a); s2=Isinr(y::'b)\|] ==> s1 << s2 = ((x::'a) = UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	128	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	129	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	130	(cut_facts_tac prems 1),
4535 f24cebc299e4 added select_equality to the implicit claset oheimb parents: 3323 diff changeset	131	(rtac select_equality 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	132	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	133	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	134	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	135	(eq_left "x" "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	136	(UU_left "xa"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	137	(rtac iffI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	138	(res_inst_tac [("s","x"),("t","UU::'a")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	139	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	140	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	141	(etac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	142	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	143	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	144	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	145	(UU_left "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	146	(UU_right "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	147	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	148	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	149	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	150	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	151	(eq_left "x" "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	152	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	153	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	154	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	155	(UU_left "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	156	(UU_right "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	157	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	158	(dtac conjunct2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	159	(dtac conjunct2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	160	(dtac conjunct1 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	161	(dtac spec 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	162	(dtac spec 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	163	(etac mp 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	164	(fast_tac HOL_cs 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	165	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	166
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	167
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	168	val less_ssum1d = prove_goalw thy [less_ssum_def]
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	169	"[\|s1=Isinr(x); s2=Isinl(y)\|] ==> s1 << s2 = (x = UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	170	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	171	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	172	(cut_facts_tac prems 1),
4535 f24cebc299e4 added select_equality to the implicit claset oheimb parents: 3323 diff changeset	173	(rtac select_equality 1),
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	174	(dtac conjunct2 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	175	(dtac conjunct2 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	176	(dtac conjunct2 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	177	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	178	(dtac spec 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	179	(etac mp 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	180	(fast_tac HOL_cs 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	181	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	182	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	183	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	184	(UU_right "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	185	(UU_left "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	186	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	187	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	188	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	189	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	190	(UU_right "ya"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	191	(eq_right "x" "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	192	(rtac iffI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	193	(etac UU_I 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	194	(res_inst_tac [("s","UU"),("t","x")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	195	(etac sym 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	196	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	197	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	198	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	199	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	200	(UU_right "x"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	201	(UU_left "u"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	202	(Simp_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	203	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	204	(etac conjE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	205	(eq_right "x" "v"),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	206	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	207	])
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	208	end;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	209
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	210
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	211	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	212	(* optimize lemmas about less_ssum *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	213	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	214
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	215	qed_goal "less_ssum2a" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	216	"(Isinl x) << (Isinl y) = (x << y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	217	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	218	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	219	(rtac less_ssum1a 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	220	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	221	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	222	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	223
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	224	qed_goal "less_ssum2b" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	225	"(Isinr x) << (Isinr y) = (x << y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	226	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	227	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	228	(rtac less_ssum1b 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	229	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	230	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	231	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	232
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	233	qed_goal "less_ssum2c" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	234	"(Isinl x) << (Isinr y) = (x = UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	235	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	236	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	237	(rtac less_ssum1c 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	238	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	239	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	240	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	241
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	242	qed_goal "less_ssum2d" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	243	"(Isinr x) << (Isinl y) = (x = UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	244	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	245	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	246	(rtac less_ssum1d 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	247	(rtac refl 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	248	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	249	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	250
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	251
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	252	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	253	(* less_ssum is a partial order on ++ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	254	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	255
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	256	qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	257	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	258	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	259	(res_inst_tac [("p","p")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	260	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	261	(rtac (less_ssum2a RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	262	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	263	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	264	(rtac (less_ssum2b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	265	(rtac refl_less 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	266	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	267
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	268	qed_goal "antisym_less_ssum" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	269	"[\|(p1::'a++'b) << p2; p2 << p1\|] ==> p1=p2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	270	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	271	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	272	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	273	(res_inst_tac [("p","p1")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	274	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	275	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	276	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	277	(res_inst_tac [("f","Isinl")] arg_cong 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	278	(rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	279	(etac (less_ssum2a RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	280	(etac (less_ssum2a RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	281	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	282	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	283	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	284	(rtac strict_IsinlIsinr 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	285	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	286	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	287	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	288	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	289	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	290	(rtac (strict_IsinlIsinr RS sym) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	291	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	292	(res_inst_tac [("f","Isinr")] arg_cong 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	293	(rtac antisym_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	294	(etac (less_ssum2b RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	295	(etac (less_ssum2b RS iffD1) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	296	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	297
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	298	qed_goal "trans_less_ssum" thy
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2640 diff changeset	299	"[\|(p1::'a++'b) << p2; p2 << p3\|] ==> p1 << p3"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	300	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	301	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	302	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	303	(res_inst_tac [("p","p1")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	304	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	305	(res_inst_tac [("p","p3")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	306	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	307	(rtac (less_ssum2a RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	308	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	309	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	310	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	311	(etac (less_ssum2a RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	312	(etac (less_ssum2a RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	313	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	314	(etac (less_ssum2c RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	315	(rtac minimal 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	316	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	317	(rtac (less_ssum2c RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	318	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	319	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	320	(rtac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	321	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	322	(etac (less_ssum2a RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	323	(rtac (antisym_less_inverse RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	324	(etac (less_ssum2c RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	325	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	326	(etac (less_ssum2c RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	327	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	328	(res_inst_tac [("p","p3")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	329	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	330	(rtac (less_ssum2d RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	331	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	332	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	333	(etac (less_ssum2d RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	334	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	335	(rtac UU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	336	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	337	(etac (less_ssum2b RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	338	(rtac (antisym_less_inverse RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	339	(etac (less_ssum2d RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	340	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	341	(rtac (less_ssum2b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	342	(res_inst_tac [("p","p2")] IssumE2 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	343	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	344	(etac (less_ssum2d RS iffD1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	345	(rtac minimal 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	346	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	347	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	348	(etac (less_ssum2b RS iffD1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	349	(etac (less_ssum2b RS iffD1) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1267 diff changeset	350	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	351
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	352
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	353

author	wenzelm
	Tue, 24 Nov 1998 12:03:09 +0100
changeset 5953	d6017ce6b93e
parent 4535	f24cebc299e4
child 9169	85a47aa21f74
permissions	-rw-r--r--