src/HOLCF/Cfun.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16209 36ee7f6af79f
child 16314 7102a1aaecfd
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     1
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     2
(* legacy ML bindings *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     3
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
val less_cfun_def = thm "less_cfun_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
val cfun_cong = thm "cfun_cong";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
val cfun_fun_cong = thm "cfun_fun_cong";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
val cfun_arg_cong = thm "cfun_arg_cong";
16209
36ee7f6af79f removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents: 16099
diff changeset
     8
val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
val beta_cfun = thm "beta_cfun";
15641
b389f108c485 added theorems eta_cfun and cont2cont_eta
huffman
parents: 15576
diff changeset
    10
val eta_cfun = thm "eta_cfun";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
val cont_Rep_CFun2 = thm "cont_Rep_CFun2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
val cont_cfun_arg = thm "cont_cfun_arg";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    15
val contlub_cfun_arg = thm "contlub_cfun_arg";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    16
val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
val monofun_cfun_fun = thm "monofun_cfun_fun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
val monofun_cfun_arg = thm "monofun_cfun_arg";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
val chain_monofun = thm "chain_monofun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
val monofun_cfun = thm "monofun_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
val strictI = thm "strictI";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val lub_cfun_mono = thm "lub_cfun_mono";
16209
36ee7f6af79f removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents: 16099
diff changeset
    25
val ex_lub_cfun = thm "ex_lub_cfun";
36ee7f6af79f removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents: 16099
diff changeset
    26
val cont_lub_cfun = thm "cont_lub_cfun";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
val lub_cfun = thm "lub_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
val thelub_cfun = thm "thelub_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
val ext_cfun = thm "ext_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun";
16209
36ee7f6af79f removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents: 16099
diff changeset
    31
val less_cfun_ext = thm "less_cfun_ext";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
val Istrictify_def = thm "Istrictify_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
val strictify_def = thm "strictify_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
val ID_def = thm "ID_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
val oo_def = thm "oo_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
val inst_cfun_pcpo = thm "inst_cfun_pcpo";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
val cont_Rep_CFun1 = thm "cont_Rep_CFun1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
val contlub_cfun_fun = thm "contlub_cfun_fun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
val cont_cfun_fun = thm "cont_cfun_fun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
val contlub_cfun = thm "contlub_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
val cont_cfun = thm "cont_cfun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
val cont2mono_LAM = thm "cont2mono_LAM";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
val cont2cont_LAM = thm "cont2cont_LAM";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
                    cont2cont_Rep_CFun, cont2cont_LAM];
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
val Istrictify1 = thm "Istrictify1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
val Istrictify2 = thm "Istrictify2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
val monofun_Istrictify2 = thm "monofun_Istrictify2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
val contlub_Istrictify2 = thm "contlub_Istrictify2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
val cont_Istrictify1 = thm "cont_Istrictify1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
val cont_Istrictify2 = thm "cont_Istrictify2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    54
val strictify1 = thm "strictify1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    55
val strictify2 = thm "strictify2";
16209
36ee7f6af79f removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents: 16099
diff changeset
    56
val Rep_CFun_strict1 = thm "Rep_CFun_strict1";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
16085
c004b9bc970e rewrote continuous isomorphism section, cleaned up
huffman
parents: 15641
diff changeset
    58
val retraction_strict = thm "retraction_strict";
c004b9bc970e rewrote continuous isomorphism section, cleaned up
huffman
parents: 15641
diff changeset
    59
val injection_eq = thm "injection_eq";
c004b9bc970e rewrote continuous isomorphism section, cleaned up
huffman
parents: 15641
diff changeset
    60
val injection_defined_rev = thm "injection_defined_rev";
c004b9bc970e rewrote continuous isomorphism section, cleaned up
huffman
parents: 15641
diff changeset
    61
val injection_defined = thm "injection_defined";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
val chfin2chfin = thm "chfin2chfin";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    63
val flat2flat = thm "flat2flat";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    64
val flat_codom = thm "flat_codom";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
val ID1 = thm "ID1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    66
val cfcomp1 = thm "cfcomp1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    67
val cfcomp2 = thm "cfcomp2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
val ID2 = thm "ID2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    69
val ID3 = thm "ID3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    70
val assoc_oo = thm "assoc_oo";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
structure Cfun =
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    73
struct
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    74
  val thy = the_context ();
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    75
  val Istrictify_def = Istrictify_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    76
  val strictify_def = strictify_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
  val ID_def = ID_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    78
  val oo_def = oo_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    79
end;