author  huffman 
Wed, 02 Mar 2005 22:30:00 +0100  
changeset 15562  8455c9671494 
parent 14981  e73f8140af78 
child 15576  efb95d0d01f7 
permissions  rwrr 
1479  1 
(* Title: HOLCF/porder.thy 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1479  3 
Author: Franz Regensburger 
15562  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

5 

297  6 
Conservative extension of theory Porder0 by constant definitions 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

8 

15562  9 
theory Porder = Porder0: 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

10 

1479  11 
consts 
12 
"<" :: "['a set,'a::po] => bool" (infixl 55) 

13 
"<<" :: "['a set,'a::po] => bool" (infixl 55) 

14 
lub :: "'a set => 'a::po" 

4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset

15 
tord :: "'a::po set => bool" 
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset

16 
chain :: "(nat=>'a::po) => bool" 
1479  17 
max_in_chain :: "[nat,nat=>'a::po]=>bool" 
18 
finite_chain :: "(nat=>'a::po)=>bool" 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

19 

2394  20 
syntax 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12114
diff
changeset

21 
"@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) 
2394  22 

23 
translations 

24 

3842  25 
"LUB x. t" == "lub(range(%x. t))" 
2394  26 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12030
diff
changeset

27 
syntax (xsymbols) 
2394  28 

15562  29 
"LUB " :: "[idts, 'a] => 'a" ("(3\<Squnion>_./ _)"[0,10] 10) 
2394  30 

1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

31 
defs 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

32 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

33 
(* class definitions *) 
15562  34 
is_ub_def: "S < x == ! y. y:S > y<<x" 
35 
is_lub_def: "S << x == S < x & (!u. S < u > x << u)" 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

36 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

37 
(* Arbitrary chains are total orders *) 
15562  38 
tord_def: "tord S == !x y. x:S & y:S > (x<<y  y<<x)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

39 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

40 
(* Here we use countable chains and I prefer to code them as functions! *) 
15562  41 
chain_def: "chain F == !i. F i << F (Suc i)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

42 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

43 
(* finite chains, needed for monotony of continouous functions *) 
15562  44 
max_in_chain_def: "max_in_chain i C == ! j. i <= j > C(i) = C(j)" 
45 
finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" 

46 

47 
lub_def: "lub S == (@x. S << x)" 

48 

49 
(* Title: HOLCF/Porder 

50 
ID: $Id$ 

51 
Author: Franz Regensburger 

52 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

53 

54 
Conservative extension of theory Porder0 by constant definitions 

55 
*) 

56 

57 
(*  *) 

58 
(* lubs are unique *) 

59 
(*  *) 

60 

61 

62 
lemma unique_lub: 

63 
"[ S << x ; S << y ] ==> x=y" 

64 
apply (unfold is_lub_def is_ub_def) 

65 
apply (blast intro: antisym_less) 

66 
done 

67 

68 
(*  *) 

69 
(* chains are monotone functions *) 

70 
(*  *) 

71 

72 
lemma chain_mono [rule_format]: "chain F ==> x<y > F x<<F y" 

73 
apply (unfold chain_def) 

74 
apply (induct_tac "y") 

75 
apply auto 

76 
prefer 2 apply (blast intro: trans_less) 

77 
apply (blast elim!: less_SucE) 

78 
done 

79 

80 
lemma chain_mono3: "[ chain F; x <= y ] ==> F x << F y" 

81 
apply (drule le_imp_less_or_eq) 

82 
apply (blast intro: chain_mono) 

83 
done 

84 

85 

86 
(*  *) 

87 
(* The range of a chain is a totally ordered << *) 

88 
(*  *) 

89 

90 
lemma chain_tord: "chain(F) ==> tord(range(F))" 

91 
apply (unfold tord_def) 

92 
apply safe 

93 
apply (rule nat_less_cases) 

94 
apply (fast intro: chain_mono)+ 

95 
done 

96 

97 

98 
(*  *) 

99 
(* technical lemmas about lub and is_lub *) 

100 
(*  *) 

101 
lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] 

102 

103 
lemma lubI[OF exI]: "EX x. M << x ==> M << lub(M)" 

104 
apply (simp add: lub some_eq_ex) 

105 
done 

106 

107 
lemma thelubI: "M << l ==> lub(M) = l" 

108 
apply (rule unique_lub) 

109 
apply (subst lub) 

110 
apply (erule someI) 

111 
apply assumption 

112 
done 

113 

114 

115 
lemma lub_singleton: "lub{x} = x" 

116 
apply (simp (no_asm) add: thelubI is_lub_def is_ub_def) 

117 
done 

118 
declare lub_singleton [simp] 

119 

120 
(*  *) 

121 
(* access to some definition as inference rule *) 

122 
(*  *) 

123 

124 
lemma is_lubD1: "S << x ==> S < x" 

125 
apply (unfold is_lub_def) 

126 
apply auto 

127 
done 

128 

129 
lemma is_lub_lub: "[ S << x; S < u ] ==> x << u" 

130 
apply (unfold is_lub_def) 

131 
apply auto 

132 
done 

133 

134 
lemma is_lubI: 

135 
"[ S < x; !!u. S < u ==> x << u ] ==> S << x" 

136 
apply (unfold is_lub_def) 

137 
apply blast 

138 
done 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

139 

15562  140 
lemma chainE: "chain F ==> F(i) << F(Suc(i))" 
141 
apply (unfold chain_def) 

142 
apply auto 

143 
done 

144 

145 
lemma chainI: "(!!i. F i << F(Suc i)) ==> chain F" 

146 
apply (unfold chain_def) 

147 
apply blast 

148 
done 

149 

150 
lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))" 

151 
apply (rule chainI) 

152 
apply clarsimp 

153 
apply (erule chainE) 

154 
done 

155 

156 
(*  *) 

157 
(* technical lemmas about (least) upper bounds of chains *) 

158 
(*  *) 

159 

160 
lemma ub_rangeD: "range S < x ==> S(i) << x" 

161 
apply (unfold is_ub_def) 

162 
apply blast 

163 
done 

164 

165 
lemma ub_rangeI: "(!!i. S i << x) ==> range S < x" 

166 
apply (unfold is_ub_def) 

167 
apply blast 

168 
done 

169 

170 
lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] 

171 
(* range(?S1) << ?x1 ==> ?S1(?x) << ?x1 *) 

172 

173 

174 
(*  *) 

175 
(* results about finite chains *) 

176 
(*  *) 

177 

178 
lemma lub_finch1: 

179 
"[ chain C; max_in_chain i C] ==> range C << C i" 

180 
apply (unfold max_in_chain_def) 

181 
apply (rule is_lubI) 

182 
apply (rule ub_rangeI) 

183 
apply (rule_tac m = "i" in nat_less_cases) 

184 
apply (rule antisym_less_inverse [THEN conjunct2]) 

185 
apply (erule disjI1 [THEN less_or_eq_imp_le, THEN rev_mp]) 

186 
apply (erule spec) 

187 
apply (rule antisym_less_inverse [THEN conjunct2]) 

188 
apply (erule disjI2 [THEN less_or_eq_imp_le, THEN rev_mp]) 

189 
apply (erule spec) 

190 
apply (erule chain_mono) 

191 
apply assumption 

192 
apply (erule ub_rangeD) 

193 
done 

194 

195 
lemma lub_finch2: 

196 
"finite_chain(C) ==> range(C) << C(@ i. max_in_chain i C)" 

197 
apply (unfold finite_chain_def) 

198 
apply (rule lub_finch1) 

199 
prefer 2 apply (best intro: someI) 

200 
apply blast 

201 
done 

202 

203 

204 
lemma bin_chain: "x<<y ==> chain (%i. if i=0 then x else y)" 

205 
apply (rule chainI) 

206 
apply (induct_tac "i") 

207 
apply auto 

208 
done 

209 

210 
lemma bin_chainmax: 

211 
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" 

212 
apply (unfold max_in_chain_def le_def) 

213 
apply (rule allI) 

214 
apply (induct_tac "j") 

215 
apply auto 

216 
done 

217 

218 
lemma lub_bin_chain: "x << y ==> range(%i::nat. if (i=0) then x else y) << y" 

219 
apply (rule_tac s = "if (Suc 0) = 0 then x else y" in subst , rule_tac [2] lub_finch1) 

220 
apply (erule_tac [2] bin_chain) 

221 
apply (erule_tac [2] bin_chainmax) 

222 
apply (simp (no_asm)) 

223 
done 

224 

225 
(*  *) 

226 
(* the maximal element in a chain is its lub *) 

227 
(*  *) 

228 

229 
lemma lub_chain_maxelem: "[ Y i = c; ALL i. Y i<<c ] ==> lub(range Y) = c" 

230 
apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) 

231 
done 

232 

233 
(*  *) 

234 
(* the lub of a constant chain is the constant *) 

235 
(*  *) 

236 

237 
lemma lub_const: "range(%x. c) << c" 

238 
apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI) 

239 
done 

1274  240 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

241 
end 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

242 

74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

243 