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