src/HOLCF/Cont.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16204 5dd79d3f0105
child 16388 1ff571813848
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
15565
2454493bd77b 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
16204
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 15565
diff changeset
     4
val monofun_def = thm "monofun_def";
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 15565
diff changeset
     5
val contlub_def = thm "contlub_def";
5dd79d3f0105 renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
huffman
parents: 15565
diff changeset
     6
val cont_def = thm "cont_def";
15565
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
     7
val contlubI = thm "contlubI";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
     8
val contlubE = thm "contlubE";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
     9
val contI = thm "contI";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    10
val contE = thm "contE";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    11
val monofunI = thm "monofunI";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    12
val monofunE = thm "monofunE";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    13
val ch2ch_monofun = thm "ch2ch_monofun";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    14
val ub2ub_monofun = thm "ub2ub_monofun";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    15
val monocontlub2cont = thm "monocontlub2cont";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    16
val binchain_cont = thm "binchain_cont";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    17
val cont2mono = thm "cont2mono";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    18
val cont2contlub = thm "cont2contlub";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    19
val monofun_finch2finch = thm "monofun_finch2finch";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    20
val cont_finch2finch = thm "cont_finch2finch";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    21
val monofun_fun_fun = thm "monofun_fun_fun";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    22
val monofun_fun_arg = thm "monofun_fun_arg";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    23
val mono2mono_MF1L = thm "mono2mono_MF1L";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    24
val cont2cont_CF1L = thm "cont2cont_CF1L";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    25
val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    26
val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    27
val contlub_abstraction = thm "contlub_abstraction";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    28
val mono2mono_app = thm "mono2mono_app";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    29
val cont2contlub_app = thm "cont2contlub_app";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    30
val cont2cont_app = thm "cont2cont_app";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    31
val cont2cont_app2 = thm "cont2cont_app2";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    32
val cont_id = thm "cont_id";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    33
val cont_const = thm "cont_const";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    34
val cont2cont_app3 = thm "cont2cont_app3";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    35
val flatdom2monofun = thm "flatdom2monofun";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    36
val chfindom_monofun2cont = thm "chfindom_monofun2cont";
2454493bd77b converted to new-style theory
huffman
parents: 14981
diff changeset
    37
val flatdom_strict2cont = thm "flatdom_strict2cont";