isabelle: src/HOLCF/Lift3.ML@1358dc040edb (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	(* Title: HOLCF/lift3.ML
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	Author: Franz Regensburger
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 lift3.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	open Lift3;
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	(* -------------------------------------------------------------------------*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	(* some lemmas restated for class pcpo *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	15	qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19	(rtac less_lift2b 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	22	qed_goal "defined_Iup2" Lift3.thy "Iup(x) ~= UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	23	(fn prems =>
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	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26	(rtac defined_Iup 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30	(* continuity for Iup *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	33	qed_goal "contlub_Iup" Lift3.thy "contlub(Iup)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36	(rtac contlubI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38	(rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	(rtac (thelub_lift1a RS sym) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40	(fast_tac HOL_cs 3),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	(etac (monofun_Iup RS ch2ch_monofun) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42	(res_inst_tac [("f","Iup")] arg_cong 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43	(rtac lub_equal 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	44	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	45	(rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	46	(etac (monofun_Iup RS ch2ch_monofun) 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	47	(asm_simp_tac Lift0_ss 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	48	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	49
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	50	qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	51	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	52	[
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	53	(rtac monocontlub2cont 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	54	(rtac monofun_Iup 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	55	(rtac contlub_Iup 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	56	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	57
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	(* continuity for Ilift *)
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
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	63	qed_goal "contlub_Ilift1" Lift3.thy "contlub(Ilift)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	64	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	65	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	66	(rtac contlubI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	67	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	68	(rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	69	(rtac (thelub_fun RS sym) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	70	(etac (monofun_Ilift1 RS ch2ch_monofun) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	71	(rtac ext 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	72	(res_inst_tac [("p","x")] liftE 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	73	(asm_simp_tac Lift0_ss 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	74	(rtac (lub_const RS thelubI RS sym) 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	75	(asm_simp_tac Lift0_ss 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	76	(etac contlub_cfun_fun 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	77	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	78
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	79
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	80	qed_goal "contlub_Ilift2" Lift3.thy "contlub(Ilift(f))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	81	(fn prems =>
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	(rtac contlubI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	84	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	85	(rtac disjE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	86	(rtac (thelub_lift1a RS ssubst) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	87	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	88	(atac 2),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	89	(asm_simp_tac Lift0_ss 2),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	90	(rtac (thelub_lift1b RS ssubst) 3),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	91	(atac 3),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	92	(atac 3),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	93	(fast_tac HOL_cs 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	94	(asm_simp_tac Lift0_ss 2),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	95	(rtac (chain_UU_I_inverse RS sym) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	96	(rtac allI 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	97	(res_inst_tac [("p","Y(i)")] liftE 2),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	98	(asm_simp_tac Lift0_ss 2),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	99	(rtac notE 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	100	(dtac spec 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	101	(etac spec 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	102	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	103	(rtac (contlub_cfun_arg RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	104	(etac (monofun_Ilift2 RS ch2ch_monofun) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	105	(rtac lub_equal2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	106	(rtac (monofun_fapp2 RS ch2ch_monofun) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	107	(etac (monofun_Ilift2 RS ch2ch_monofun) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	108	(etac (monofun_Ilift2 RS ch2ch_monofun) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	109	(rtac (chain_mono2 RS exE) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	110	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	111	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	112	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	113	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	114	(res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	115	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	116	(rtac defined_Iup2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	117	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	118	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	119	(res_inst_tac [("p","Y(i)")] liftE 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	120	(asm_simp_tac Lift0_ss 2),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	121	(res_inst_tac [("P","Y(i) = UU")] notE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	122	(fast_tac HOL_cs 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	123	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	124	(atac 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	125	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	126
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	127	qed_goal "cont_Ilift1" Lift3.thy "cont(Ilift)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	128	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	129	[
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	130	(rtac monocontlub2cont 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	131	(rtac monofun_Ilift1 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	132	(rtac contlub_Ilift1 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	133	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	134
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	135	qed_goal "cont_Ilift2" Lift3.thy "cont(Ilift(f))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	136	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	137	[
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	138	(rtac monocontlub2cont 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	139	(rtac monofun_Ilift2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	140	(rtac contlub_Ilift2 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	141	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	142
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	143
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	144	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	145	(* continuous versions of lemmas for ('a)u *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	146	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	147
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	148	qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU \| (? x. z = up`x)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	149	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	150	[
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	151	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	152	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	153	(rtac Exh_Lift 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	154	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	155
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	156	qed_goalw "inject_up" Lift3.thy [up_def] "up`x=up`y ==> x=y"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	157	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	158	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	159	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	160	(rtac inject_Iup 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	161	(etac box_equals 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	162	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	163	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	164	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	165
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	166	qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	167	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	168	[
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	169	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	170	(rtac defined_Iup2 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	171	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	172
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	173	qed_goalw "liftE1" Lift3.thy [up_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	174	"[\| p=UU ==> Q; !!x. p=up`x==>Q\|] ==>Q"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	175	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	176	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	177	(rtac liftE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	178	(resolve_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	179	(etac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	180	(resolve_tac (tl prems) 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	181	(asm_simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	182	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	183
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	184
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	185	qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	186	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	187	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	188	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	189	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	190	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	191	cont_Ilift2,cont2cont_CF1L]) 1)),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	192	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	193	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	194	cont_Ilift2,cont2cont_CF1L]) 1)),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	195	(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	196	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	197
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	198	qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	199	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	200	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	201	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	202	(rtac cont_Iup 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	203	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	204	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	205	cont_Ilift2,cont2cont_CF1L]) 1)),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	206	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	207	(rtac cont_Ilift2 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	208	(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
243 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
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	211	qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	212	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	213	[
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	214	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	215	(rtac less_lift3b 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	216	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	217
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	218	qed_goalw "less_lift4c" Lift3.thy [up_def,lift_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	219	"(up`x << up`y) = (x<<y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	220	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	221	[
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	222	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	223	(rtac less_lift2c 1)
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
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	226	qed_goalw "thelub_lift2a" Lift3.thy [up_def,lift_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	227	"[\| is_chain(Y); ? i x. Y(i) = up`x \|] ==>\
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	228	\ lub(range(Y)) = up`(lub(range(%i. lift`(LAM x. x)`(Y i))))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	229	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	230	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	231	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	232	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	233	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	234	cont_Ilift2,cont2cont_CF1L]) 1)),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	235	(rtac (beta_cfun RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	236	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	237	cont_Ilift2,cont2cont_CF1L]) 1)),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	238
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	239	(rtac (beta_cfun RS ext RS ssubst) 1),
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	240	(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	241	cont_Ilift2,cont2cont_CF1L]) 1)),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	242	(rtac thelub_lift1a 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	243	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	244	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	245	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	246	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	247	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	248	(etac box_equals 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	249	(rtac refl 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	250	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
243 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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	254
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	255	qed_goalw "thelub_lift2b" Lift3.thy [up_def,lift_def]
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	256	"[\| is_chain(Y); ! i x. Y(i) ~= up`x \|] ==> lub(range(Y)) = UU"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	257	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	258	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	259	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	260	(rtac (inst_lift_pcpo RS ssubst) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	261	(rtac thelub_lift1b 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	262	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	263	(strip_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	264	(dtac spec 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	265	(dtac spec 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	266	(rtac swap 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	267	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	268	(dtac notnotD 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	269	(etac box_equals 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	270	(rtac refl 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	271	(simp_tac (Lift0_ss addsimps [cont_Iup]) 1)
243 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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	274
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	275	qed_goal "lift_lemma2" Lift3.thy " (? x.z = up`x) = (z~=UU)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	276	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	277	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	278	(rtac iffI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	279	(etac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	280	(hyp_subst_tac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	281	(rtac defined_up 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	282	(res_inst_tac [("p","z")] liftE1 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	283	(etac notE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	284	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	285	(etac exI 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	286	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	287
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	288
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	289	qed_goal "thelub_lift2a_rev" Lift3.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	290	"[\| is_chain(Y); lub(range(Y)) = up`x \|] ==> ? i x. Y(i) = up`x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	291	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	292	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	293	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	294	(rtac exE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	295	(rtac chain_UU_I_inverse2 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	296	(rtac (lift_lemma2 RS iffD1) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	297	(etac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	298	(rtac exI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	299	(rtac (lift_lemma2 RS iffD2) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	300	(atac 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	301	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	302
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	303	qed_goal "thelub_lift2b_rev" Lift3.thy
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	304	"[\| is_chain(Y); lub(range(Y)) = UU \|] ==> ! i x. Y(i) ~= up`x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	305	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	306	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	307	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	308	(rtac allI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	309	(rtac (notex2all RS iffD1) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	310	(rtac contrapos 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	311	(etac (lift_lemma2 RS iffD1) 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	312	(rtac notnotI 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	313	(rtac (chain_UU_I RS spec) 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	314	(atac 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	315	(atac 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	316	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	317
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	318
892 d0dc8d057929 added qed, qed_goal[w] clasohm parents: 243 diff changeset	319	qed_goal "thelub_lift3" Lift3.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	320	"is_chain(Y) ==> lub(range(Y)) = UU \|\
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	321	\ lub(range(Y)) = up`(lub(range(%i. lift`(LAM x.x)`(Y i))))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	322	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	323	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	324	(cut_facts_tac prems 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	325	(rtac disjE 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	326	(rtac disjI1 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	327	(rtac thelub_lift2b 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	328	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	329	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	330	(rtac disjI2 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	331	(rtac thelub_lift2a 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	332	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	333	(atac 2),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	334	(fast_tac HOL_cs 1)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	335	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	336
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	337	qed_goal "lift3" Lift3.thy "lift`up`x=x"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	338	(fn prems =>
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	339	[
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	340	(res_inst_tac [("p","x")] liftE1 1),
1277 caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	341	(asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1),
caef3601c0b2 corrected some errors that occurred after introduction of local simpsets regensbu parents: 1274 diff changeset	342	(asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	343	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	344
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	345	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	346	(* install simplifier for ('a)u *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	347	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	348
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	349	val lift_rews = [lift1,lift2,defined_up];
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	350

author	clasohm
	Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294	1358dc040edb
parent 1277	caef3601c0b2
child 1461	6bcb44e4d6e5
permissions	-rw-r--r--