src/HOLCF/Pcpo.thy
author slotosch
Mon, 17 Feb 1997 10:57:11 +0100
changeset 2640 ee4dfce170a0
parent 2394 91d8abf108be
child 3326 930c9bed5a09
permissions -rw-r--r--
Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     1
(*  Title:      HOLCF/Pcpo.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     2
    ID:         $Id$
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     3
    Author:     Franz Regensburger
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     5
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     6
introduction of the classes cpo and pcpo 
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     7
*)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
Pcpo = Porder +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    10
(* The class cpo of chain complete partial orders *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    11
(* ********************************************** *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    12
axclass cpo < po
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    13
        (* class axiom: *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    14
  cpo   "is_chain S ==> ? x. range(S) <<| (x::'a::po)" 
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    15
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    16
(* The class pcpo of pointed cpos *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    17
(* ****************************** *)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    18
axclass pcpo < cpo
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    19
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    20
  least         "? x.!y.x<<y"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    22
consts
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    23
  UU            :: "'a::pcpo"        
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    24
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    25
syntax (symbols)
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    26
  UU            :: "'a::pcpo"                           ("\\<bottom>")
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    27
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    28
defs
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    29
  UU_def        "UU == @x.!y.x<<y"       
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    30
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
end