src/HOLCF/Lift.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16067 c57725e8055a
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:
3655
0531f2c64c91 new extended adm tactic introduced;
mueller
parents: 3457
diff changeset
     1
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     2
(* legacy ML bindings *)
3324
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents:
diff changeset
     3
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     4
structure lift =
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     5
struct
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     6
  val distinct = thms "lift.distinct";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     7
  val inject = thms "lift.inject";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     8
  val exhaust = thm "lift.exhaust";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
     9
  val cases = thms "lift.cases";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    10
  val split = thm "lift.split";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    11
  val split_asm = thm "lift.split_asm";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    12
  val induct = thm "lift.induct";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    13
  val recs = thms "lift.recs";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    14
  val simps = thms "lift.simps";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    15
  val size = thms "lift.size";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    16
end;
3324
6b26b886ff69 Eliminated the prediates flat,chfin
slotosch
parents:
diff changeset
    17
12026
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    18
val Def_not_UU = thm "Def_not_UU";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    19
val DefE = thm "DefE";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    20
val DefE2 = thm "DefE2";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    21
val Def_inject_less_eq = thm "Def_inject_less_eq";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    22
val Def_less_is_eq = thm "Def_less_is_eq";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    23
val Lift_cases = thm "Lift_cases";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    24
val Lift_exhaust = thm "Lift_exhaust";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    25
val UU_lift_def = thm "UU_lift_def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    26
val Undef_eq_UU = thm "Undef_eq_UU";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    27
val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    28
val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    29
val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    30
val cont_flift1_arg = thm "cont_flift1_arg";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    31
val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    32
val cont_flift1_not_arg = thm "cont_flift1_not_arg";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    33
val cont_flift2_arg = thm "cont_flift2_arg";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    34
val cont_if = thm "cont_if";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    35
val flat_imp_chfin_poo = thm "flat_imp_chfin_poo";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    36
val flift1_Def = thm "flift1_Def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    37
val flift1_UU = thm "flift1_UU";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    38
val flift1_def = thm "flift1_def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    39
val flift2_Def = thm "flift2_Def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    40
val flift2_UU = thm "flift2_UU";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    41
val flift2_def = thm "flift2_def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    42
val flift2_nUU = thm "flift2_nUU";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    43
val inst_lift_pcpo = thm "inst_lift_pcpo";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    44
val inst_lift_po = thm "inst_lift_po";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    45
val least_lift = thm "least_lift";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    46
val less_lift = thm "less_lift";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    47
val less_lift_def = thm "less_lift_def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    48
val liftpair_def = thm "liftpair_def";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    49
val minimal_lift = thm "minimal_lift";
0b1d80ada4ab rep_datatype lift;
wenzelm
parents: 10834
diff changeset
    50
val not_Undef_is_Def = thm "not_Undef_is_Def";