17 -- {* introduce a (syntactic) class for the constant @{text "<<"} *} |
14 -- {* introduce a (syntactic) class for the constant @{text "<<"} *} |
18 axclass sq_ord < type |
15 axclass sq_ord < type |
19 |
16 |
20 -- {* characteristic constant @{text "<<"} for po *} |
17 -- {* characteristic constant @{text "<<"} for po *} |
21 consts |
18 consts |
22 "<<" :: "['a,'a::sq_ord] => bool" (infixl 55) |
19 "<<" :: "['a,'a::sq_ord] => bool" (infixl "<<" 55) |
23 |
20 |
24 syntax (xsymbols) |
21 syntax (xsymbols) |
25 "op <<" :: "['a,'a::sq_ord] => bool" (infixl "\<sqsubseteq>" 55) |
22 "<<" :: "['a,'a::sq_ord] => bool" (infixl "\<sqsubseteq>" 55) |
26 |
23 |
27 axclass po < sq_ord |
24 axclass po < sq_ord |
28 -- {* class axioms: *} |
25 -- {* class axioms: *} |
29 refl_less [iff]: "x << x" |
26 refl_less [iff]: "x \<sqsubseteq> x" |
30 antisym_less: "[|x << y; y << x |] ==> x = y" |
27 antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y" |
31 trans_less: "[|x << y; y << z |] ==> x << z" |
28 trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
32 |
29 |
33 text {* minimal fixes least element *} |
30 text {* minimal fixes least element *} |
34 |
31 |
35 lemma minimal2UU[OF allI] : "!x::'a::po. uu<<x ==> uu=(THE u.!y. u<<y)" |
32 lemma minimal2UU[OF allI] : "\<forall>x::'a::po. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)" |
36 by (blast intro: theI2 antisym_less) |
33 by (blast intro: theI2 antisym_less) |
37 |
34 |
38 text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
35 text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
39 |
36 |
40 lemma antisym_less_inverse: "(x::'a::po)=y ==> x << y & y << x" |
37 lemma antisym_less_inverse: "(x::'a::po) = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" |
41 apply blast |
38 by simp |
42 done |
39 |
43 |
40 lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d" |
44 lemma box_less: "[| (a::'a::po) << b; c << a; b << d|] ==> c << d" |
|
45 apply (erule trans_less) |
41 apply (erule trans_less) |
46 apply (erule trans_less) |
42 apply (erule trans_less) |
47 apply assumption |
43 apply assumption |
48 done |
44 done |
49 |
45 |
50 lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)" |
46 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)" |
51 apply (fast elim!: antisym_less_inverse intro!: antisym_less) |
47 by (fast elim!: antisym_less_inverse intro!: antisym_less) |
52 done |
48 |
|
49 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
|
50 by (rule trans_less) |
53 |
51 |
54 subsection {* Chains and least upper bounds *} |
52 subsection {* Chains and least upper bounds *} |
55 |
53 |
56 consts |
54 consts |
57 "<|" :: "['a set,'a::po] => bool" (infixl 55) |
55 "<|" :: "['a set,'a::po] \<Rightarrow> bool" (infixl "<|" 55) |
58 "<<|" :: "['a set,'a::po] => bool" (infixl 55) |
56 "<<|" :: "['a set,'a::po] \<Rightarrow> bool" (infixl "<<|" 55) |
59 lub :: "'a set => 'a::po" |
57 lub :: "'a set \<Rightarrow> 'a::po" |
60 tord :: "'a::po set => bool" |
58 tord :: "'a::po set \<Rightarrow> bool" |
61 chain :: "(nat=>'a::po) => bool" |
59 chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" |
62 max_in_chain :: "[nat,nat=>'a::po]=>bool" |
60 max_in_chain :: "[nat,nat\<Rightarrow>'a::po]\<Rightarrow>bool" |
63 finite_chain :: "(nat=>'a::po)=>bool" |
61 finite_chain :: "(nat\<Rightarrow>'a::po)\<Rightarrow>bool" |
64 |
62 |
65 syntax |
63 syntax |
66 "@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10) |
64 "@LUB" :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "LUB " 10) |
67 |
65 |
68 translations |
66 translations |
69 "LUB x. t" == "lub(range(%x. t))" |
67 "LUB x. t" == "lub(range(%x. t))" |
70 |
68 |
71 syntax (xsymbols) |
69 syntax (xsymbols) |
72 "LUB " :: "[idts, 'a] => 'a" ("(3\<Squnion>_./ _)"[0,10] 10) |
70 "LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)"[0,10] 10) |
73 |
71 |
74 defs |
72 defs |
75 |
73 |
76 -- {* class definitions *} |
74 -- {* class definitions *} |
77 is_ub_def: "S <| x == ! y. y:S --> y<<x" |
75 is_ub_def: "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x" |
78 is_lub_def: "S <<| x == S <| x & (!u. S <| u --> x << u)" |
76 is_lub_def: "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)" |
79 |
77 |
80 -- {* Arbitrary chains are total orders *} |
78 -- {* Arbitrary chains are total orders *} |
81 tord_def: "tord S == !x y. x:S & y:S --> (x<<y | y<<x)" |
79 tord_def: "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)" |
82 |
80 |
83 -- {* Here we use countable chains and I prefer to code them as functions! *} |
81 -- {* Here we use countable chains and I prefer to code them as functions! *} |
84 chain_def: "chain F == !i. F i << F (Suc i)" |
82 chain_def: "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)" |
85 |
83 |
86 -- {* finite chains, needed for monotony of continouous functions *} |
84 -- {* finite chains, needed for monotony of continuous functions *} |
87 max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" |
85 max_in_chain_def: "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" |
88 finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" |
86 finite_chain_def: "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)" |
89 |
87 |
90 lub_def: "lub S == (THE x. S <<| x)" |
88 lub_def: "lub S \<equiv> THE x. S <<| x" |
91 |
89 |
92 text {* lubs are unique *} |
90 text {* lubs are unique *} |
93 |
91 |
94 lemma unique_lub: |
92 lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y" |
95 "[| S <<| x ; S <<| y |] ==> x=y" |
|
96 apply (unfold is_lub_def is_ub_def) |
93 apply (unfold is_lub_def is_ub_def) |
97 apply (blast intro: antisym_less) |
94 apply (blast intro: antisym_less) |
98 done |
95 done |
99 |
96 |
100 text {* chains are monotone functions *} |
97 text {* chains are monotone functions *} |
101 |
98 |
102 lemma chain_mono [rule_format]: "chain F ==> x<y --> F x<<F y" |
99 lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y" |
103 apply (unfold chain_def) |
100 apply (unfold chain_def) |
104 apply (induct_tac "y") |
101 apply (induct_tac y) |
105 apply auto |
102 apply simp |
106 prefer 2 apply (blast intro: trans_less) |
103 apply (blast elim: less_SucE intro: trans_less) |
107 apply (blast elim!: less_SucE) |
104 done |
108 done |
105 |
109 |
106 lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y" |
110 lemma chain_mono3: "[| chain F; x <= y |] ==> F x << F y" |
|
111 apply (drule le_imp_less_or_eq) |
107 apply (drule le_imp_less_or_eq) |
112 apply (blast intro: chain_mono) |
108 apply (blast intro: chain_mono) |
113 done |
109 done |
114 |
110 |
115 text {* The range of a chain is a totally ordered *} |
111 text {* The range of a chain is a totally ordered *} |
116 |
112 |
117 lemma chain_tord: "chain(F) ==> tord(range(F))" |
113 lemma chain_tord: "chain F \<Longrightarrow> tord (range F)" |
118 apply (unfold tord_def) |
114 apply (unfold tord_def, clarify) |
119 apply safe |
|
120 apply (rule nat_less_cases) |
115 apply (rule nat_less_cases) |
121 apply (fast intro: chain_mono)+ |
116 apply (fast intro: chain_mono)+ |
122 done |
117 done |
123 |
118 |
124 text {* technical lemmas about @{term lub} and @{term is_lub} *} |
119 text {* technical lemmas about @{term lub} and @{term is_lub} *} |
125 |
120 |
126 lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] |
121 lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] |
127 |
122 |
128 lemma lubI[OF exI]: "EX x. M <<| x ==> M <<| lub(M)" |
123 lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M" |
129 apply (unfold lub_def) |
124 apply (unfold lub_def) |
130 apply (rule theI') |
125 apply (rule theI) |
131 apply (erule ex_ex1I) |
126 apply assumption |
132 apply (erule unique_lub) |
127 apply (erule (1) unique_lub) |
133 apply assumption |
128 done |
134 done |
129 |
135 |
130 lemma thelubI: "M <<| l \<Longrightarrow> lub M = l" |
136 lemma thelubI: "M <<| l ==> lub(M) = l" |
|
137 apply (rule unique_lub) |
131 apply (rule unique_lub) |
138 apply (rule lubI) |
132 apply (rule lubI) |
139 apply assumption |
133 apply assumption |
140 apply assumption |
134 apply assumption |
141 done |
135 done |
142 |
136 |
143 lemma lub_singleton [simp]: "lub{x} = x" |
137 lemma lub_singleton [simp]: "lub {x} = x" |
144 apply (simp (no_asm) add: thelubI is_lub_def is_ub_def) |
138 by (simp add: thelubI is_lub_def is_ub_def) |
145 done |
|
146 |
139 |
147 text {* access to some definition as inference rule *} |
140 text {* access to some definition as inference rule *} |
148 |
141 |
149 lemma is_lubD1: "S <<| x ==> S <| x" |
142 lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x" |
150 apply (unfold is_lub_def) |
143 by (unfold is_lub_def, simp) |
151 apply auto |
144 |
152 done |
145 lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" |
153 |
146 by (unfold is_lub_def, simp) |
154 lemma is_lub_lub: "[| S <<| x; S <| u |] ==> x << u" |
147 |
155 apply (unfold is_lub_def) |
148 lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x" |
156 apply auto |
149 by (unfold is_lub_def, fast) |
157 done |
150 |
158 |
151 lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)" |
159 lemma is_lubI: |
152 by (unfold chain_def, simp) |
160 "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x" |
153 |
161 apply (unfold is_lub_def) |
154 lemma chainI: "(\<And>i. F i \<sqsubseteq> F (Suc i)) \<Longrightarrow> chain F" |
162 apply blast |
155 by (unfold chain_def, simp) |
163 done |
156 |
164 |
157 lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" |
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) |
158 apply (rule chainI) |
177 apply simp |
159 apply simp |
178 apply (erule chainE) |
160 apply (erule chainE) |
179 done |
161 done |
180 |
162 |
181 text {* technical lemmas about (least) upper bounds of chains *} |
163 text {* technical lemmas about (least) upper bounds of chains *} |
182 |
164 |
183 lemma ub_rangeD: "range S <| x ==> S(i) << x" |
165 lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x" |
184 apply (unfold is_ub_def) |
166 by (unfold is_ub_def, simp) |
185 apply blast |
167 |
186 done |
168 lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x" |
187 |
169 by (unfold is_ub_def, fast) |
188 lemma ub_rangeI: "(!!i. S i << x) ==> range S <| x" |
170 |
189 apply (unfold is_ub_def) |
171 lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x" |
190 apply blast |
172 by (rule is_lubD1 [THEN ub_rangeD]) |
191 done |
|
192 |
|
193 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] |
|
194 -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) |
|
195 |
173 |
196 lemma is_ub_range_shift: |
174 lemma is_ub_range_shift: |
197 "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x" |
175 "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x" |
198 apply (rule iffI) |
176 apply (rule iffI) |
199 apply (rule ub_rangeI) |
177 apply (rule ub_rangeI) |
209 "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" |
187 "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" |
210 by (simp add: is_lub_def is_ub_range_shift) |
188 by (simp add: is_lub_def is_ub_range_shift) |
211 |
189 |
212 text {* results about finite chains *} |
190 text {* results about finite chains *} |
213 |
191 |
214 lemma lub_finch1: |
192 lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i" |
215 "[| chain C; max_in_chain i C|] ==> range C <<| C i" |
|
216 apply (unfold max_in_chain_def) |
193 apply (unfold max_in_chain_def) |
217 apply (rule is_lubI) |
194 apply (rule is_lubI) |
218 apply (rule ub_rangeI) |
195 apply (rule ub_rangeI, rename_tac j) |
219 apply (rule_tac m = "i" in nat_less_cases) |
196 apply (rule_tac x=i and y=j in linorder_le_cases) |
220 apply (rule antisym_less_inverse [THEN conjunct2]) |
197 apply simp |
221 apply (erule disjI1 [THEN less_or_eq_imp_le, THEN rev_mp]) |
198 apply (erule (1) chain_mono3) |
222 apply (erule spec) |
|
223 apply (rule antisym_less_inverse [THEN conjunct2]) |
|
224 apply (erule disjI2 [THEN less_or_eq_imp_le, THEN rev_mp]) |
|
225 apply (erule spec) |
|
226 apply (erule chain_mono) |
|
227 apply assumption |
|
228 apply (erule ub_rangeD) |
199 apply (erule ub_rangeD) |
229 done |
200 done |
230 |
201 |
231 lemma lub_finch2: |
202 lemma lub_finch2: |
232 "finite_chain(C) ==> range(C) <<| C(LEAST i. max_in_chain i C)" |
203 "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)" |
233 apply (unfold finite_chain_def) |
204 apply (unfold finite_chain_def) |
234 apply (rule lub_finch1) |
205 apply (erule conjE) |
235 prefer 2 apply (best intro: LeastI) |
206 apply (erule LeastI2_ex) |
236 apply blast |
207 apply (erule (1) lub_finch1) |
237 done |
208 done |
238 |
209 |
239 lemma bin_chain: "x<<y ==> chain (%i. if i=0 then x else y)" |
210 lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)" |
240 apply (rule chainI) |
211 by (rule chainI, simp) |
241 apply (induct_tac "i") |
212 |
242 apply auto |
213 lemma bin_chainmax: |
243 done |
214 "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)" |
244 |
215 by (unfold max_in_chain_def, simp) |
245 lemma bin_chainmax: |
216 |
246 "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)" |
217 lemma lub_bin_chain: |
247 apply (unfold max_in_chain_def le_def) |
218 "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y" |
248 apply (rule allI) |
219 apply (frule bin_chain) |
249 apply (induct_tac "j") |
220 apply (drule bin_chainmax) |
250 apply auto |
221 apply (drule (1) lub_finch1) |
251 done |
222 apply simp |
252 |
|
253 lemma lub_bin_chain: "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y" |
|
254 apply (rule_tac s = "if (Suc 0) = 0 then x else y" in subst , rule_tac [2] lub_finch1) |
|
255 apply (erule_tac [2] bin_chain) |
|
256 apply (erule_tac [2] bin_chainmax) |
|
257 apply (simp (no_asm)) |
|
258 done |
223 done |
259 |
224 |
260 text {* the maximal element in a chain is its lub *} |
225 text {* the maximal element in a chain is its lub *} |
261 |
226 |
262 lemma lub_chain_maxelem: "[| Y i = c; ALL i. Y i<<c |] ==> lub(range Y) = c" |
227 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c" |
263 apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) |
228 by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) |
264 done |
|
265 |
229 |
266 text {* the lub of a constant chain is the constant *} |
230 text {* the lub of a constant chain is the constant *} |
267 |
231 |
268 lemma chain_const: "chain (\<lambda>i. c)" |
232 lemma chain_const: "chain (\<lambda>i. c)" |
269 by (simp add: chainI) |
233 by (simp add: chainI) |
270 |
234 |
271 lemma lub_const: "range(%x. c) <<| c" |
235 lemma lub_const: "range (\<lambda>x. c) <<| c" |
272 apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI) |
236 by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) |
273 done |
|
274 |
237 |
275 lemmas thelub_const = lub_const [THEN thelubI, standard] |
238 lemmas thelub_const = lub_const [THEN thelubI, standard] |
276 |
239 |
277 end |
240 end |