src/HOLCF/Cont.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15565 2454493bd77b
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/cont.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     3
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
    Results about continuity and monotonicity
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
*)
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
Cont = Fun3 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
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
   Now we change the default class! Form now on all untyped typevariables are
3323
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents: 2838
diff changeset
    13
   of default class po
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 1479
diff changeset
    18
default po
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    20
consts  
2838
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 1479
diff changeset
    21
        monofun :: "('a => 'b) => bool" (* monotonicity    *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 1479
diff changeset
    22
        contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances)
slotosch
parents: 1479
diff changeset
    23
        cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 1150
diff changeset
    25
defs 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    27
monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    28
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 3842
diff changeset
    29
contlub         "contlub(f) == ! Y. chain(Y) --> 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3323
diff changeset
    30
                                f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    31
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 3842
diff changeset
    32
cont            "cont(f)   == ! Y. chain(Y) --> 
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3323
diff changeset
    33
                                range(% i. f(Y(i))) <<| f(lub(range(Y)))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    34
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
(* the main purpose of cont.thy is to show:                                 *)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    37
(*              monofun(f) & contlub(f)  <==> cont(f)                       *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    39
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    40
end