isabelle: src/HOL/HOLCF/HOLCF.thy@1e008cc4883a (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
40497 d2e876d6da8c rename class 'bifinite' to 'domain' huffman parents: 40431 diff changeset	14	default_sort "domain"
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	15
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	16	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	17
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	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	19	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	20	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	21	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	22	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	23	lemmas below_cfun_ext = cfun_belowI
40011 b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	24	lemmas monofun_fun_fun = fun_belowD
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	25	lemmas monofun_fun_arg = monofunE
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	26	lemmas monofun_lub_fun = adm_monofun [THEN admD]
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names huffman parents: 40002 diff changeset	27	lemmas cont_lub_fun = adm_cont [THEN admD]
40326 73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	28	lemmas cont2cont_Rep_CFun = cont2cont_APP
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	29	lemmas cont_Rep_CFun_app = cont_APP_app
73d45866dbda renamed lemma cont2cont_Rep_CFun to cont2cont_APP huffman parents: 40011 diff changeset	30	lemmas cont_Rep_CFun_app_app = cont_APP_app_app
40771 1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS) huffman parents: 40497 diff changeset	31	lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS) huffman parents: 40497 diff changeset	32	lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
41027 c599955d9806 add lemmas lub_APP, lub_LAM huffman parents: 40774 diff changeset	33	lemmas contlub_cfun = lub_APP [symmetric]
c599955d9806 add lemmas lub_APP, lub_LAM huffman parents: 40774 diff changeset	34	lemmas contlub_LAM = lub_LAM [symmetric]
40771 1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS) huffman parents: 40497 diff changeset	35	lemmas thelubI = lub_eqI
41430 1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	36	lemmas UU_I = bottomI
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	37	lemmas lift_distinct1 = lift.distinct(1)
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	38	lemmas lift_distinct2 = lift.distinct(2)
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	39	lemmas Def_not_UU = lift.distinct(2)
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	40	lemmas Def_inject = lift.inject
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	41	lemmas below_UU_iff = below_bottom_iff
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom' huffman parents: 41414 diff changeset	42	lemmas eq_UU_iff = eq_bottom_iff
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	43
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	44	end

author	bulwahn
	Fri, 11 Mar 2011 15:21:13 +0100
changeset 41930	1e008cc4883a
parent 41886	aa8dce9ab8a9
child 42151	4da4fc77664b
permissions	-rw-r--r--