isabelle: src/HOLCF/Sprod2.ML@0ef6ea27ab15 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	1	(* Title: HOLCF/sprod2.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: 1168 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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Lemmas for sprod2.thy
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10	open Sprod2;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11
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	(* access to less_sprod in class po *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	16	qed_goal "less_sprod3a" Sprod2.thy
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	17	"p1=Ispair UU UU ==> p1 << p2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	19	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	20	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	21	(rtac (inst_sprod_po RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	22	(etac less_sprod1a 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	23	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	24
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	26	qed_goal "less_sprod3b" Sprod2.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	27	"p1~=Ispair UU UU ==>\
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	28	\ (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	30	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	31	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	32	(rtac (inst_sprod_po RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	33	(etac less_sprod1b 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	34	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	36	qed_goal "less_sprod4b" Sprod2.thy
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	37	"p << Ispair UU UU ==> p = Ispair UU UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	39	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	40	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	41	(rtac less_sprod2b 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	42	(etac (inst_sprod_po RS subst) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	43	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	44
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45	val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	46	(* Ispair ?a ?b << Ispair UU UU ==> ?a = UU \| ?b = UU *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	48	qed_goal "less_sprod4c" Sprod2.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	49	"[\|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU\|] ==>\
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	50	\ xa<<x & ya << y"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	51	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	52	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	53	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	54	(rtac less_sprod2c 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	55	(etac (inst_sprod_po RS subst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	56	(REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	57	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	58
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	59	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	60	(* type sprod is pointed *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	61	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	62
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	63	qed_goal "minimal_sprod" Sprod2.thy "Ispair UU UU << p"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	64	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	65	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	66	(rtac less_sprod3a 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	67	(rtac refl 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	68	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	69
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	70	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	71	(* Ispair is monotone in both arguments *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	72	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	73
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	74	qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	75	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	76	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	77	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	78	(rtac (less_fun RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	79	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	80	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	81	" Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	82	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	83	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	84	(rtac (less_sprod3b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	85	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	86	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	87	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	88	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	89	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	90	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	91	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	92	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	93	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	94	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	95	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	96	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	97	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	98	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	99	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	100	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	101	(etac less_sprod3a 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	102	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	103	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	104	(etac less_sprod3a 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	105	(res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	106	(atac 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	107	(rtac defined_Ispair 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	108	(etac notUU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	109	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	110	(etac (strict_Ispair_rev RS conjunct2) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	111	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	112
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	113
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	114	qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	115	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	116	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	117	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	118	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	119	" Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	120	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	121	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	122	(rtac (less_sprod3b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	123	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	124	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	125	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	126	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	127	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	128	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	129	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	130	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	131	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	132	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	133	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	134	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	135	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	136	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	137	(etac (strict_Ispair_rev RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	138	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	139	(etac less_sprod3a 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	140	(res_inst_tac [("Q",
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	141	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	142	(etac less_sprod3a 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	143	(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	144	(atac 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	145	(rtac defined_Ispair 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	146	(etac (strict_Ispair_rev RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	147	(etac notUU_I 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	148	(etac (strict_Ispair_rev RS conjunct2) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	149	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	150
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	151	qed_goal " monofun_Ispair" Sprod2.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	152	"[\|x1<<x2; y1<<y2\|] ==> Ispair x1 y1 << Ispair x2 y2"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	153	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	154	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	155	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	156	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	157	(rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	158	(less_fun RS iffD1 RS spec)) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	159	(rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	160	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	161	(atac 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	162	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	163
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	164
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	165	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	166	(* Isfst and Issnd are monotone *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	167	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	168
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	169	qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
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: 1168 diff changeset	171	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	172	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	173	(res_inst_tac [("p","x")] IsprodE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	174	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	175	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	176	(rtac minimal 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	177	(rtac (strict_Isfst1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	178	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	179	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	180	(res_inst_tac [("p","y")] IsprodE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	181	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	182	(res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	183	(rtac refl_less 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	184	(etac (less_sprod4b RS sym RS arg_cong) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	185	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	186	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	187	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	188	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	189	(rtac (Isfst RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	190	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	191	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	192	(etac (less_sprod4c RS conjunct1) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	193	(REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	194	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	195
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	196	qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	197	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	198	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	199	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	200	(res_inst_tac [("p","x")] IsprodE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	201	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	202	(rtac trans_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	203	(rtac minimal 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	204	(rtac (strict_Issnd1 RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	205	(rtac refl_less 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	206	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	207	(res_inst_tac [("p","y")] IsprodE 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	208	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	209	(res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	210	(rtac refl_less 2),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	211	(etac (less_sprod4b RS sym RS arg_cong) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	212	(hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	213	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	214	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	215	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	216	(rtac (Issnd RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	217	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	218	(atac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	219	(etac (less_sprod4c RS conjunct2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	220	(REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	221	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	222
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	223
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	224	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	225	(* the type 'a ** 'b is a cpo *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	226	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	227
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	228	qed_goal "lub_sprod" Sprod2.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	229	"[\|is_chain(S)\|] ==> range(S) <<\| \
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	230	\ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	231	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	232	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	233	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	234	(rtac is_lubI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	235	(rtac conjI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	236	(rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	237	(rtac allI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	238	(res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	239	(rtac monofun_Ispair 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	240	(rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	241	(etac (monofun_Isfst RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	242	(rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	243	(etac (monofun_Issnd RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	244	(strip_tac 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	245	(res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	246	(rtac monofun_Ispair 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	247	(rtac is_lub_thelub 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	248	(etac (monofun_Isfst RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	249	(etac (monofun_Isfst RS ub2ub_monofun) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	250	(rtac is_lub_thelub 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	251	(etac (monofun_Issnd RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	252	(etac (monofun_Issnd RS ub2ub_monofun) 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	253	]);
243 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	val thelub_sprod = (lub_sprod RS thelubI);
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	256
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	257
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	258	qed_goal "cpo_sprod" Sprod2.thy
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	259	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<\| x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	260	(fn prems =>
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	261	[
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	262	(cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	263	(rtac exI 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	264	(etac lub_sprod 1)
6bcb44e4d6e5 expanded tabs clasohm parents: 1168 diff changeset	265	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	266
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	267
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	268
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	269
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	270
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	271
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	272
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	273

author	paulson
	Thu, 21 Mar 1996 13:02:26 +0100
changeset 1601	0ef6ea27ab15
parent 1461	6bcb44e4d6e5
child 1779	1155c06fa956
permissions	-rw-r--r--