src/HOLCF/Porder.thy
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12338 de0f4a63baa5
child 14981 e73f8140af78
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/porder.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
12030
wenzelm
parents: 11346
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
     6
Conservative extension of theory Porder0 by constant definitions 
243
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
297
5ef75ff3baeb Franz fragen
nipkow
parents: 243
diff changeset
     9
Porder = Porder0 +
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    11
consts  
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    12
        "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    13
        "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    14
        lub     ::      "'a set => 'a::po"
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 3842
diff changeset
    15
        tord ::      "'a::po set => bool"
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 3842
diff changeset
    16
        chain ::     "(nat=>'a::po) => bool"
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    17
        max_in_chain :: "[nat,nat=>'a::po]=>bool"
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    18
        finite_chain :: "(nat=>'a::po)=>bool"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    20
syntax
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12114
diff changeset
    21
  "@LUB"	:: "('b => 'a) => 'a"	(binder "LUB " 10)
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    22
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    23
translations
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    24
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2640
diff changeset
    25
  "LUB x. t"	== "lub(range(%x. t))"
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    26
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 12030
diff changeset
    27
syntax (xsymbols)
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    28
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    29
  "LUB "	:: "[idts, 'a] => 'a"		("(3\\<Squnion>_./ _)"[0,10] 10)
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    30
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 297
diff changeset
    31
defs
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
(* class definitions *)
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 4721
diff changeset
    34
is_ub_def       "S  <| x == ! y. y:S --> y<<x"
0d28bc664955 corrected ML names of definitions
oheimb
parents: 4721
diff changeset
    35
is_lub_def      "S <<| x == S <| x & (!u. S <| u  --> x << u)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    36
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    37
(* Arbitrary chains are total orders    *)                  
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 4721
diff changeset
    38
tord_def     "tord S == !x y. x:S & y:S --> (x<<y | y<<x)"
243
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
(* Here we use countable chains and I prefer to code them as functions! *)
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 4721
diff changeset
    41
chain_def        "chain F == !i. F i << F (Suc i)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    42
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    43
(* finite chains, needed for monotony of continouous functions *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 297
diff changeset
    44
max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 3842
diff changeset
    45
finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    46
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
    47
lub_def          "lub S == (@x. S <<| x)"
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    48
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    49
end 
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 297
diff changeset
    50
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 297
diff changeset
    51