src/HOLCF/Up.thy
author huffman
Sun, 19 Feb 2006 02:11:27 +0100
changeset 19105 3aabd46340e0
parent 18290 5fc309770840
child 25131 2c8caac48ade
permissions -rw-r--r--
use minimal imports
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
     1
(*  Title:      HOLCF/Up.thy
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     2
    ID:         $Id$
16070
4a83dd540b88 removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents: 15599
diff changeset
     3
    Author:     Franz Regensburger and Brian Huffman
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
Lifting.
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
header {* The type of lifted values *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
theory Up
19105
3aabd46340e0 use minimal imports
huffman
parents: 18290
diff changeset
    11
imports Cfun
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    12
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    14
defaultsort cpo
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    15
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    16
subsection {* Definition of new type for lifting *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    18
datatype 'a u = Ibottom | Iup 'a
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    20
syntax (xsymbols)
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    21
  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    22
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
consts
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    24
  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    26
primrec
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    27
  "Ifup f Ibottom = \<bottom>"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    28
  "Ifup f (Iup x) = f\<cdot>x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    30
subsection {* Ordering on lifted cpo *}
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    31
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    32
instance u :: (sq_ord) sq_ord ..
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    34
defs (overloaded)
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    35
  less_up_def:
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    36
    "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    37
      (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    39
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    40
by (simp add: less_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    42
lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    43
by (simp add: less_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    45
lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    46
by (simp add: less_up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    48
subsection {* Lifted cpo is a partial order *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    50
lemma refl_less_up: "(x::'a u) \<sqsubseteq> x"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    51
by (simp add: less_up_def split: u.split)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    53
lemma antisym_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    54
apply (simp add: less_up_def split: u.split_asm)
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    55
apply (erule (1) antisym_less)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    58
lemma trans_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    59
apply (simp add: less_up_def split: u.split_asm)
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    60
apply (erule (1) trans_less)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    61
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    63
instance u :: (cpo) po
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    64
by intro_classes
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    65
  (assumption | rule refl_less_up antisym_less_up trans_less_up)+
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    66
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
    67
subsection {* Lifted cpo is a cpo *}
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    68
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    69
lemma is_lub_Iup:
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    70
  "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
apply (rule ub_rangeI)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    73
apply (subst Iup_less)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    74
apply (erule is_ub_lub)
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    75
apply (case_tac u)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    76
apply (drule ub_rangeD)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    77
apply simp
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    78
apply simp
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    79
apply (erule is_lub_lub)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    80
apply (rule ub_rangeI)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    81
apply (drule_tac i=i in ub_rangeD)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    82
apply simp
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    83
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    84
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    85
text {* Now some lemmas about chains of @{typ "'a u"} elements *}
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    86
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    87
lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    88
by (case_tac z, simp_all)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    89
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    90
lemma up_lemma2:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    91
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    92
apply (erule contrapos_nn)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    93
apply (drule_tac x="j" and y="i + j" in chain_mono3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    94
apply (rule le_add2)
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
    95
apply (case_tac "Y j")
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    96
apply assumption
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
    97
apply simp
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    98
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    99
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   100
lemma up_lemma3:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   101
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   102
by (rule up_lemma1 [OF up_lemma2])
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   103
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   104
lemma up_lemma4:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   105
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   106
apply (rule chainI)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   107
apply (rule Iup_less [THEN iffD1])
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   108
apply (subst up_lemma3, assumption+)+
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   109
apply (simp add: chainE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   110
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   111
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   112
lemma up_lemma5:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   113
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow>
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   114
    (\<lambda>i. Y (i + j)) = (\<lambda>i. Iup (THE a. Iup a = Y (i + j)))"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   115
by (rule ext, rule up_lemma3 [symmetric])
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   116
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   117
lemma up_lemma6:
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   118
  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   119
      \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
16933
91ded127f5f7 fixed var index in tactic;
wenzelm
parents: 16753
diff changeset
   120
apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   121
apply assumption
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   122
apply (subst up_lemma5, assumption+)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   123
apply (rule is_lub_Iup)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   124
apply (rule thelubE [OF _ refl])
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   125
apply (erule (1) up_lemma4)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   126
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   127
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   128
lemma up_chain_lemma:
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   129
  "chain Y \<Longrightarrow>
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   130
   (\<exists>A. chain A \<and> lub (range Y) = Iup (lub (range A)) \<and>
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   131
   (\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   132
apply (rule disjCI)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   133
apply (simp add: expand_fun_eq)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   134
apply (erule exE, rename_tac j)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   135
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   136
apply (simp add: up_lemma4)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   137
apply (simp add: up_lemma6 [THEN thelubI])
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   138
apply (rule_tac x=j in exI)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   139
apply (simp add: up_lemma3)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   140
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   141
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   142
lemma cpo_up: "chain (Y::nat \<Rightarrow> 'a u) \<Longrightarrow> \<exists>x. range Y <<| x"
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   143
apply (frule up_chain_lemma, safe)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   144
apply (rule_tac x="Iup (lub (range A))" in exI)
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   145
apply (erule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   146
apply (simp add: is_lub_Iup thelubE)
17585
f12d7ac88eb4 cleaned up
huffman
parents: 16933
diff changeset
   147
apply (rule exI, rule lub_const)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   148
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   149
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   150
instance u :: (cpo) cpo
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   151
by intro_classes (rule cpo_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   152
18290
5fc309770840 add xsymbol syntax for u type constructor
huffman
parents: 18078
diff changeset
   153
subsection {* Lifted cpo is pointed *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   154
17585
f12d7ac88eb4 cleaned up
huffman
parents: 16933
diff changeset
   155
lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   156
apply (rule_tac x = "Ibottom" in exI)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   157
apply (rule minimal_up [THEN allI])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   158
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   159
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   160
instance u :: (cpo) pcpo
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   161
by intro_classes (rule least_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   162
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   163
text {* for compatibility with old HOLCF-Version *}
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   164
lemma inst_up_pcpo: "\<bottom> = Ibottom"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   165
by (rule minimal_up [THEN UU_I, symmetric])
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   166
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   167
subsection {* Continuity of @{term Iup} and @{term Ifup} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   168
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   169
text {* continuity for @{term Iup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   170
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   171
lemma cont_Iup: "cont Iup"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   172
apply (rule contI)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   173
apply (rule is_lub_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   174
apply (erule thelubE [OF _ refl])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   175
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   176
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   177
text {* continuity for @{term Ifup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   178
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   179
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   180
by (induct x, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   181
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   182
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   183
apply (rule monofunI)
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   184
apply (case_tac x, simp)
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   185
apply (case_tac y, simp)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   186
apply (simp add: monofun_cfun_arg)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   187
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   189
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   190
apply (rule contI)
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   191
apply (frule up_chain_lemma, safe)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   192
apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   193
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   194
apply (simp add: cont_cfun_arg)
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17838
diff changeset
   195
apply (simp add: lub_const)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   196
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   198
subsection {* Continuous versions of constants *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   199
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   200
constdefs  
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   201
  up  :: "'a \<rightarrow> 'a u"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   202
  "up \<equiv> \<Lambda> x. Iup x"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   203
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   204
  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   205
  "fup \<equiv> \<Lambda> f p. Ifup f p"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   206
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   207
translations
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17838
diff changeset
   208
  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17838
diff changeset
   209
  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   210
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   211
text {* continuous versions of lemmas for @{typ "('a)u"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   212
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   213
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   214
apply (induct z)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   215
apply (simp add: inst_up_pcpo)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   216
apply (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   217
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   218
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   219
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   220
by (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   221
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   222
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   223
by simp
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   224
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   225
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   226
by (simp add: up_def cont_Iup inst_up_pcpo)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   227
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   228
lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   229
by (simp add: eq_UU_iff [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   230
16326
50a613925c4e make up_eq and up_less into simp rules
huffman
parents: 16319
diff changeset
   231
lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   232
by (simp add: up_def cont_Iup)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   233
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   234
lemma upE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   235
apply (case_tac p)
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   236
apply (simp add: inst_up_pcpo)
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   237
apply (simp add: up_def cont_Iup)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   239
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   240
lemma up_chain_cases:
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   241
  "chain Y \<Longrightarrow>
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   242
  (\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and>
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   243
  (\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)"
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   244
by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   245
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   246
lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)"
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   247
apply (unfold compact_def)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   248
apply (rule admI)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   249
apply (drule up_chain_cases)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   250
apply (elim disjE exE conjE)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   251
apply simp
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   252
apply (erule (1) admD)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   253
apply (rule allI, drule_tac x="i + j" in spec)
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   254
apply simp
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17838
diff changeset
   255
apply simp
17838
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   256
done
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   257
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   258
text {* properties of fup *}
3032e90c4975 added compactness theorems
huffman
parents: 17585
diff changeset
   259
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   260
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   261
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   262
16319
1ff2965cc2e7 major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents: 16215
diff changeset
   263
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   264
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   265
16553
aa36d41e4263 add csplit3, ssplit3, fup3 as simp rules
huffman
parents: 16326
diff changeset
   266
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
16753
fb6801c926d2 define 'a u with datatype package;
huffman
parents: 16553
diff changeset
   267
by (rule_tac p=x in upE, simp_all)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   268
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   269
end