src/HOLCF/Domain.thy
author wenzelm
Wed Jun 13 18:30:17 2007 +0200 (2007-06-13)
changeset 23376 53317a1ec8b2
parent 23152 9497234a2743
child 25806 2b976fcee6e5
permissions -rw-r--r--
tuned proofs: avoid implicit prems;
tuned;
huffman@15741
     1
(*  Title:      HOLCF/Domain.thy
huffman@15741
     2
    ID:         $Id$
huffman@15741
     3
    Author:     Brian Huffman
huffman@15741
     4
*)
huffman@15741
     5
huffman@15741
     6
header {* Domain package *}
huffman@15741
     7
huffman@15741
     8
theory Domain
huffman@16230
     9
imports Ssum Sprod Up One Tr Fixrec
huffman@15741
    10
begin
huffman@15741
    11
huffman@15741
    12
defaultsort pcpo
huffman@15741
    13
wenzelm@23376
    14
huffman@15741
    15
subsection {* Continuous isomorphisms *}
huffman@15741
    16
huffman@15741
    17
text {* A locale for continuous isomorphisms *}
huffman@15741
    18
huffman@15741
    19
locale iso =
huffman@15741
    20
  fixes abs :: "'a \<rightarrow> 'b"
huffman@15741
    21
  fixes rep :: "'b \<rightarrow> 'a"
huffman@15741
    22
  assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
huffman@15741
    23
  assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
wenzelm@23376
    24
begin
huffman@15741
    25
wenzelm@23376
    26
lemma swap: "iso rep abs"
wenzelm@23376
    27
  by (rule iso.intro [OF rep_iso abs_iso])
huffman@15741
    28
wenzelm@23376
    29
lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
huffman@17835
    30
proof
huffman@17835
    31
  assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
wenzelm@23376
    32
  then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
wenzelm@23376
    33
  then show "x \<sqsubseteq> y" by simp
huffman@17835
    34
next
huffman@17835
    35
  assume "x \<sqsubseteq> y"
wenzelm@23376
    36
  then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
huffman@17835
    37
qed
huffman@17835
    38
wenzelm@23376
    39
lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
wenzelm@23376
    40
  by (rule iso.abs_less [OF swap])
huffman@17835
    41
wenzelm@23376
    42
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
wenzelm@23376
    43
  by (simp add: po_eq_conv abs_less)
huffman@17835
    44
wenzelm@23376
    45
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
wenzelm@23376
    46
  by (rule iso.abs_eq [OF swap])
huffman@17835
    47
wenzelm@23376
    48
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
huffman@15741
    49
proof -
huffman@15741
    50
  have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
wenzelm@23376
    51
  then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
wenzelm@23376
    52
  then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
wenzelm@23376
    53
  then show ?thesis by (rule UU_I)
huffman@15741
    54
qed
huffman@15741
    55
wenzelm@23376
    56
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
wenzelm@23376
    57
  by (rule iso.abs_strict [OF swap])
huffman@15741
    58
wenzelm@23376
    59
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
huffman@15741
    60
proof -
huffman@17835
    61
  have "x = rep\<cdot>(abs\<cdot>x)" by simp
huffman@17835
    62
  also assume "abs\<cdot>x = \<bottom>"
huffman@15741
    63
  also note rep_strict
huffman@17835
    64
  finally show "x = \<bottom>" .
huffman@15741
    65
qed
huffman@15741
    66
wenzelm@23376
    67
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
wenzelm@23376
    68
  by (rule iso.abs_defin' [OF swap])
huffman@15741
    69
wenzelm@23376
    70
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
wenzelm@23376
    71
  by (erule contrapos_nn, erule abs_defin')
huffman@15741
    72
wenzelm@23376
    73
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
wenzelm@23376
    74
  by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
huffman@17835
    75
wenzelm@23376
    76
lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
wenzelm@23376
    77
  by (auto elim: abs_defin' intro: abs_strict)
huffman@17835
    78
wenzelm@23376
    79
lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
wenzelm@23376
    80
  by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
huffman@15741
    81
huffman@17836
    82
lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
huffman@17836
    83
proof (unfold compact_def)
huffman@17836
    84
  assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
huffman@17836
    85
  with cont_Rep_CFun2
huffman@17836
    86
  have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
wenzelm@23376
    87
  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
huffman@17836
    88
qed
huffman@17836
    89
wenzelm@23376
    90
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
wenzelm@23376
    91
  by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
huffman@17836
    92
wenzelm@23376
    93
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
wenzelm@23376
    94
  by (rule compact_rep_rev) simp
huffman@17836
    95
wenzelm@23376
    96
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
wenzelm@23376
    97
  by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
huffman@17836
    98
wenzelm@23376
    99
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
huffman@15741
   100
proof
huffman@15741
   101
  assume "x = abs\<cdot>y"
wenzelm@23376
   102
  then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
wenzelm@23376
   103
  then show "rep\<cdot>x = y" by simp
huffman@15741
   104
next
huffman@15741
   105
  assume "rep\<cdot>x = y"
wenzelm@23376
   106
  then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
wenzelm@23376
   107
  then show "x = abs\<cdot>y" by simp
huffman@15741
   108
qed
huffman@15741
   109
wenzelm@23376
   110
end
wenzelm@23376
   111
wenzelm@23376
   112
huffman@15741
   113
subsection {* Casedist *}
huffman@15741
   114
huffman@15741
   115
lemma ex_one_defined_iff:
huffman@15741
   116
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
huffman@15741
   117
 apply safe
huffman@15741
   118
  apply (rule_tac p=x in oneE)
huffman@15741
   119
   apply simp
huffman@15741
   120
  apply simp
huffman@15741
   121
 apply force
wenzelm@23376
   122
 done
huffman@15741
   123
huffman@15741
   124
lemma ex_up_defined_iff:
huffman@15741
   125
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
huffman@15741
   126
 apply safe
huffman@16754
   127
  apply (rule_tac p=x in upE)
huffman@15741
   128
   apply simp
huffman@15741
   129
  apply fast
huffman@16320
   130
 apply (force intro!: up_defined)
wenzelm@23376
   131
 done
huffman@15741
   132
huffman@15741
   133
lemma ex_sprod_defined_iff:
huffman@15741
   134
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
huffman@15741
   135
  (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
huffman@15741
   136
 apply safe
huffman@15741
   137
  apply (rule_tac p=y in sprodE)
huffman@15741
   138
   apply simp
huffman@15741
   139
  apply fast
huffman@16217
   140
 apply (force intro!: spair_defined)
wenzelm@23376
   141
 done
huffman@15741
   142
huffman@15741
   143
lemma ex_sprod_up_defined_iff:
huffman@15741
   144
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
huffman@15741
   145
  (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
huffman@15741
   146
 apply safe
huffman@15741
   147
  apply (rule_tac p=y in sprodE)
huffman@15741
   148
   apply simp
huffman@16754
   149
  apply (rule_tac p=x in upE)
huffman@15741
   150
   apply simp
huffman@15741
   151
  apply fast
huffman@16217
   152
 apply (force intro!: spair_defined)
wenzelm@23376
   153
 done
huffman@15741
   154
huffman@15741
   155
lemma ex_ssum_defined_iff:
huffman@15741
   156
 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
huffman@15741
   157
 ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
huffman@15741
   158
  (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
huffman@15741
   159
 apply (rule iffI)
huffman@15741
   160
  apply (erule exE)
huffman@15741
   161
  apply (erule conjE)
huffman@15741
   162
  apply (rule_tac p=x in ssumE)
huffman@15741
   163
    apply simp
huffman@15741
   164
   apply (rule disjI1, fast)
huffman@15741
   165
  apply (rule disjI2, fast)
huffman@15741
   166
 apply (erule disjE)
huffman@17835
   167
  apply force
huffman@17835
   168
 apply force
wenzelm@23376
   169
 done
huffman@15741
   170
huffman@15741
   171
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
wenzelm@23376
   172
  by auto
huffman@15741
   173
huffman@15741
   174
lemmas ex_defined_iffs =
huffman@15741
   175
   ex_ssum_defined_iff
huffman@15741
   176
   ex_sprod_up_defined_iff
huffman@15741
   177
   ex_sprod_defined_iff
huffman@15741
   178
   ex_up_defined_iff
huffman@15741
   179
   ex_one_defined_iff
huffman@15741
   180
huffman@15741
   181
text {* Rules for turning exh into casedist *}
huffman@15741
   182
huffman@15741
   183
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
wenzelm@23376
   184
  by auto
huffman@15741
   185
huffman@15741
   186
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
wenzelm@23376
   187
  by rule auto
huffman@15741
   188
huffman@15741
   189
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
wenzelm@23376
   190
  by rule auto
huffman@15741
   191
huffman@15741
   192
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
wenzelm@23376
   193
  by rule auto
huffman@15741
   194
huffman@15741
   195
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
huffman@15741
   196
huffman@15741
   197
huffman@15741
   198
subsection {* Setting up the package *}
huffman@15741
   199
wenzelm@16121
   200
ML {*
huffman@15741
   201
val iso_intro       = thm "iso.intro";
huffman@15741
   202
val iso_abs_iso     = thm "iso.abs_iso";
huffman@15741
   203
val iso_rep_iso     = thm "iso.rep_iso";
huffman@15741
   204
val iso_abs_strict  = thm "iso.abs_strict";
huffman@15741
   205
val iso_rep_strict  = thm "iso.rep_strict";
huffman@15741
   206
val iso_abs_defin'  = thm "iso.abs_defin'";
huffman@15741
   207
val iso_rep_defin'  = thm "iso.rep_defin'";
huffman@15741
   208
val iso_abs_defined = thm "iso.abs_defined";
huffman@15741
   209
val iso_rep_defined = thm "iso.rep_defined";
huffman@17839
   210
val iso_compact_abs = thm "iso.compact_abs";
huffman@17839
   211
val iso_compact_rep = thm "iso.compact_rep";
huffman@15741
   212
val iso_iso_swap    = thm "iso.iso_swap";
huffman@15741
   213
huffman@15741
   214
val exh_start = thm "exh_start";
huffman@15741
   215
val ex_defined_iffs = thms "ex_defined_iffs";
huffman@15741
   216
val exh_casedist0 = thm "exh_casedist0";
huffman@15741
   217
val exh_casedists = thms "exh_casedists";
huffman@15741
   218
*}
huffman@15741
   219
huffman@15741
   220
end