src/HOLCF/HOLCF.thy
author huffman
Sun, 28 Feb 2010 14:55:42 -0800
changeset 35473 c4d3d65856dd
parent 33588 ea9becc59636
child 35906 e0382e4b4da7
permissions -rw-r--r--
move some powerdomain stuff into a new file
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     1
(*  Title:      HOLCF/HOLCF.thy
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     2
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
     7
theory HOLCF
29130
685c9e05a6ab new theory Dsum: cpo of disjoint sum
huffman
parents: 28892
diff changeset
     8
imports
35473
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
     9
  Main
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
    10
  Domain
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
    11
  Powerdomains
c4d3d65856dd move some powerdomain stuff into a new file
huffman
parents: 33588
diff changeset
    12
  Sum_Cpo
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    13
uses
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    14
  "holcf_logic.ML"
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents: 19105
diff changeset
    15
  "Tools/adm_tac.ML"
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    16
begin
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    17
25904
8161f137b0e9 new theory of powerdomains
huffman
parents: 23152
diff changeset
    18
defaultsort pcpo
8161f137b0e9 new theory of powerdomains
huffman
parents: 23152
diff changeset
    19
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25904
diff changeset
    20
declaration {* fn _ =>
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 25904
diff changeset
    21
  Simplifier.map_ss (fn simpset => simpset addSolver
17612
5b37787d2d9e adm_tac/cont_tacRs: proper simpset;
wenzelm
parents: 16841
diff changeset
    22
    (mk_solver' "adm_tac" (fn ss =>
30603
71180005f251 proper context for prove_cont/adm_tac;
wenzelm
parents: 29542
diff changeset
    23
      Adm.adm_tac (Simplifier.the_context ss)
71180005f251 proper context for prove_cont/adm_tac;
wenzelm
parents: 29542
diff changeset
    24
        (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
16841
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    25
*}
228d663cc9b3 use all files in HOLCF.thy;
wenzelm
parents: 16054
diff changeset
    26
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    27
text {* Legacy theorem names *}
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    28
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    29
lemmas sq_ord_less_eq_trans = below_eq_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    30
lemmas sq_ord_eq_less_trans = eq_below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    31
lemmas refl_less = below_refl
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    32
lemmas trans_less = below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    33
lemmas antisym_less = below_antisym
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    34
lemmas antisym_less_inverse = below_antisym_inverse
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    35
lemmas box_less = box_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    36
lemmas rev_trans_less = rev_below_trans
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    37
lemmas not_less2not_eq = not_below2not_eq
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    38
lemmas less_UU_iff = below_UU_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    39
lemmas flat_less_iff = flat_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    40
lemmas adm_less = adm_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    41
lemmas adm_not_less = adm_not_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    42
lemmas adm_compact_not_less = adm_compact_not_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    43
lemmas less_fun_def = below_fun_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    44
lemmas expand_fun_less = expand_fun_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    45
lemmas less_fun_ext = below_fun_ext
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    46
lemmas less_discr_def = below_discr_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    47
lemmas discr_less_eq = discr_below_eq
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    48
lemmas less_unit_def = below_unit_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    49
lemmas less_cprod_def = below_prod_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    50
lemmas prod_lessI = prod_belowI
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    51
lemmas Pair_less_iff = Pair_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    52
lemmas fst_less_iff = fst_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    53
lemmas snd_less_iff = snd_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    54
lemmas expand_cfun_less = expand_cfun_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    55
lemmas less_cfun_ext = below_cfun_ext
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    56
lemmas injection_less = injection_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    57
lemmas approx_less = approx_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    58
lemmas profinite_less_ext = profinite_below_ext
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    59
lemmas less_up_def = below_up_def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    60
lemmas not_Iup_less = not_Iup_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    61
lemmas Iup_less = Iup_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    62
lemmas up_less = up_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    63
lemmas cpair_less = cpair_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    64
lemmas less_cprod = below_cprod
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    65
lemmas cfst_less_iff = cfst_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    66
lemmas csnd_less_iff = csnd_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    67
lemmas Def_inject_less_eq = Def_below_Def
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    68
lemmas Def_less_is_eq = Def_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    69
lemmas spair_less_iff = spair_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    70
lemmas less_sprod = below_sprod
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    71
lemmas spair_less = spair_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    72
lemmas sfst_less_iff = sfst_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    73
lemmas ssnd_less_iff = ssnd_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    74
lemmas fix_least_less = fix_least_below
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    75
lemmas dist_less_one = dist_below_one
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    76
lemmas less_ONE = below_ONE
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    77
lemmas ONE_less_iff = ONE_below_iff
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    78
lemmas less_sinlD = below_sinlD
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    79
lemmas less_sinrD = below_sinrD
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30910
diff changeset
    80
15650
b37dc98fbbc5 converted to new-style theory
huffman
parents: 15576
diff changeset
    81
end