author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64911  f0e07600de47 
child 67408  4a4c14b24800 
permissions  rwrr 
62058  1 
(* Title: HOL/Library/Bourbaki_Witt_Fixpoint.thy 
2 
Author: Andreas Lochbihler, ETH Zurich 

62141  3 

4 
Follows G. Smolka, S. SchÃ¤fer and C. Doczkal: Transfinite Constructions in 

5 
Classical Type Theory. ITP 2015 

62058  6 
*) 
61766
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 
section \<open>The BourbakiWitt tower construction for transfinite iteration\<close> 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

9 

63540  10 
theory Bourbaki_Witt_Fixpoint 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

11 
imports While_Combinator 
63540  12 
begin 
61766
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

13 

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

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

15 
"(\<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

16 
unfolding Chains_def by blast 
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 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

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

20 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

21 
lemma in_ChainsD: "\<lbrakk> M \<in> Chains r; x \<in> M; y \<in> M \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

22 
unfolding Chains_def by fast 
61766
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

23 

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

24 
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

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

26 

62622  27 
lemma in_Chains_conv_chain: "M \<in> Chains r \<longleftrightarrow> Complete_Partial_Order.chain (\<lambda>x y. (x, y) \<in> r) M" 
28 
by(simp add: Chains_def chain_def) 

29 

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

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

31 
"\<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

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

33 

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

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

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

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

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

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

39 
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

40 
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

41 
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

42 
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

43 
begin 
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 
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

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

47 

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

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

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

50 

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

51 
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

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

53 

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

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

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

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

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

58 
 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

59 
 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

60 

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

61 
definition fixp_above :: "'a \<Rightarrow> 'a" 
62647  62 
where "fixp_above a = (if a \<in> Field leq then lub (iterates_above a) else a)" 
63 

64 
lemma fixp_above_outside: "a \<notin> Field leq \<Longrightarrow> fixp_above a = a" 

65 
by(simp add: fixp_above_def) 

66 

67 
lemma fixp_above_inside: "a \<in> Field leq \<Longrightarrow> fixp_above a = lub (iterates_above a)" 

68 
by(simp add: fixp_above_def) 

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

69 

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

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

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

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

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

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

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

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

77 

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

78 
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

79 
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

80 

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

81 
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

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

83 

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

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

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

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

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

88 
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

89 

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

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

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

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

93 
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

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

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

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

97 
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

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

99 
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

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

101 
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

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

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

104 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

119 
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

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

121 
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

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

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

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

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

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

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

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

129 
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

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

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

132 
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

133 
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

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

135 
next 
63540  136 
assume *: "y \<in> iterates_above (f a)" 
137 
with increasing[OF a] have "y \<in> Field leq" 

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

138 
by(auto dest!: iterates_above_Field intro: FieldI2) 
63540  139 
with * show ?thesis using y by auto 
61766
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

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

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

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

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

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

145 

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

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

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

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

149 
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

150 
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

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

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

153 
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

154 
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

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

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

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

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

159 
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

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

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

162 
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

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

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

165 
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

166 
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

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

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

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

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

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

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

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

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

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

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

177 
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

178 
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

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

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

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

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

183 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

207 
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

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

209 
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

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

211 
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

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

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

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

215 
qed 
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 chain_iterates_above: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

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

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

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

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

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

223 
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

224 
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

225 
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

226 
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

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

228 

62647  229 
lemma fixp_iterates_above: "fixp_above a \<in> iterates_above a" 
230 
by(auto intro: chain_iterates_above simp add: fixp_above_def) 

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

231 

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

232 
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

233 
using fixp_iterates_above by(rule iterates_above_Field) 
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_unfold: 
507b39df1a57
add formalisation of BourbakiWitt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset

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

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

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

239 
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

240 

62647  241 
have "f ?a \<in> iterates_above a" using fixp_iterates_above by(rule iterates_above.step) 
242 
with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" 

243 
by(simp add: fixp_above_inside assms lub_upper) 

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

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

245 

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

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

247 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

248 
lemma fixp_above_induct [case_names adm base step]: 
62622  249 
assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P" 
250 
and base: "P a" 

251 
and step: "\<And>x. P x \<Longrightarrow> P (f x)" 

252 
shows "P (fixp_above a)" 

62647  253 
proof(cases "a \<in> Field leq") 
254 
case True 

255 
from adm chain_iterates_above[OF True] 

256 
show ?thesis unfolding fixp_above_inside[OF True] in_Chains_conv_chain 

257 
proof(rule ccpo.admissibleD) 

258 
have "a \<in> iterates_above a" .. 

259 
then show "iterates_above a \<noteq> {}" by(auto) 

260 
show "P x" if "x \<in> iterates_above a" for x using that 

261 
by induction(auto intro: base step simp add: in_Chains_conv_chain dest: ccpo.admissibleD[OF adm]) 

262 
qed 

263 
qed(simp add: fixp_above_outside base) 

62622  264 

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

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

266 

63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

267 
subsection \<open>Connect with the while combinator for executability on chainfinite lattices.\<close> 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

268 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

269 
context bourbaki_witt_fixpoint begin 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

270 

64911  271 
lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close> 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

272 
assumes "M \<in> Chains leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

273 
and "M \<noteq> {}" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

274 
and "finite M" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

275 
shows "lub M \<in> M" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

276 
using assms(3,1,2) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

277 
proof induction 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

278 
case empty thus ?case by simp 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

279 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

280 
case (insert x M) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

281 
note chain = \<open>insert x M \<in> Chains leq\<close> 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

282 
show ?case 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

283 
proof(cases "M = {}") 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

284 
case True thus ?thesis 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

285 
using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

286 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

287 
case False 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

288 
from chain have chain': "M \<in> Chains leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

289 
using in_Chains_subset subset_insertI by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

290 
hence "lub M \<in> M" using False by(rule insert.IH) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

291 
show ?thesis 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

292 
proof(cases "(x, lub M) \<in> leq") 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

293 
case True 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

294 
have "(lub (insert x M), lub M) \<in> leq" using chain 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

295 
by (rule lub_least) (auto simp: True intro: lub_upper[OF chain']) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

296 
with False have "lub (insert x M) = lub M" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

297 
using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

298 
with \<open>lub M \<in> M\<close> show ?thesis by simp 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

299 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

300 
case False 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

301 
with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close> 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

302 
have "lub (insert x M) = x" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

303 
by  (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

304 
thus ?thesis by simp 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

305 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

306 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

307 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

308 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

309 
lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

310 
using iterates_above.base iterates_above.step by (induct k) simp_all 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

311 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

312 
lemma chfin_iterates_above_fun_pow: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

313 
assumes "x \<in> iterates_above a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

314 
assumes "\<forall>M \<in> Chains leq. finite M" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

315 
shows "\<exists>j. x = (f ^^ j) a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

316 
using assms(1) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

317 
proof induct 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

318 
case base then show ?case by (simp add: exI[where x=0]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

319 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

320 
case (step x) then obtain j where "x = (f ^^ j) a" by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

321 
with step(1) show ?case by (simp add: exI[where x="Suc j"]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

322 
next 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

323 
case (Sup M) with in_Chains_finite assms(2) show ?case by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

324 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

325 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

326 
lemma Chain_finite_iterates_above_fun_pow_iff: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

327 
assumes "\<forall>M \<in> Chains leq. finite M" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

328 
shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

329 
using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

330 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

331 
lemma fixp_above_Kleene_iter_ex: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

332 
assumes "(\<forall>M \<in> Chains leq. finite M)" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

333 
obtains k where "fixp_above a = (f ^^ k) a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

334 
using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

335 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

336 
context fixes a assumes a: "a \<in> Field leq" begin 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

337 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

338 
lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

339 
using a by (induct k) (auto intro: increasing FieldI2) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

340 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

341 
lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

342 
proof(induct k) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

343 
case (Suc k) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

344 
with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

345 
show ?case by simp (metis less_antisym) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

346 
qed simp 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

347 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

348 
lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

349 
using funpow_Field_leq 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

350 
by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

351 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

352 
lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

353 
using funpow_prefix funpow_suffix[where j="j  k" and k=k] by (cases "j < k") simp_all 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

354 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

355 
lemma funpow_in_Chains: "{(f ^^ k) a k. True} \<in> Chains leq" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

356 
using chain_iterates_above[OF a] fun_pow_iterates_above 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

357 
by (blast intro: ChainsI dest: in_ChainsD) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

358 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

359 
lemma fixp_above_Kleene_iter: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

360 
assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

361 
assumes "(f ^^ Suc k) a = (f ^^ k) a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

362 
shows "fixp_above a = (f ^^ k) a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

363 
proof(rule leq_antisym) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

364 
show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

365 
by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

366 
show "((f ^^ k) a, fixp_above a) \<in> leq" using a 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

367 
by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

368 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

369 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

370 
context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

371 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

372 
lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

373 
apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

374 
apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

375 
apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+ 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

376 
done 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

377 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

378 
lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

379 
by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\<lambda>A. (\<exists>k. A = (f ^^ k) a) \<and> (A, f A) \<in> leq" and s="a"]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

380 
(auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0]) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

381 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

382 
lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

383 
proof  
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

384 
obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

385 
using while_option_finite_increasing by blast 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

386 
with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin] 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

387 
show ?thesis by fastforce 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

388 
qed 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

389 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

390 
lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

391 
unfolding while_def by (rule fixp_above_the_while_option) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

392 

62390  393 
end 
63561
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

394 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

395 
end 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

396 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

397 
end 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

398 

fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

399 
lemma bourbaki_witt_fixpoint_complete_latticeI: 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

400 
fixes f :: "'a::complete_lattice \<Rightarrow> 'a" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

401 
assumes "\<And>x. x \<le> f x" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

402 
shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f" 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

403 
by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least) 
fba08009ff3e
add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents:
63540
diff
changeset

404 

64267  405 
end 