author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24728  e2b3a1065676 
child 25131  2c8caac48ade 
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 
*) 
c22b85994e17
Franz Regensburger's HigherOrder 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 newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

7 

15577  8 
theory Porder 
24728  9 
imports Datatype Finite_Set 
15577  10 
begin 
15576
efb95d0d01f7
converted to newstyle 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 newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

14 
class sq_ord = type + 
07ae93e58fea
use newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

16 

23284
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

17 
notation 
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

18 
sq_le (infixl "<<" 55) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

19 

23284
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

20 
notation (xsymbols) 
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

21 
sq_le (infixl "\<sqsubseteq>" 55) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

22 

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

23 
axclass po < sq_ord 
23284
07ae93e58fea
use newstyle 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 newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

27 

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

28 
text {* minimal fixes least element *} 
efb95d0d01f7
converted to newstyle 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 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 {* the reverse law of antisymmetry of @{term "op <<"} *} 
efb95d0d01f7
converted to newstyle 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 newstyle 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 newstyle 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 newstyle 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 HigherOrder 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 HigherOrder 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 HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

94 

15562  95 

15576
efb95d0d01f7
converted to newstyle 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 newstyle 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 newstyle 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 newstyle 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 newstyle 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 HigherOrder 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 newstyle 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 newstyle 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 newstyle 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 newstyle 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 