author  huffman 
Sat, 04 Jun 2005 00:22:08 +0200  
changeset 16221  879400e029bf 
parent 16092  a1a481ee9425 
child 16318  45b12a01382f 
permissions  rwrr 
15600  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 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 

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

5 
Definition of class porder (partial order). 
16070
4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
15930
diff
changeset

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 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

9 
header {* Partial orders *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

10 

15577  11 
theory Porder 
12 
imports Main 

13 
begin 

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

14 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

15 
subsection {* Type class for partial orders *} 
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

16 

f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

17 
 {* introduce a (syntactic) class for the constant @{text "<<"} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

18 
axclass sq_ord < type 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

19 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

20 
 {* characteristic constant @{text "<<"} for po *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

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

22 
"<<" :: "['a,'a::sq_ord] => bool" (infixl 55) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

23 

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

24 
syntax (xsymbols) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

25 
"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\<sqsubseteq>" 55) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

26 

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

27 
axclass po < sq_ord 
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

28 
 {* class axioms: *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

29 
refl_less [iff]: "x << x" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

30 
antisym_less: "[x << y; y << x ] ==> x = y" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

31 
trans_less: "[x << y; y << z ] ==> x << z" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

32 

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

33 
text {* minimal fixes least element *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

34 

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

35 
lemma minimal2UU[OF allI] : "!x::'a::po. uu<<x ==> uu=(THE u.!y. u<<y)" 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

36 
by (blast intro: theI2 antisym_less) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

37 

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

38 
text {* the reverse law of antisymmetry of @{term "op <<"} *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

39 

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

40 
lemma antisym_less_inverse: "(x::'a::po)=y ==> x << y & y << x" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

41 
apply blast 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

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

43 

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

44 
lemma box_less: "[ (a::'a::po) << b; c << a; b << d] ==> c << d" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

45 
apply (erule trans_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

46 
apply (erule trans_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

47 
apply assumption 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

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

49 

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

50 
lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)" 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

51 
apply (fast elim!: antisym_less_inverse intro!: antisym_less) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

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

53 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

54 
subsection {* Chains and least upper bounds *} 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

55 

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

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

59 
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

60 
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

61 
chain :: "(nat=>'a::po) => bool" 
1479  62 
max_in_chain :: "[nat,nat=>'a::po]=>bool" 
63 
finite_chain :: "(nat=>'a::po)=>bool" 

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

64 

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

66 
"@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) 
2394  67 

68 
translations 

3842  69 
"LUB x. t" == "lub(range(%x. t))" 
2394  70 

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

71 
syntax (xsymbols) 
15562  72 
"LUB " :: "[idts, 'a] => 'a" ("(3\<Squnion>_./ _)"[0,10] 10) 
2394  73 

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

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

75 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

76 
 {* class definitions *} 
15562  77 
is_ub_def: "S < x == ! y. y:S > y<<x" 
78 
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

79 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

80 
 {* Arbitrary chains are total orders *} 
15562  81 
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

82 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

83 
 {* Here we use countable chains and I prefer to code them as functions! *} 
15562  84 
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

85 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

86 
 {* finite chains, needed for monotony of continouous functions *} 
15562  87 
max_in_chain_def: "max_in_chain i C == ! j. i <= j > C(i) = C(j)" 
88 
finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" 

89 

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

90 
lub_def: "lub S == (THE x. S << x)" 
15562  91 

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

92 
text {* lubs are unique *} 
15562  93 

94 
lemma unique_lub: 

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

96 
apply (unfold is_lub_def is_ub_def) 

97 
apply (blast intro: antisym_less) 

98 
done 

99 

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

100 
text {* chains are monotone functions *} 
15562  101 

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

103 
apply (unfold chain_def) 

104 
apply (induct_tac "y") 

105 
apply auto 

106 
prefer 2 apply (blast intro: trans_less) 

107 
apply (blast elim!: less_SucE) 

108 
done 

109 

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

111 
apply (drule le_imp_less_or_eq) 

112 
apply (blast intro: chain_mono) 

113 
done 

114 

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

115 
text {* The range of a chain is a totally ordered *} 
15562  116 

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

118 
apply (unfold tord_def) 

119 
apply safe 

120 
apply (rule nat_less_cases) 

121 
apply (fast intro: chain_mono)+ 

122 
done 

123 

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

124 
text {* technical lemmas about @{term lub} and @{term is_lub} *} 
15562  125 

126 
lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] 

127 

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

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

129 
apply (unfold lub_def) 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

130 
apply (rule theI') 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

131 
apply (erule ex_ex1I) 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

132 
apply (erule unique_lub) 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

133 
apply assumption 
15562  134 
done 
135 

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

137 
apply (rule unique_lub) 

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

138 
apply (rule lubI) 
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

139 
apply assumption 
15562  140 
apply assumption 
141 
done 

142 

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

143 
lemma lub_singleton [simp]: "lub{x} = x" 
15562  144 
apply (simp (no_asm) add: thelubI is_lub_def is_ub_def) 
145 
done 

146 

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

147 
text {* access to some definition as inference rule *} 
15562  148 

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

150 
apply (unfold is_lub_def) 

151 
apply auto 

152 
done 

153 

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

155 
apply (unfold is_lub_def) 

156 
apply auto 

157 
done 

158 

159 
lemma is_lubI: 

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

161 
apply (unfold is_lub_def) 

162 
apply blast 

163 
done 

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

164 

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

167 
apply auto 

168 
done 

169 

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

171 
apply (unfold chain_def) 

172 
apply blast 

173 
done 

174 

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

176 
apply (rule chainI) 

177 
apply clarsimp 

178 
apply (erule chainE) 

179 
done 

180 

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

181 
text {* technical lemmas about (least) upper bounds of chains *} 
15562  182 

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

184 
apply (unfold is_ub_def) 

185 
apply blast 

186 
done 

187 

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

189 
apply (unfold is_ub_def) 

190 
apply blast 

191 
done 

192 

193 
lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

194 
 {* @{thm is_ub_lub} *} (* range(?S1) << ?x1 ==> ?S1(?x) << ?x1 *) 
15562  195 

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

196 
text {* results about finite chains *} 
15562  197 

198 
lemma lub_finch1: 

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

200 
apply (unfold max_in_chain_def) 

201 
apply (rule is_lubI) 

202 
apply (rule ub_rangeI) 

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

204 
apply (rule antisym_less_inverse [THEN conjunct2]) 

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

206 
apply (erule spec) 

207 
apply (rule antisym_less_inverse [THEN conjunct2]) 

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

209 
apply (erule spec) 

210 
apply (erule chain_mono) 

211 
apply assumption 

212 
apply (erule ub_rangeD) 

213 
done 

214 

215 
lemma lub_finch2: 

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

216 
"finite_chain(C) ==> range(C) << C(LEAST i. max_in_chain i C)" 
15562  217 
apply (unfold finite_chain_def) 
218 
apply (rule lub_finch1) 

15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset

219 
prefer 2 apply (best intro: LeastI) 
15562  220 
apply blast 
221 
done 

222 

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

224 
apply (rule chainI) 

225 
apply (induct_tac "i") 

226 
apply auto 

227 
done 

228 

229 
lemma bin_chainmax: 

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

231 
apply (unfold max_in_chain_def le_def) 

232 
apply (rule allI) 

233 
apply (induct_tac "j") 

234 
apply auto 

235 
done 

236 

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

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

239 
apply (erule_tac [2] bin_chain) 

240 
apply (erule_tac [2] bin_chainmax) 

241 
apply (simp (no_asm)) 

242 
done 

243 

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

244 
text {* the maximal element in a chain is its lub *} 
15562  245 

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

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

248 
done 

249 

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

250 
text {* the lub of a constant chain is the constant *} 
15562  251 

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

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

254 
done 

1274  255 

16092  256 
lemmas thelub_const = lub_const [THEN thelubI, standard] 
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset

257 

16092  258 
end 