author  Andreas Lochbihler 
Tue, 01 Dec 2015 12:35:11 +0100  
changeset 61766  507b39df1a57 
child 62058  1cfd5d604937 
permissions  rwrr 
61766
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

1 
(* Title: Bourbaki_Witt_Fixpoint.thy 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

2 
Author: Andreas Lochbihler, ETH Zurich *) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

3 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

4 
section \<open>The BourbakiWitt tower construction for transfinite iteration\<close> 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

5 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

6 
theory Bourbaki_Witt_Fixpoint imports Main begin 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

7 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

8 
lemma ChainsI [intro?]: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

9 
"(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

10 
unfolding Chains_def by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

11 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

12 
lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

13 
by(auto simp add: Chains_def) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

14 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

15 
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

16 
unfolding Field_def by auto 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

17 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

18 
lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

19 
by(auto simp add: Chains_def intro: FieldI1 FieldI2) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

20 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

21 
lemma partial_order_on_trans: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

22 
"\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

23 
by(auto simp add: order_on_defs dest: transD) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

24 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

25 
locale bourbaki_witt_fixpoint = 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

26 
fixes lub :: "'a set \<Rightarrow> 'a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

27 
and leq :: "('a \<times> 'a) set" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

28 
and f :: "'a \<Rightarrow> 'a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

29 
assumes po: "Partial_order leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

30 
and lub_least: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> (x, z) \<in> leq \<rbrakk> \<Longrightarrow> (lub M, z) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

31 
and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

32 
and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

33 
and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

34 
begin 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

35 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

36 
lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

37 
by(rule partial_order_on_trans[OF po]) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

38 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

39 
lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

40 
using po by(simp add: order_on_defs refl_on_def) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

41 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

42 
lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

43 
using po by(simp add: order_on_defs antisym_def) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

44 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

45 
inductive_set iterates_above :: "'a \<Rightarrow> 'a set" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

46 
for a 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

47 
where 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

48 
base: "a \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

49 
 step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

50 
 Sup: "\<lbrakk> M \<in> Chains leq; M \<noteq> {}; \<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above a \<rbrakk> \<Longrightarrow> lub M \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

51 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

52 
definition fixp_above :: "'a \<Rightarrow> 'a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

53 
where "fixp_above a = lub (iterates_above a)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

54 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

55 
context 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

56 
notes leq_refl [intro!, simp] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

57 
and base [intro] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

58 
and step [intro] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

59 
and Sup [intro] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

60 
and leq_trans [trans] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

61 
begin 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

62 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

63 
lemma iterates_above_le_f: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> (x, f x) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

64 
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+ 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

65 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

66 
lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

67 
by(drule (1) iterates_above_le_f)(rule FieldI1) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

68 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

69 
lemma iterates_above_ge: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

70 
assumes y: "y \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

71 
and a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

72 
shows "(a, y) \<in> leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

73 
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper]) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

74 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

75 
lemma iterates_above_lub: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

76 
assumes M: "M \<in> Chains leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

77 
and nempty: "M \<noteq> {}" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

78 
and upper: "\<And>y. y \<in> M \<Longrightarrow> \<exists>z \<in> M. (y, z) \<in> leq \<and> z \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

79 
shows "lub M \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

80 
proof  
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

81 
let ?M = "M \<inter> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

82 
from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

83 
have "?M \<noteq> {}" using nempty by(auto dest: upper) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

84 
with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

85 
also have "lub ?M = lub M" using nempty 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

86 
by(intro leq_antisym)(blast intro!: lub_least[OF M] lub_least[OF M'] intro: lub_upper[OF M'] lub_upper[OF M] leq_trans dest: upper)+ 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

87 
finally show ?thesis . 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

88 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

89 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

90 
lemma iterates_above_successor: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

91 
assumes y: "y \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

92 
and a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

93 
shows "y = a \<or> y \<in> iterates_above (f a)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

94 
using y 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

95 
proof induction 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

96 
case base thus ?case by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

97 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

98 
case (step x) thus ?case by auto 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

99 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

100 
case (Sup M) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

101 
show ?case 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

102 
proof(cases "\<exists>x. M \<subseteq> {x}") 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

103 
case True 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

104 
with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

105 
have "lub M = y" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

106 
by(rule leq_antisym)(auto intro!: lub_upper Sup lub_least ChainsI simp add: a M Sup.hyps(3)[of y, THEN iterates_above_Field] dest: iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

107 
with Sup.IH[of y] M show ?thesis by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

108 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

109 
case False 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

110 
from Sup(12) have "lub M \<in> iterates_above (f a)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

111 
proof(rule iterates_above_lub) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

112 
fix y 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

113 
assume y: "y \<in> M" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

114 
from Sup.IH[OF this] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (f a)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

115 
proof 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

116 
assume "y = a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

117 
from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

118 
with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z] 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

119 
show ?thesis by(auto dest: iterates_above_ge intro: a) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

120 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

121 
assume "y \<in> iterates_above (f a)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

122 
moreover with increasing[OF a] have "y \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

123 
by(auto dest!: iterates_above_Field intro: FieldI2) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

124 
ultimately show ?thesis using y by(auto) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

125 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

126 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

127 
thus ?thesis by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

128 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

129 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

130 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

131 
lemma iterates_above_Sup_aux: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

132 
assumes M: "M \<in> Chains leq" "M \<noteq> {}" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

133 
and M': "M' \<in> Chains leq" "M' \<noteq> {}" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

134 
and comp: "\<And>x. x \<in> M \<Longrightarrow> x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

135 
shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

136 
proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')") 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

137 
case True 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

138 
then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

139 
have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

140 
have "lub M \<in> iterates_above (lub M')" using M 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

141 
proof(rule iterates_above_lub) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

142 
fix y 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

143 
assume y: "y \<in> M" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

144 
from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

145 
proof 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

146 
assume "y \<in> iterates_above (lub M')" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

147 
from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

148 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

149 
assume "lub M' \<in> iterates_above y" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

150 
hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

151 
also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

152 
finally show ?thesis using x by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

153 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

154 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

155 
thus ?thesis .. 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

156 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

157 
case False 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

158 
have "(lub M, lub M') \<in> leq" using M 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

159 
proof(rule lub_least) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

160 
fix x 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

161 
assume x: "x \<in> M" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

162 
from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

163 
moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

164 
ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

165 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

166 
thus ?thesis .. 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

167 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

168 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

169 
lemma iterates_above_triangle: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

170 
assumes x: "x \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

171 
and y: "y \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

172 
and a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

173 
shows "x \<in> iterates_above y \<or> y \<in> iterates_above x" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

174 
using x y 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

175 
proof(induction arbitrary: y) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

176 
case base then show ?case by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

177 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

178 
case (step x) thus ?case using a 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

179 
by(auto dest: iterates_above_successor intro: iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

180 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

181 
case x: (Sup M) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

182 
hence lub: "lub M \<in> iterates_above a" by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

183 
from \<open>y \<in> iterates_above a\<close> show ?case 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

184 
proof(induction) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

185 
case base show ?case using lub by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

186 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

187 
case (step y) thus ?case using a 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

188 
by(auto dest: iterates_above_successor intro: iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

189 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

190 
case y: (Sup M') 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

191 
hence lub': "lub M' \<in> iterates_above a" by blast 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

192 
have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

193 
using that lub' by(rule x.IH) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

194 
with x(12) y(12) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

195 
by(rule iterates_above_Sup_aux) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

196 
moreover from y(12) x(12) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

197 
by(rule iterates_above_Sup_aux)(blast dest: y.IH) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

198 
ultimately show ?case by(auto 4 3 dest: leq_antisym) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

199 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

200 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

201 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

202 
lemma chain_iterates_above: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

203 
assumes a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

204 
shows "iterates_above a \<in> Chains leq" (is "?C \<in> _") 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

205 
proof (rule ChainsI) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

206 
fix x y 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

207 
assume "x \<in> ?C" "y \<in> ?C" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

208 
hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

209 
moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

210 
moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

211 
ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

212 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

213 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

214 
lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

215 
unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+ 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

216 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

217 
lemma 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

218 
assumes b: "b \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

219 
and fb: "f b = b" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

220 
and x: "x \<in> iterates_above a" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

221 
and a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

222 
shows "b \<in> iterates_above x" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

223 
using x 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

224 
proof(induction) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

225 
case base show ?case using b by simp 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

226 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

227 
case (step x) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

228 
from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

229 
from iterates_above_successor[OF step.IH this] fb 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

230 
show ?case by(auto) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

231 
next 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

232 
case (Sup M) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

233 
oops 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

234 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

235 
lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

236 
using fixp_iterates_above by(rule iterates_above_Field) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

237 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

238 
lemma fixp_above_unfold: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

239 
assumes a: "a \<in> Field leq" 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

240 
shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a") 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

241 
proof(rule leq_antisym) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

242 
show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

243 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

244 
have "f ?a \<in> iterates_above a" using fixp_iterates_above[OF a] by(rule iterates_above.step) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

245 
with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" unfolding fixp_above_def by(rule lub_upper) 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

246 
qed 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

247 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

248 
end 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

249 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

250 
end 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

251 

507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

252 
end 