author  huffman 
Fri, 04 Nov 2005 22:27:40 +0100  
changeset 18088  e5b23b85e932 
parent 18071  940c2c0ff33a 
child 18647  5f5d37e763c4 
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 
9 
imports Main 

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 

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

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

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

16 

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

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

18 
consts 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

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

20 

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

21 
syntax (xsymbols) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

22 
"<<" :: "['a,'a::sq_ord] => bool" (infixl "\<sqsubseteq>" 55) 
15576
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 
axclass po < sq_ord 
15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

25 
 {* class axioms: *} 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

26 
refl_less [iff]: "x \<sqsubseteq> x" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

27 
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

28 
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

29 

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

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

31 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

32 
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

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

34 

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

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

36 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

37 
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

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

39 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

40 
lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d" 
18088  41 
by (rule trans_less [OF trans_less]) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

42 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

43 
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

44 
by (fast elim!: antisym_less_inverse intro!: antisym_less) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

45 

3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

46 
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

47 
by (rule trans_less) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

48 

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

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

50 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

51 
constdefs 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

52 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

53 
 {* class definitions *} 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

54 
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

55 
"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

56 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

57 
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

58 
"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

59 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

60 
 {* Arbitrary chains are total orders *} 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

61 
tord :: "'a::po set \<Rightarrow> bool" 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

62 
"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

63 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

64 
 {* 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

65 
chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

66 
"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

67 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

68 
 {* finite chains, needed for monotony of continuous functions *} 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

69 
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

70 
"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

71 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

72 
finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

73 
"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

74 

940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

75 
lub :: "'a set \<Rightarrow> 'a::po" 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

76 
"lub S \<equiv> THE x. S << x" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

77 

2394  78 
syntax 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

79 
"@LUB" :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a" (binder "LUB " 10) 
2394  80 

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

81 
syntax (xsymbols) 
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

82 
"LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)" [0,10] 10) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

83 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

84 
translations 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

85 
"\<Squnion>n. t" == "lub(range(\<lambda>n. t))" 
15562  86 

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

87 
text {* lubs are unique *} 
15562  88 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

89 
lemma unique_lub: "\<lbrakk>S << x; S << y\<rbrakk> \<Longrightarrow> x = y" 
15562  90 
apply (unfold is_lub_def is_ub_def) 
91 
apply (blast intro: antisym_less) 

92 
done 

93 

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

94 
text {* chains are monotone functions *} 
15562  95 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

96 
lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y" 
15562  97 
apply (unfold chain_def) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

98 
apply (induct_tac y) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

99 
apply simp 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

100 
apply (blast elim: less_SucE intro: trans_less) 
15562  101 
done 
102 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

103 
lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y" 
15562  104 
apply (drule le_imp_less_or_eq) 
105 
apply (blast intro: chain_mono) 

106 
done 

107 

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

108 
text {* The range of a chain is a totally ordered *} 
15562  109 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

110 
lemma chain_tord: "chain F \<Longrightarrow> tord (range F)" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

111 
apply (unfold tord_def, clarify) 
15562  112 
apply (rule nat_less_cases) 
113 
apply (fast intro: chain_mono)+ 

114 
done 

115 

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

116 
text {* technical lemmas about @{term lub} and @{term is_lub} *} 
15562  117 

118 
lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] 

119 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

120 
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

121 
apply (unfold lub_def) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

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

123 
apply assumption 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

124 
apply (erule (1) unique_lub) 
15562  125 
done 
126 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

127 
lemma thelubI: "M << l \<Longrightarrow> lub M = l" 
18088  128 
by (rule unique_lub [OF lubI]) 
15562  129 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

130 
lemma lub_singleton [simp]: "lub {x} = x" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

131 
by (simp add: thelubI is_lub_def is_ub_def) 
15562  132 

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

133 
text {* access to some definition as inference rule *} 
15562  134 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

135 
lemma is_lubD1: "S << x \<Longrightarrow> S < x" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

136 
by (unfold is_lub_def, simp) 
15562  137 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

138 
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

139 
by (unfold is_lub_def, simp) 
15562  140 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

141 
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

142 
by (unfold is_lub_def, fast) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

143 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

144 
lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

145 
by (unfold chain_def, simp) 
15562  146 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

147 
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

148 
by (unfold chain_def, simp) 
15562  149 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

150 
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" 
15562  151 
apply (rule chainI) 
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

152 
apply simp 
15562  153 
apply (erule chainE) 
154 
done 

155 

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

156 
text {* technical lemmas about (least) upper bounds of chains *} 
15562  157 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

158 
lemma ub_rangeD: "range S < x \<Longrightarrow> S i \<sqsubseteq> x" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

159 
by (unfold is_ub_def, simp) 
15562  160 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

161 
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

162 
by (unfold is_ub_def, fast) 
15562  163 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

164 
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

165 
by (rule is_lubD1 [THEN ub_rangeD]) 
15562  166 

16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

167 
lemma is_ub_range_shift: 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

168 
"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

169 
apply (rule iffI) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

170 
apply (rule ub_rangeI) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

171 
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

172 
apply (erule chain_mono3) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

173 
apply (rule le_add1) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

174 
apply (erule ub_rangeD) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

175 
apply (rule ub_rangeI) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

176 
apply (erule ub_rangeD) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

177 
done 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

178 

45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

179 
lemma is_lub_range_shift: 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

180 
"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

181 
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

182 

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

183 
text {* results about finite chains *} 
15562  184 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

185 
lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C << C i" 
15562  186 
apply (unfold max_in_chain_def) 
187 
apply (rule is_lubI) 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

188 
apply (rule ub_rangeI, rename_tac j) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

189 
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

190 
apply simp 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

191 
apply (erule (1) chain_mono3) 
15562  192 
apply (erule ub_rangeD) 
193 
done 

194 

195 
lemma lub_finch2: 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

196 
"finite_chain C \<Longrightarrow> range C << C (LEAST i. max_in_chain i C)" 
15562  197 
apply (unfold finite_chain_def) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

198 
apply (erule conjE) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

199 
apply (erule LeastI2_ex) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

200 
apply (erule (1) lub_finch1) 
15562  201 
done 
202 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

203 
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

204 
by (rule chainI, simp) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

205 

3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

206 
lemma bin_chainmax: 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

207 
"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

208 
by (unfold max_in_chain_def, simp) 
15562  209 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

210 
lemma lub_bin_chain: 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

211 
"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

212 
apply (frule bin_chain) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

213 
apply (drule bin_chainmax) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

214 
apply (drule (1) lub_finch1) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

215 
apply simp 
15562  216 
done 
217 

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

218 
text {* the maximal element in a chain is its lub *} 
15562  219 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

220 
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

221 
by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) 
15562  222 

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

223 
text {* the lub of a constant chain is the constant *} 
15562  224 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

225 
lemma chain_const [simp]: "chain (\<lambda>i. c)" 
17372  226 
by (simp add: chainI) 
227 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

228 
lemma lub_const: "range (\<lambda>x. c) << c" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

229 
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) 
1274  230 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

231 
lemma thelub_const [simp]: "(\<Squnion>i. c) = c" 
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

232 
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

233 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

234 
end 