src/HOLCF/Up.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16215 7ff978ca1920
child 16319 1ff2965cc2e7
permissions -rw-r--r--
New theory with lemmas for the fixrec package
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
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    11
imports Cfun Sum_Type Datatype
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
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    18
typedef (Up) ('a) "u" = "UNIV :: (unit + 'a) set" ..
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
consts
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
  Iup         :: "'a => ('a)u"
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
    22
  Ifup        :: "('a->'b)=>('a)u => 'b::pcpo"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
defs
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
  Iup_def:     "Iup x == Abs_Up(Inr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
  Ifup_def:    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
lemma Abs_Up_inverse2: "Rep_Up (Abs_Up y) = y"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    29
by (simp add: Up_def Abs_Up_inverse)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
lemma Exh_Up: "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
apply (rule Rep_Up_inverse [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
apply (rule_tac s = "Rep_Up z" in sumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
apply (rule_tac f = "Abs_Up" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
apply (rule unit_eq [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
apply (rule_tac f = "Abs_Up" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
lemma inj_Abs_Up: "inj(Abs_Up)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
apply (rule Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
lemma inj_Rep_Up: "inj(Rep_Up)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
apply (rule Rep_Up_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    54
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    55
lemma inject_Iup [dest!]: "Iup x=Iup y ==> x=y"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
apply (rule inj_Inr [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    58
apply (rule inj_Abs_Up [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    60
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    61
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
lemma defined_Iup: "Iup x~=Abs_Up(Inl ())"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    63
apply (unfold Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    64
apply (rule notI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    66
apply (rule Inl_not_Inr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    67
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
apply (erule inj_Abs_Up [THEN injD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    69
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    70
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
lemma upE: "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
apply (rule Exh_Up [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    73
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    74
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    75
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    76
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    78
lemma Ifup1 [simp]: "Ifup(f)(Abs_Up(Inl ()))=UU"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    79
apply (unfold Ifup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    80
apply (subst Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    81
apply (subst sum_case_Inl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    82
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    83
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    84
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    85
lemma Ifup2 [simp]: "Ifup(f)(Iup(x))=f$x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    86
apply (unfold Ifup_def Iup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    87
apply (subst Abs_Up_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    88
apply (subst sum_case_Inr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    89
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    90
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    91
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    92
subsection {* Ordering on type @{typ "'a u"} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    93
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    94
instance u :: (sq_ord) sq_ord ..
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    95
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    96
defs (overloaded)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    97
  less_up_def: "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    98
               Inl(y1) => True          
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    99
             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   100
                                            | Inr(z2) => y2<<z2))"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   101
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   102
lemma less_up1a [iff]: 
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   103
        "Abs_Up(Inl ())<< z"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   104
by (simp add: less_up_def Abs_Up_inverse2)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   105
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   106
lemma less_up1b [iff]: 
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   107
        "~(Iup x) << (Abs_Up(Inl ()))"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   108
by (simp add: Iup_def less_up_def Abs_Up_inverse2)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   109
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   110
lemma less_up1c [iff]: 
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
        "(Iup x) << (Iup y)=(x<<y)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   112
by (simp add: Iup_def less_up_def Abs_Up_inverse2)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   113
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   114
subsection {* Type @{typ "'a u"} is a partial order *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   115
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   116
lemma refl_less_up: "(p::'a u) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   117
apply (rule_tac p = "p" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   118
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   119
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   120
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   121
lemma antisym_less_up: "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   122
apply (rule_tac p = "p1" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   123
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   125
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   126
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   127
apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   128
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   129
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   130
apply (drule antisym_less, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   131
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   132
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   133
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   134
lemma trans_less_up: "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   135
apply (rule_tac p = "p1" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   136
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   137
apply (rule_tac p = "p2" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   139
apply (rule_tac p = "p3" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   141
apply (blast intro: trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   142
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   143
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   144
instance u :: (cpo) po
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   145
by intro_classes
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   146
  (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
   147
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   148
text {* for compatibility with old HOLCF-Version *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   149
lemma inst_up_po: "(op <<)=(%x1 x2. case Rep_Up(x1) of                 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   150
                Inl(y1) => True  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   151
              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   152
                                             | Inr(z2) => y2<<z2))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   153
apply (fold less_up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   154
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   155
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   156
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   157
subsection {* Monotonicity of @{term Iup} and @{term Ifup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   158
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   159
lemma monofun_Iup: "monofun(Iup)"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   160
by (simp add: monofun_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   161
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   162
lemma monofun_Ifup1: "monofun(Ifup)"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   163
apply (rule monofunI)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   164
apply (rule less_fun [THEN iffD2, rule_format])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   165
apply (rule_tac p = "xa" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   166
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   168
apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   169
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   170
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   171
lemma monofun_Ifup2: "monofun(Ifup(f))"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   172
apply (rule monofunI)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   173
apply (rule_tac p = "x" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   174
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   175
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   176
apply (rule_tac p = "y" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   177
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   178
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   179
apply (erule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   180
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   181
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   182
subsection {* Type @{typ "'a u"} is a cpo *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   183
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   184
text {* Some kind of surjectivity lemma *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   185
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   186
lemma up_lemma1: "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   187
by simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   189
lemma lub_up1a: "[|chain(Y);EX i x. Y(i)=Iup(x)|]  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   190
      ==> range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   191
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   192
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   193
apply (rule_tac p = "Y (i) " in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   194
apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   195
apply (erule sym)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   196
apply (rule less_up1a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
apply (rule_tac t = "Y (i) " in up_lemma1 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   198
apply assumption
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   199
apply (rule less_up1c [THEN iffD2])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   200
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   201
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   202
apply (rule_tac p = "u" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   203
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   204
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   205
apply (rule_tac P = "Y (i) <<Abs_Up (Inl ())" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   206
apply (rule_tac s = "Iup (x) " and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   207
apply assumption
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   208
apply (rule less_up1b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   209
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   210
apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   211
apply (rule_tac t = "u" in up_lemma1 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   212
apply assumption
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   213
apply (rule less_up1c [THEN iffD2])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   214
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   215
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   216
apply (erule monofun_Ifup2 [THEN ub2ub_monofun])
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   219
lemma lub_up1b: "[|chain(Y); ALL i x. Y(i)~=Iup(x)|] ==> range(Y) <<| Abs_Up (Inl ())"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   220
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   221
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   222
apply (rule_tac p = "Y (i) " in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   223
apply (rule_tac s = "Abs_Up (Inl ())" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   224
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   225
apply (rule refl_less)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   226
apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   227
apply (rule less_up1a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   228
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   229
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   230
lemmas thelub_up1a = lub_up1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   231
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   232
[| chain ?Y1; EX i x. ?Y1 i = Iup x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   233
 lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   234
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   235
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   236
lemmas thelub_up1b = lub_up1b [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   237
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
[| chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   239
 lub (range ?Y1) = UU_up
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   240
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   241
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   242
text {* New versions where @{typ "'a"} does not have to be a pcpo *}
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   243
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   244
lemma up_lemma1a: "EX x. z=Iup(x) ==> Iup(THE a. Iup a = z) = z"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   245
apply (erule exE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   246
apply (rule theI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   247
apply (erule sym)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   248
apply simp
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   249
apply (erule inject_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   250
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   251
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   252
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
   253
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   254
lemma up_chain_lemma1:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   255
  "[| chain Y; EX x. Y j = Iup x |] ==> EX x. Y (i + j) = Iup x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   256
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
   257
apply (rule le_add2)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   258
apply (rule_tac p="Y (i + j)" in upE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   259
apply auto
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   260
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   261
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   262
lemma up_chain_lemma2:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   263
  "[| chain Y; EX x. Y j = Iup x |] ==>
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   264
    Iup (THE a. Iup a = Y (i + j)) = Y (i + j)"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   265
apply (drule_tac i=i in up_chain_lemma1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   266
apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   267
apply (erule up_lemma1a)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   268
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   269
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   270
lemma up_chain_lemma3:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   271
  "[| chain Y; EX x. Y j = Iup x |] ==> chain (%i. THE a. Iup a = Y (i + j))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   272
apply (rule chainI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   273
apply (rule less_up1c [THEN iffD1])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   274
apply (simp only: up_chain_lemma2)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   275
apply (simp add: chainE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   276
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   277
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   278
lemma up_chain_lemma4:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   279
  "[| chain Y; EX x. Y j = Iup x |] ==>
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   280
    (%i. Y (i + j)) = (%i. Iup (THE a. Iup a = Y (i + j)))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   281
apply (rule ext)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   282
apply (rule up_chain_lemma2 [symmetric])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   283
apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   284
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   285
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   286
lemma is_lub_range_shift:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   287
  "[| chain S; range (%i. S (i + j)) <<| x |] ==> range S <<| x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   288
apply (rule is_lubI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   289
apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   290
apply (rule trans_less)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   291
apply (erule chain_mono3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   292
apply (rule le_add1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   293
apply (erule is_ub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   294
apply (erule is_lub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   295
apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   296
apply (erule ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   297
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   298
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   299
lemma is_lub_Iup:
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   300
  "range S <<| x \<Longrightarrow> range (%i. Iup (S i)) <<| Iup x"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   301
apply (rule is_lubI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   302
apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   303
apply (subst less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   304
apply (erule is_ub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   305
apply (rule_tac p=u in upE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   306
apply (drule ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   307
apply (simp only: less_up1b)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   308
apply (simp only: less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   309
apply (erule is_lub_lub)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   310
apply (rule ub_rangeI)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   311
apply (drule_tac i=i in ub_rangeD)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   312
apply (simp only: less_up1c)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   313
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   314
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   315
lemma lub_up1c: "[|chain(Y); EX x. Y(j)=Iup(x)|]  
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   316
      ==> range(Y) <<| Iup(lub(range(%i. THE a. Iup a = Y(i + j))))"
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   317
apply (rule_tac j=j in is_lub_range_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   318
apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   319
apply (subst up_chain_lemma4)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   320
apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   321
apply (rule is_lub_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   322
apply (rule thelubE [OF _ refl])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   323
apply (rule up_chain_lemma3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   324
apply assumption+
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   325
done
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   326
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   327
lemmas thelub_up1c = lub_up1c [THEN thelubI, standard]
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   328
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   329
lemma cpo_up: "chain(Y::nat=>('a)u) ==> EX x. range(Y) <<|x"
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   330
apply (case_tac "EX i x. Y i = Iup x")
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   331
apply (erule exE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   332
apply (rule exI)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   333
apply (erule lub_up1c)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   334
apply assumption
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   335
apply (rule exI)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   336
apply (erule lub_up1b)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   337
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   338
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   339
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   340
instance u :: (cpo) cpo
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   341
by intro_classes (rule cpo_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   342
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   343
subsection {* Type @{typ "'a u"} is pointed *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   344
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   345
lemma minimal_up: "Abs_Up(Inl ()) << z"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   346
by (rule less_up1a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   347
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   348
lemmas UU_up_def = minimal_up [THEN minimal2UU, symmetric, standard]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   349
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   350
lemma least_up: "EX x::'a u. ALL y. x<<y"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   351
apply (rule_tac x = "Abs_Up (Inl ())" in exI)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   352
apply (rule minimal_up [THEN allI])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   353
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   354
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   355
instance u :: (cpo) pcpo
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   356
by intro_classes (rule least_up)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   357
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   358
text {* for compatibility with old HOLCF-Version *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   359
lemma inst_up_pcpo: "UU = Abs_Up(Inl ())"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   360
by (simp add: UU_def UU_up_def)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   361
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   362
text {* some lemmas restated for class pcpo *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   363
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   364
lemma less_up3b: "~ Iup(x) << UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   365
apply (subst inst_up_pcpo)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   366
apply (rule less_up1b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   367
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   368
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   369
lemma defined_Iup2 [iff]: "Iup(x) ~= UU"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   370
apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   371
apply (rule defined_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   372
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   373
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   374
subsection {* Continuity of @{term Iup} and @{term Ifup} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   375
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   376
text {* continuity for @{term Iup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   377
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   378
lemma cont_Iup [iff]: "cont(Iup)"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   379
apply (rule contI)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   380
apply (rule is_lub_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   381
apply (erule thelubE [OF _ refl])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   382
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   383
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   384
lemmas contlub_Iup = cont_Iup [THEN cont2contlub]
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   385
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   386
text {* continuity for @{term Ifup} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   387
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   388
lemma contlub_Ifup1: "contlub(Ifup)"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   389
apply (rule contlubI)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   390
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   391
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   392
apply (erule_tac [2] monofun_Ifup1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   393
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   394
apply (rule_tac p = "x" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   395
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   396
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   397
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   398
apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   399
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   400
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   401
lemma contlub_Ifup2: "contlub(Ifup(f))"
16215
7ff978ca1920 changed to use new contlubI, etc.
huffman
parents: 16070
diff changeset
   402
apply (rule contlubI)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   403
apply (case_tac "EX i x. Y i = Iup x")
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   404
apply (erule exE)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   405
apply (subst thelub_up1c)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   406
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   407
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   408
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   409
prefer 2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   410
apply (subst thelub_up1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   411
apply assumption
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   412
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   413
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   414
apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   415
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   416
apply (rule_tac p = "Y(i)" in upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   417
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   418
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   419
apply (subst contlub_cfun_arg)
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   420
apply  (erule up_chain_lemma3)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   421
apply  assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   422
apply (rule trans)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   423
prefer 2
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   424
apply (rule_tac j=i in lub_range_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   425
apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   426
apply (rule lub_equal [rule_format])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   427
apply (rule chain_monofun)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   428
apply (erule up_chain_lemma3)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   429
apply assumption
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   430
apply (rule monofun_Ifup2 [THEN ch2ch_monofun])
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   431
apply (erule chain_shift)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   432
apply (drule_tac i=k in up_chain_lemma1)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   433
apply assumption
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   434
apply clarify
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   435
apply simp
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   436
apply (subst the_equality)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   437
apply (rule refl)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   438
apply (erule inject_Iup)
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   439
apply (rule refl)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   440
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   441
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   442
lemma cont_Ifup1: "cont(Ifup)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   443
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   444
apply (rule monofun_Ifup1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   445
apply (rule contlub_Ifup1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   446
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   447
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   448
lemma cont_Ifup2: "cont(Ifup(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   449
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   450
apply (rule monofun_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   451
apply (rule contlub_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   452
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   453
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   454
subsection {* Continuous versions of constants *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   455
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   456
constdefs  
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   457
        up  :: "'a -> ('a)u"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   458
       "up  == (LAM x. Iup(x))"
15599
10cedbd5289e instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents: 15593
diff changeset
   459
        fup :: "('a->'c)-> ('a)u -> 'c::pcpo"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   460
       "fup == (LAM f p. Ifup(f)(p))"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   461
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   462
translations
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   463
"case l of up$x => t1" == "fup$(LAM x. t1)$l"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   464
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   465
text {* continuous versions of lemmas for @{typ "('a)u"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   466
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   467
lemma Exh_Up1: "z = UU | (EX x. z = up$x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   468
apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   469
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   470
apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   471
apply (rule Exh_Up)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   472
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   473
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   474
lemma inject_up: "up$x=up$y ==> x=y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   475
apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   476
apply (rule inject_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   477
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   478
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   479
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   480
lemma defined_up [simp]: " up$x ~= UU"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   481
by (simp add: up_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   482
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   483
lemma upE1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   484
        "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   485
apply (unfold up_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   486
apply (rule upE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   487
apply (simp only: inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   488
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   489
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   490
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   491
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   492
lemmas up_conts = cont_lemmas1 cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   493
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   494
lemma fup1 [simp]: "fup$f$UU=UU"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   495
apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   496
apply (subst inst_up_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   497
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   498
apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   499
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   500
apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   501
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   502
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   503
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   504
lemma fup2 [simp]: "fup$f$(up$x)=f$x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   505
apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   506
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   507
apply (rule cont_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   508
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   509
apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   510
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   511
apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   512
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   513
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   514
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   515
lemma less_up4b: "~ up$x << UU"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   516
by (simp add: up_def fup_def less_up3b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   517
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   518
lemma less_up4c: "(up$x << up$y) = (x<<y)"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   519
by (simp add: up_def fup_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   520
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   521
lemma thelub_up2a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   522
"[| chain(Y); EX i x. Y(i) = up$x |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   523
       lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   524
apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   525
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   526
apply (rule cont_Iup)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   527
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   528
apply (intro up_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   529
apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   530
apply (rule cont_Ifup2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   531
apply (rule thelub_up1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   532
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   533
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   534
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   535
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   536
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   537
apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   538
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   539
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   540
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   541
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   542
lemma thelub_up2b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   543
"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   544
apply (unfold up_def fup_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   545
apply (subst inst_up_pcpo)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   546
apply (erule thelub_up1b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   547
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   548
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   549
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   550
lemma up_lemma2: "(EX x. z = up$x) = (z~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   551
apply (rule iffI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   552
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   553
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   554
apply (rule_tac p = "z" in upE1)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   555
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   556
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   557
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   558
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   559
lemma thelub_up2a_rev:
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   560
  "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   561
apply (rule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   562
apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   563
apply (rule up_lemma2 [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   564
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   565
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   566
apply (rule up_lemma2 [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   567
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   568
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   569
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   570
lemma thelub_up2b_rev:
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   571
  "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   572
by (blast dest!: chain_UU_I [THEN spec] exI [THEN up_lemma2 [THEN iffD1]])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   573
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   574
lemma thelub_up3: "chain(Y) ==> lub(range(Y)) = UU |  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   575
                   lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   576
apply (rule disjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   577
apply (rule_tac [2] disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   578
apply (rule_tac [2] thelub_up2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   579
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   580
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   581
apply (rule_tac [2] disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   582
apply (rule_tac [2] thelub_up2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   583
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   584
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   585
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   586
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   587
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   588
lemma fup3: "fup$up$x=x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   589
apply (rule_tac p = "x" in upE1)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   590
apply simp
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   591
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   592
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   593
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   594
text {* for backward compatibility *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   595
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   596
lemmas less_up2b = less_up1b
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   597
lemmas less_up2c = less_up1c
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   598
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   599
end