src/HOL/HOLCF/HOLCF.thy
author wenzelm
Thu, 03 Mar 2011 18:10:28 +0100
changeset 41886 aa8dce9ab8a9
parent 41430 1aa23e9f2c87
child 42151 4da4fc77664b
permissions -rw-r--r--
discontinued legacy load path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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