src/HOLCF/Pcpo.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 15563 9e125b675253
child 16922 2128ac2aa5db
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     1
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     2
(* legacy ML bindings *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     4
val cpo = thm "cpo";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     5
val least = thm "least";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     6
val UU_def = thm "UU_def";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     7
val chfin = thm "chfin";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     8
val ax_flat = thm "ax_flat";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
     9
val UU_least = thm "UU_least";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    10
val minimal = thm "minimal";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    11
val thelubE = thm "thelubE";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    12
val is_ub_thelub = thm "is_ub_thelub";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    13
val is_lub_thelub = thm "is_lub_thelub";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    14
val lub_range_shift = thm "lub_range_shift";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    15
val maxinch_is_thelub = thm "maxinch_is_thelub";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    16
val lub_mono = thm "lub_mono";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    17
val lub_equal = thm "lub_equal";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    18
val lub_mono2 = thm "lub_mono2";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    19
val lub_equal2 = thm "lub_equal2";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    20
val lub_mono3 = thm "lub_mono3";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    21
val eq_UU_iff = thm "eq_UU_iff";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    22
val UU_I = thm "UU_I";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    23
val not_less2not_eq = thm "not_less2not_eq";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    24
val chain_UU_I = thm "chain_UU_I";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    25
val chain_UU_I_inverse = thm "chain_UU_I_inverse";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    26
val chain_UU_I_inverse2 = thm "chain_UU_I_inverse2";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    27
val notUU_I = thm "notUU_I";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    28
val chain_mono2 = thm "chain_mono2";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    29
val flat_imp_chfin = thm "flat_imp_chfin";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    30
val flat_eq = thm "flat_eq";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    31
val chfin2finch = thm "chfin2finch";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    32
val infinite_chain_adm_lemma = thm "infinite_chain_adm_lemma";
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    33
val increasing_chain_adm_lemma = thm "increasing_chain_adm_lemma";
3326
930c9bed5a09 Moved the classes flat chfin from Fix to Pcpo.
slotosch
parents: 3323
diff changeset
    34
15563
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    35
structure Pcpo =
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    36
struct
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    37
  val thy = the_context ();
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    38
  val UU_def = UU_def;
9e125b675253 converted to new-style theory
huffman
parents: 14981
diff changeset
    39
end;