author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 19105  3aabd46340e0 
child 25131  2c8caac48ade 
permissions  rwrr 
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 newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

4 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

5 
Lifting. 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

6 
*) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

7 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

8 
header {* The type of lifted values *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

9 

15577  10 
theory Up 
19105  11 
imports Cfun 
15577  12 
begin 
15576
efb95d0d01f7
converted to newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

17 

16753  18 
datatype 'a u = Ibottom  Iup 'a 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

19 

18290  20 
syntax (xsymbols) 
21 
"u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999) 

22 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

23 
consts 
16753  24 
Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

25 

16753  26 
primrec 
27 
"Ifup f Ibottom = \<bottom>" 

28 
"Ifup f (Iup x) = f\<cdot>x" 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

29 

18290  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 newstyle 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  35 
less_up_def: 
36 
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True  Iup a \<Rightarrow> 

37 
(case y of Ibottom \<Rightarrow> False  Iup b \<Rightarrow> a \<sqsubseteq> b))" 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

38 

16753  39 
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" 
40 
by (simp add: less_up_def) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

41 

16753  42 
lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom" 
43 
by (simp add: less_up_def) 

15576
efb95d0d01f7
converted to newstyle 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  46 
by (simp add: less_up_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

47 

18290  48 
subsection {* Lifted cpo is a partial order *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

49 

16753  50 
lemma refl_less_up: "(x::'a u) \<sqsubseteq> x" 
51 
by (simp add: less_up_def split: u.split) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

52 

16753  53 
lemma antisym_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y" 
54 
apply (simp add: less_up_def split: u.split_asm) 

55 
apply (erule (1) antisym_less) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

56 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

57 

16753  58 
lemma trans_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" 
59 
apply (simp add: less_up_def split: u.split_asm) 

60 
apply (erule (1) trans_less) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

61 
done 
efb95d0d01f7
converted to newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

66 

18290  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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

71 
apply (rule is_lubI) 
efb95d0d01f7
converted to newstyle 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  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 newstyle 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  87 
lemma up_lemma1: "z \<noteq> Ibottom \<Longrightarrow> Iup (THE a. Iup a = z) = z" 
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  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  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  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  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  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  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  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  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  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  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  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  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  147 
apply (rule exI, rule lub_const) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

148 
done 
efb95d0d01f7
converted to newstyle 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  153 
subsection {* Lifted cpo is pointed *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

154 

17585  155 
lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y" 
16753  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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

158 
done 
efb95d0d01f7
converted to newstyle 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 HOLCFVersion *} 
16753  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 newstyle 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  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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

175 
done 
efb95d0d01f7
converted to newstyle 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 newstyle 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  180 
by (induct x, simp_all) 
15576
efb95d0d01f7
converted to newstyle 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  184 
apply (case_tac x, simp) 
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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

187 
done 
efb95d0d01f7
converted to newstyle 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  191 
apply (frule up_chain_lemma, safe) 
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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

196 
done 
efb95d0d01f7
converted to newstyle 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 newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

212 

16753  213 
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" 
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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

217 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

218 

16753  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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

221 

16753  222 
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" 
223 
by simp 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

224 

17838  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 newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

230 

16326  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  234 
lemma upE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
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 newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

238 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

239 

17838  240 
lemma up_chain_cases: 
241 
"chain Y \<Longrightarrow> 

242 
(\<exists>A. chain A \<and> (\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i) \<and> 

243 
(\<exists>j. \<forall>i. Y (i + j) = up\<cdot>(A i))) \<or> Y = (\<lambda>i. \<bottom>)" 

244 
by (simp add: inst_up_pcpo up_def cont_Iup up_chain_lemma) 

245 

246 
lemma compact_up [simp]: "compact x \<Longrightarrow> compact (up\<cdot>x)" 

247 
apply (unfold compact_def) 

248 
apply (rule admI) 

249 
apply (drule up_chain_cases) 

250 
apply (elim disjE exE conjE) 

251 
apply simp 

252 
apply (erule (1) admD) 

253 
apply (rule allI, drule_tac x="i + j" in spec) 

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  256 
done 
257 

258 
text {* properties of fup *} 

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 newstyle 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  264 
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

265 

16553  266 
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" 
16753  267 
by (rule_tac p=x in upE, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

268 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

269 
end 