src/HOLCF/HOLCF.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 31076 99fe356cbbc2
child 33588 ea9becc59636
permissions -rw-r--r--
merged
clasohm@1479
     1
(*  Title:      HOLCF/HOLCF.thy
clasohm@1479
     2
    Author:     Franz Regensburger
nipkow@243
     3
wenzelm@16841
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     5
*)
nipkow@243
     6
huffman@15650
     7
theory HOLCF
huffman@29130
     8
imports
huffman@29534
     9
  Domain ConvexPD Algebraic Universal Sum_Cpo Main
wenzelm@16841
    10
uses
wenzelm@16841
    11
  "holcf_logic.ML"
wenzelm@23152
    12
  "Tools/adm_tac.ML"
huffman@15650
    13
begin
huffman@15650
    14
huffman@25904
    15
defaultsort pcpo
huffman@25904
    16
wenzelm@26339
    17
declaration {* fn _ =>
wenzelm@26339
    18
  Simplifier.map_ss (fn simpset => simpset addSolver
wenzelm@17612
    19
    (mk_solver' "adm_tac" (fn ss =>
wenzelm@30603
    20
      Adm.adm_tac (Simplifier.the_context ss)
wenzelm@30603
    21
        (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
wenzelm@16841
    22
*}
wenzelm@16841
    23
huffman@31076
    24
text {* Legacy theorem names *}
huffman@31076
    25
huffman@31076
    26
lemmas sq_ord_less_eq_trans = below_eq_trans
huffman@31076
    27
lemmas sq_ord_eq_less_trans = eq_below_trans
huffman@31076
    28
lemmas refl_less = below_refl
huffman@31076
    29
lemmas trans_less = below_trans
huffman@31076
    30
lemmas antisym_less = below_antisym
huffman@31076
    31
lemmas antisym_less_inverse = below_antisym_inverse
huffman@31076
    32
lemmas box_less = box_below
huffman@31076
    33
lemmas rev_trans_less = rev_below_trans
huffman@31076
    34
lemmas not_less2not_eq = not_below2not_eq
huffman@31076
    35
lemmas less_UU_iff = below_UU_iff
huffman@31076
    36
lemmas flat_less_iff = flat_below_iff
huffman@31076
    37
lemmas adm_less = adm_below
huffman@31076
    38
lemmas adm_not_less = adm_not_below
huffman@31076
    39
lemmas adm_compact_not_less = adm_compact_not_below
huffman@31076
    40
lemmas less_fun_def = below_fun_def
huffman@31076
    41
lemmas expand_fun_less = expand_fun_below
huffman@31076
    42
lemmas less_fun_ext = below_fun_ext
huffman@31076
    43
lemmas less_discr_def = below_discr_def
huffman@31076
    44
lemmas discr_less_eq = discr_below_eq
huffman@31076
    45
lemmas less_unit_def = below_unit_def
huffman@31076
    46
lemmas less_cprod_def = below_prod_def
huffman@31076
    47
lemmas prod_lessI = prod_belowI
huffman@31076
    48
lemmas Pair_less_iff = Pair_below_iff
huffman@31076
    49
lemmas fst_less_iff = fst_below_iff
huffman@31076
    50
lemmas snd_less_iff = snd_below_iff
huffman@31076
    51
lemmas expand_cfun_less = expand_cfun_below
huffman@31076
    52
lemmas less_cfun_ext = below_cfun_ext
huffman@31076
    53
lemmas injection_less = injection_below
huffman@31076
    54
lemmas approx_less = approx_below
huffman@31076
    55
lemmas profinite_less_ext = profinite_below_ext
huffman@31076
    56
lemmas less_up_def = below_up_def
huffman@31076
    57
lemmas not_Iup_less = not_Iup_below
huffman@31076
    58
lemmas Iup_less = Iup_below
huffman@31076
    59
lemmas up_less = up_below
huffman@31076
    60
lemmas cpair_less = cpair_below
huffman@31076
    61
lemmas less_cprod = below_cprod
huffman@31076
    62
lemmas cfst_less_iff = cfst_below_iff
huffman@31076
    63
lemmas csnd_less_iff = csnd_below_iff
huffman@31076
    64
lemmas Def_inject_less_eq = Def_below_Def
huffman@31076
    65
lemmas Def_less_is_eq = Def_below_iff
huffman@31076
    66
lemmas spair_less_iff = spair_below_iff
huffman@31076
    67
lemmas less_sprod = below_sprod
huffman@31076
    68
lemmas spair_less = spair_below
huffman@31076
    69
lemmas sfst_less_iff = sfst_below_iff
huffman@31076
    70
lemmas ssnd_less_iff = ssnd_below_iff
huffman@31076
    71
lemmas fix_least_less = fix_least_below
huffman@31076
    72
lemmas dist_less_one = dist_below_one
huffman@31076
    73
lemmas less_ONE = below_ONE
huffman@31076
    74
lemmas ONE_less_iff = ONE_below_iff
huffman@31076
    75
lemmas less_sinlD = below_sinlD
huffman@31076
    76
lemmas less_sinrD = below_sinrD
huffman@31076
    77
huffman@15650
    78
end