src/HOLCF/Porder.ML
author huffman
Tue, 13 Sep 2005 23:30:01 +0200
changeset 17372 d73f67e90a95
parent 16922 2128ac2aa5db
permissions -rw-r--r--
add theorem chain_const
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
15562
8455c9671494 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
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
     4
val antisym_less_inverse = thm "antisym_less_inverse";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15562
diff changeset
     5
val antisym_less = thm "antisym_less";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
     6
val bin_chainmax = thm "bin_chainmax";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
     7
val bin_chain = thm "bin_chain";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 15562
diff changeset
     8
val box_less = thm "box_less";
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
     9
val chain_def = thm "chain_def";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    10
val chainE = thm "chainE";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    11
val chainI = thm "chainI";
17372
d73f67e90a95 add theorem chain_const
huffman
parents: 16922
diff changeset
    12
val chain_const = thm "chain_const";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    13
val chain_mono3 = thm "chain_mono3";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    14
val chain_mono = thm "chain_mono";
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    15
val chain_shift = thm "chain_shift";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    16
val chain_tord = thm "chain_tord";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    17
val finite_chain_def = thm "finite_chain_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    18
val is_lubD1 = thm "is_lubD1";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    19
val is_lub_def = thm "is_lub_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    20
val is_lubI = thm "is_lubI";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    21
val is_lub_lub = thm "is_lub_lub";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    22
val is_lub_range_shift = thm "is_lub_range_shift";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    23
val is_ub_def = thm "is_ub_def";
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    24
val is_ub_lub = thm "is_ub_lub";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    25
val is_ub_range_shift = thm "is_ub_range_shift";
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    26
val lub_bin_chain = thm "lub_bin_chain";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    27
val lub_chain_maxelem = thm "lub_chain_maxelem";
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    28
val lub_const = thm "lub_const";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    29
val lub_def = thm "lub_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    30
val lub_finch1 = thm "lub_finch1";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    31
val lub_finch2 = thm "lub_finch2";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    32
val lubI = thm "lubI";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    33
val lub_singleton = thm "lub_singleton";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    34
val lub = thm "lub";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    35
val max_in_chain_def = thm "max_in_chain_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    36
val minimal2UU = thm "minimal2UU";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    37
val po_eq_conv = thm "po_eq_conv";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    38
val refl_less = thm "refl_less";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    39
val thelubI = thm "thelubI";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    40
val tord_def = thm "tord_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    41
val trans_less = thm "trans_less";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    42
val ub_rangeD = thm "ub_rangeD";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    43
val ub_rangeI = thm "ub_rangeI";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 15576
diff changeset
    44
val unique_lub = thm "unique_lub";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    45
15562
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    46
structure Porder =
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    47
struct
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    48
  val thy = the_context ();
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    49
  val is_ub_def = is_ub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    50
  val is_lub_def = is_lub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    51
  val tord_def = tord_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    52
  val chain_def = chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    53
  val max_in_chain_def = max_in_chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    54
  val finite_chain_def = finite_chain_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    55
  val lub_def = lub_def;
8455c9671494 converted to new-style theory
huffman
parents: 14981
diff changeset
    56
end;