src/HOLCF/Domain.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16217 96f0c8546265
child 16223 84a177eeb49c
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15741
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Domain.thy
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     2
    ID:         $Id$
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     3
    Author:     Brian Huffman
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     4
*)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     5
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     6
header {* Domain package *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     7
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     8
theory Domain
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
     9
imports Ssum Sprod One Up
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    10
files
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    11
  ("domain/library.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    12
  ("domain/syntax.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    13
  ("domain/axioms.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    14
  ("domain/theorems.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    15
  ("domain/extender.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    16
  ("domain/interface.ML")
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    17
begin
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    18
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    19
defaultsort pcpo
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    20
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    21
subsection {* Continuous isomorphisms *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    22
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    23
text {* A locale for continuous isomorphisms *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    24
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    25
locale iso =
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    26
  fixes abs :: "'a \<rightarrow> 'b"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    27
  fixes rep :: "'b \<rightarrow> 'a"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    28
  assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    29
  assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    30
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    31
lemma (in iso) swap: "iso rep abs"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    32
by (rule iso.intro [OF rep_iso abs_iso])
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    33
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    34
lemma (in iso) abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    35
proof -
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    36
  have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    37
  hence "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    38
  hence "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    39
  thus ?thesis by (rule UU_I)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    40
qed
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    41
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    42
lemma (in iso) rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    43
by (rule iso.abs_strict [OF swap])
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    44
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    45
lemma (in iso) abs_defin': "abs\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    46
proof -
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    47
  assume A: "abs\<cdot>z = \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    48
  have "z = rep\<cdot>(abs\<cdot>z)" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    49
  also have "\<dots> = rep\<cdot>\<bottom>" by (simp only: A)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    50
  also note rep_strict
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    51
  finally show "z = \<bottom>" .
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    52
qed
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    53
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    54
lemma (in iso) rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    55
by (rule iso.abs_defin' [OF swap])
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    56
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    57
lemma (in iso) abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    58
by (erule contrapos_nn, erule abs_defin')
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    59
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    60
lemma (in iso) rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    61
by (erule contrapos_nn, erule rep_defin')
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    62
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    63
lemma (in iso) iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    64
proof
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    65
  assume "x = abs\<cdot>y"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    66
  hence "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    67
  thus "rep\<cdot>x = y" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    68
next
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    69
  assume "rep\<cdot>x = y"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    70
  hence "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    71
  thus "x = abs\<cdot>y" by simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    72
qed
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    73
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    74
subsection {* Casedist *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    75
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    76
lemma ex_one_defined_iff:
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    77
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    78
 apply safe
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    79
  apply (rule_tac p=x in oneE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    80
   apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    81
  apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    82
 apply force
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    83
done
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    84
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    85
lemma ex_up_defined_iff:
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    86
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    87
 apply safe
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    88
  apply (rule_tac p=x in upE1)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    89
   apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    90
  apply fast
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    91
 apply (force intro!: defined_up)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    92
done
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    93
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    94
lemma ex_sprod_defined_iff:
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    95
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    96
  (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    97
 apply safe
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    98
  apply (rule_tac p=y in sprodE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
    99
   apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   100
  apply fast
16217
96f0c8546265 renamed defined lemmas
huffman
parents: 16121
diff changeset
   101
 apply (force intro!: spair_defined)
15741
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   102
done
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   103
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   104
lemma ex_sprod_up_defined_iff:
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   105
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   106
  (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   107
 apply safe
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   108
  apply (rule_tac p=y in sprodE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   109
   apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   110
  apply (rule_tac p=x in upE1)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   111
   apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   112
  apply fast
16217
96f0c8546265 renamed defined lemmas
huffman
parents: 16121
diff changeset
   113
 apply (force intro!: spair_defined)
15741
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   114
done
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   115
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   116
lemma ex_ssum_defined_iff:
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   117
 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   118
 ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   119
  (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   120
 apply (rule iffI)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   121
  apply (erule exE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   122
  apply (erule conjE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   123
  apply (rule_tac p=x in ssumE)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   124
    apply simp
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   125
   apply (rule disjI1, fast)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   126
  apply (rule disjI2, fast)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   127
 apply (erule disjE)
16217
96f0c8546265 renamed defined lemmas
huffman
parents: 16121
diff changeset
   128
  apply (force intro: sinl_defined)
96f0c8546265 renamed defined lemmas
huffman
parents: 16121
diff changeset
   129
 apply (force intro: sinr_defined)
15741
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   130
done
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   131
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   132
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   133
by auto
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   134
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   135
lemmas ex_defined_iffs =
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   136
   ex_ssum_defined_iff
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   137
   ex_sprod_up_defined_iff
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   138
   ex_sprod_defined_iff
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   139
   ex_up_defined_iff
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   140
   ex_one_defined_iff
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   141
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   142
text {* Rules for turning exh into casedist *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   143
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   144
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   145
by auto
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   146
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   147
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   148
by rule auto
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   149
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   150
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   151
by rule auto
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   152
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   153
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   154
by rule auto
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   155
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   156
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   157
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   158
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   159
subsection {* Setting up the package *}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   160
16121
wenzelm
parents: 16070
diff changeset
   161
ML {*
15741
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   162
val iso_intro       = thm "iso.intro";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   163
val iso_abs_iso     = thm "iso.abs_iso";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   164
val iso_rep_iso     = thm "iso.rep_iso";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   165
val iso_abs_strict  = thm "iso.abs_strict";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   166
val iso_rep_strict  = thm "iso.rep_strict";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   167
val iso_abs_defin'  = thm "iso.abs_defin'";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   168
val iso_rep_defin'  = thm "iso.rep_defin'";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   169
val iso_abs_defined = thm "iso.abs_defined";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   170
val iso_rep_defined = thm "iso.rep_defined";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   171
val iso_iso_swap    = thm "iso.iso_swap";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   172
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   173
val exh_start = thm "exh_start";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   174
val ex_defined_iffs = thms "ex_defined_iffs";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   175
val exh_casedist0 = thm "exh_casedist0";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   176
val exh_casedists = thms "exh_casedists";
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   177
*}
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   178
29a78517543f New file for theorems used by the domain package
huffman
parents:
diff changeset
   179
end