author | wenzelm |
Wed, 13 Jun 2007 14:21:54 +0200 | |
changeset 23371 | ed60e560048d |
parent 23284 | 07ae93e58fea |
child 24728 | e2b3a1065676 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Porder.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
6 |
header {* Partial orders *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
7 |
|
15577 | 8 |
theory Porder |
19621 | 9 |
imports Finite_Set |
15577 | 10 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
11 |
|
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
12 |
subsection {* Type class for partial orders *} |
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
13 |
|
23284
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
14 |
class sq_ord = type + |
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
15 |
fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
16 |
|
23284
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
17 |
notation |
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
18 |
sq_le (infixl "<<" 55) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
19 |
|
23284
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
20 |
notation (xsymbols) |
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
21 |
sq_le (infixl "\<sqsubseteq>" 55) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
22 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
23 |
axclass po < sq_ord |
23284
07ae93e58fea
use new-style class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset
|
24 |
refl_less [iff]: "x \<sqsubseteq> x" |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
25 |
antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
26 |
trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
27 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
28 |
text {* minimal fixes least element *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
29 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
30 |
lemma minimal2UU[OF allI] : "\<forall>x::'a::po. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)" |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
31 |
by (blast intro: theI2 antisym_less) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
32 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
33 |
text {* the reverse law of anti-symmetry of @{term "op <<"} *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
34 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
35 |
lemma antisym_less_inverse: "(x::'a::po) = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
36 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
37 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
38 |
lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d" |
18088 | 39 |
by (rule trans_less [OF trans_less]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
40 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
41 |
lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
42 |
by (fast elim!: antisym_less_inverse intro!: antisym_less) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
43 |
|
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
44 |
lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
45 |
by (rule trans_less) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
46 |
|
18647 | 47 |
lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
48 |
by (rule subst) |
|
49 |
||
50 |
lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
|
51 |
by (rule ssubst) |
|
52 |
||
53 |
lemmas HOLCF_trans_rules [trans] = |
|
54 |
trans_less |
|
55 |
antisym_less |
|
56 |
sq_ord_less_eq_trans |
|
57 |
sq_ord_eq_less_trans |
|
58 |
||
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset
|
59 |
subsection {* Chains and least upper bounds *} |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
|
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
61 |
constdefs |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
62 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
63 |
-- {* class definitions *} |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
64 |
is_ub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<|" 55) |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
65 |
"S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
66 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
67 |
is_lub :: "['a set, 'a::po] \<Rightarrow> bool" (infixl "<<|" 55) |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
68 |
"S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
69 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
70 |
-- {* Arbitrary chains are total orders *} |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
71 |
tord :: "'a::po set \<Rightarrow> bool" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
72 |
"tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
73 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
74 |
-- {* Here we use countable chains and I prefer to code them as functions! *} |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
75 |
chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
76 |
"chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
77 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
78 |
-- {* finite chains, needed for monotony of continuous functions *} |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
79 |
max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
80 |
"max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
81 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
82 |
finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
83 |
"finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
84 |
|
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
85 |
lub :: "'a set \<Rightarrow> 'a::po" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
86 |
"lub S \<equiv> THE x. S <<| x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
|
21524 | 88 |
abbreviation |
89 |
Lub (binder "LUB " 10) where |
|
90 |
"LUB n. t n == lub (range t)" |
|
2394 | 91 |
|
21524 | 92 |
notation (xsymbols) |
93 |
Lub (binder "\<Squnion> " 10) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
15562 | 95 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
96 |
text {* lubs are unique *} |
15562 | 97 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
98 |
lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y" |
15562 | 99 |
apply (unfold is_lub_def is_ub_def) |
100 |
apply (blast intro: antisym_less) |
|
101 |
done |
|
102 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
103 |
text {* chains are monotone functions *} |
15562 | 104 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
105 |
lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y" |
15562 | 106 |
apply (unfold chain_def) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
107 |
apply (induct_tac y) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
108 |
apply simp |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
109 |
apply (blast elim: less_SucE intro: trans_less) |
15562 | 110 |
done |
111 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
112 |
lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y" |
15562 | 113 |
apply (drule le_imp_less_or_eq) |
114 |
apply (blast intro: chain_mono) |
|
115 |
done |
|
116 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
117 |
text {* The range of a chain is a totally ordered *} |
15562 | 118 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
119 |
lemma chain_tord: "chain F \<Longrightarrow> tord (range F)" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
120 |
apply (unfold tord_def, clarify) |
15562 | 121 |
apply (rule nat_less_cases) |
122 |
apply (fast intro: chain_mono)+ |
|
123 |
done |
|
124 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
125 |
text {* technical lemmas about @{term lub} and @{term is_lub} *} |
15562 | 126 |
|
127 |
lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] |
|
128 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
129 |
lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M" |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
130 |
apply (unfold lub_def) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
131 |
apply (rule theI) |
15930
145651bc64a8
Replaced all unnecessary uses of SOME with THE or LEAST
huffman
parents:
15600
diff
changeset
|
132 |
apply assumption |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
133 |
apply (erule (1) unique_lub) |
15562 | 134 |
done |
135 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
136 |
lemma thelubI: "M <<| l \<Longrightarrow> lub M = l" |
18088 | 137 |
by (rule unique_lub [OF lubI]) |
15562 | 138 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
139 |
lemma lub_singleton [simp]: "lub {x} = x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
140 |
by (simp add: thelubI is_lub_def is_ub_def) |
15562 | 141 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
142 |
text {* access to some definition as inference rule *} |
15562 | 143 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
144 |
lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
145 |
by (unfold is_lub_def, simp) |
15562 | 146 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
147 |
lemma is_lub_lub: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
148 |
by (unfold is_lub_def, simp) |
15562 | 149 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
150 |
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
151 |
by (unfold is_lub_def, fast) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
152 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
153 |
lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
154 |
by (unfold chain_def, simp) |
15562 | 155 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
156 |
lemma chainI: "(\<And>i. F i \<sqsubseteq> F (Suc i)) \<Longrightarrow> chain F" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
157 |
by (unfold chain_def, simp) |
15562 | 158 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
159 |
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" |
15562 | 160 |
apply (rule chainI) |
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
161 |
apply simp |
15562 | 162 |
apply (erule chainE) |
163 |
done |
|
164 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
165 |
text {* technical lemmas about (least) upper bounds of chains *} |
15562 | 166 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
167 |
lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
168 |
by (unfold is_ub_def, simp) |
15562 | 169 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
170 |
lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
171 |
by (unfold is_ub_def, fast) |
15562 | 172 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
173 |
lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
174 |
by (rule is_lubD1 [THEN ub_rangeD]) |
15562 | 175 |
|
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
176 |
lemma is_ub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
177 |
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x" |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
178 |
apply (rule iffI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
179 |
apply (rule ub_rangeI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
180 |
apply (rule_tac y="S (i + j)" in trans_less) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
181 |
apply (erule chain_mono3) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
182 |
apply (rule le_add1) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
183 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
184 |
apply (rule ub_rangeI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
185 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
186 |
done |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
187 |
|
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
188 |
lemma is_lub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
189 |
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
190 |
by (simp add: is_lub_def is_ub_range_shift) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
191 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
192 |
text {* results about finite chains *} |
15562 | 193 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
194 |
lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i" |
15562 | 195 |
apply (unfold max_in_chain_def) |
196 |
apply (rule is_lubI) |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
197 |
apply (rule ub_rangeI, rename_tac j) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
198 |
apply (rule_tac x=i and y=j in linorder_le_cases) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
199 |
apply simp |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
200 |
apply (erule (1) chain_mono3) |
15562 | 201 |
apply (erule ub_rangeD) |
202 |
done |
|
203 |
||
204 |
lemma lub_finch2: |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
205 |
"finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)" |
15562 | 206 |
apply (unfold finite_chain_def) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
207 |
apply (erule conjE) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
208 |
apply (erule LeastI2_ex) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
209 |
apply (erule (1) lub_finch1) |
15562 | 210 |
done |
211 |
||
19621 | 212 |
lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)" |
213 |
apply (unfold finite_chain_def, clarify) |
|
214 |
apply (rule_tac f="Y" and n="Suc i" in nat_seg_image_imp_finite) |
|
215 |
apply (rule equalityI) |
|
216 |
apply (rule subsetI) |
|
217 |
apply (erule rangeE, rename_tac j) |
|
218 |
apply (rule_tac x=i and y=j in linorder_le_cases) |
|
219 |
apply (subgoal_tac "Y j = Y i", simp) |
|
220 |
apply (simp add: max_in_chain_def) |
|
221 |
apply simp |
|
222 |
apply fast |
|
223 |
done |
|
224 |
||
225 |
lemma finite_tord_has_max [rule_format]: |
|
226 |
"finite S \<Longrightarrow> S \<noteq> {} \<longrightarrow> tord S \<longrightarrow> (\<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y)" |
|
227 |
apply (erule finite_induct, simp) |
|
228 |
apply (rename_tac a S, clarify) |
|
229 |
apply (case_tac "S = {}", simp) |
|
230 |
apply (drule (1) mp) |
|
231 |
apply (drule mp, simp add: tord_def) |
|
232 |
apply (erule bexE, rename_tac z) |
|
233 |
apply (subgoal_tac "a \<sqsubseteq> z \<or> z \<sqsubseteq> a") |
|
234 |
apply (erule disjE) |
|
235 |
apply (rule_tac x="z" in bexI, simp, simp) |
|
236 |
apply (rule_tac x="a" in bexI) |
|
237 |
apply (clarsimp elim!: rev_trans_less) |
|
238 |
apply simp |
|
239 |
apply (simp add: tord_def) |
|
240 |
done |
|
241 |
||
242 |
lemma finite_range_imp_finch: |
|
243 |
"\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y" |
|
244 |
apply (subgoal_tac "\<exists>y\<in>range Y. \<forall>x\<in>range Y. x \<sqsubseteq> y") |
|
245 |
apply (clarsimp, rename_tac i) |
|
246 |
apply (subgoal_tac "max_in_chain i Y") |
|
247 |
apply (simp add: finite_chain_def exI) |
|
248 |
apply (simp add: max_in_chain_def po_eq_conv chain_mono3) |
|
249 |
apply (erule finite_tord_has_max, simp) |
|
250 |
apply (erule chain_tord) |
|
251 |
done |
|
252 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
253 |
lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
254 |
by (rule chainI, simp) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
255 |
|
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
256 |
lemma bin_chainmax: |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
257 |
"x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
258 |
by (unfold max_in_chain_def, simp) |
15562 | 259 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
260 |
lemma lub_bin_chain: |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
261 |
"x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
262 |
apply (frule bin_chain) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
263 |
apply (drule bin_chainmax) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
264 |
apply (drule (1) lub_finch1) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
265 |
apply simp |
15562 | 266 |
done |
267 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
268 |
text {* the maximal element in a chain is its lub *} |
15562 | 269 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
270 |
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
271 |
by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) |
15562 | 272 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
273 |
text {* the lub of a constant chain is the constant *} |
15562 | 274 |
|
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
275 |
lemma chain_const [simp]: "chain (\<lambda>i. c)" |
17372 | 276 |
by (simp add: chainI) |
277 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
278 |
lemma lub_const: "range (\<lambda>x. c) <<| c" |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
279 |
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) |
1274 | 280 |
|
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
281 |
lemma thelub_const [simp]: "(\<Squnion>i. c) = c" |
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
282 |
by (rule lub_const [THEN thelubI]) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
297
diff
changeset
|
283 |
|
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
284 |
end |