isabelle: src/HOLCF/HOLCF.thy@1d3df64b1f88 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.thy
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	2	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	4	HOLCF -- a semantic extension of HOL by the LCF logic.
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	7	theory HOLCF
29130 685c9e05a6ab new theory Dsum: cpo of disjoint sum huffman parents: 28892 diff changeset	8	imports
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	9	Main
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	10	Domain
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	11	Powerdomains
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	12	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	13
40329 73f2b99b549d change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)' huffman parents: 40326 diff changeset	14	default_sort bifinite
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	15
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 36452 diff changeset	16	ML {* path_add "~~/src/HOLCF/Library" *}
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 36452 diff changeset	17
40002 c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	18	text {* Legacy theorem names deprecated after Isabelle2009-2: *}
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	19
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	20	lemmas expand_fun_below = fun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	21	lemmas below_fun_ext = fun_belowI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	22	lemmas expand_cfun_eq = cfun_eq_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	23	lemmas ext_cfun = cfun_eqI
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	24	lemmas expand_cfun_below = cfun_below_iff
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	25	lemmas below_cfun_ext = cfun_belowI
40011 b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	26	lemmas monofun_fun_fun = fun_belowD
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	27	lemmas monofun_fun_arg = monofunE
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	28	lemmas monofun_lub_fun = adm_monofun [THEN admD]
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	29	lemmas cont_lub_fun = adm_cont [THEN admD]
40326 73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	30	lemmas cont2cont_Rep_CFun = cont2cont_APP
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	31	lemmas cont_Rep_CFun_app = cont_APP_app
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	32	lemmas cont_Rep_CFun_app_app = cont_APP_app_app
40002 c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	33
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI huffman parents: 39974 diff changeset	34	text {* Older legacy theorem names: *}
31076 99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	35
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	36	lemmas sq_ord_less_eq_trans = below_eq_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	37	lemmas sq_ord_eq_less_trans = eq_below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	38	lemmas refl_less = below_refl
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	39	lemmas trans_less = below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	40	lemmas antisym_less = below_antisym
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	41	lemmas antisym_less_inverse = below_antisym_inverse
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	42	lemmas box_less = box_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	43	lemmas rev_trans_less = rev_below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	44	lemmas not_less2not_eq = not_below2not_eq
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	45	lemmas less_UU_iff = below_UU_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	46	lemmas flat_less_iff = flat_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	47	lemmas adm_less = adm_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	48	lemmas adm_not_less = adm_not_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	49	lemmas adm_compact_not_less = adm_compact_not_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	50	lemmas less_fun_def = below_fun_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	51	lemmas expand_fun_less = expand_fun_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	52	lemmas less_fun_ext = below_fun_ext
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	53	lemmas less_discr_def = below_discr_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	54	lemmas discr_less_eq = discr_below_eq
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	55	lemmas less_unit_def = below_unit_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	56	lemmas less_cprod_def = below_prod_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	57	lemmas prod_lessI = prod_belowI
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	58	lemmas Pair_less_iff = Pair_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	59	lemmas fst_less_iff = fst_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	60	lemmas snd_less_iff = snd_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	61	lemmas expand_cfun_less = expand_cfun_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	62	lemmas less_cfun_ext = below_cfun_ext
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	63	lemmas injection_less = injection_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	64	lemmas less_up_def = below_up_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	65	lemmas not_Iup_less = not_Iup_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	66	lemmas Iup_less = Iup_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	67	lemmas up_less = up_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	68	lemmas Def_inject_less_eq = Def_below_Def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	69	lemmas Def_less_is_eq = Def_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	70	lemmas spair_less_iff = spair_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	71	lemmas less_sprod = below_sprod
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	72	lemmas spair_less = spair_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	73	lemmas sfst_less_iff = sfst_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	74	lemmas ssnd_less_iff = ssnd_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	75	lemmas fix_least_less = fix_least_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	76	lemmas dist_less_one = dist_below_one
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	77	lemmas less_ONE = below_ONE
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	78	lemmas ONE_less_iff = ONE_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	79	lemmas less_sinlD = below_sinlD
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	80	lemmas less_sinrD = below_sinrD
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names huffman parents: 30910 diff changeset	81
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	82	end

author	blanchet
	Sun, 07 Nov 2010 18:02:02 +0100
changeset 40414	1d3df64b1f88
parent 40329	73f2b99b549d
child 40431	682d6c455670
permissions	-rw-r--r--