author | Andreas Lochbihler |
Tue, 12 Jan 2016 14:14:28 +0100 | |
changeset 62139 | 519362f817c7 |
parent 62058 | 1cfd5d604937 |
child 62141 | 00bfdf4bf237 |
permissions | -rw-r--r-- |
62058 | 1 |
(* Title: HOL/Library/Bourbaki_Witt_Fixpoint.thy |
2 |
Author: Andreas Lochbihler, ETH Zurich |
|
3 |
*) |
|
61766
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
4 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
5 |
section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close> |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
6 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
7 |
theory Bourbaki_Witt_Fixpoint imports Main begin |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
8 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
9 |
lemma ChainsI [intro?]: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
10 |
"(\<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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
11 |
unfolding Chains_def by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
12 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
13 |
lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
14 |
by(auto simp add: Chains_def) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
15 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
16 |
lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
17 |
unfolding Field_def by auto |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
18 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
19 |
lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
20 |
by(auto simp add: Chains_def intro: FieldI1 FieldI2) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
21 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
22 |
lemma partial_order_on_trans: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
23 |
"\<lbrakk> partial_order_on A r; (x, y) \<in> r; (y, z) \<in> r \<rbrakk> \<Longrightarrow> (x, z) \<in> r" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
24 |
by(auto simp add: order_on_defs dest: transD) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
25 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
26 |
locale bourbaki_witt_fixpoint = |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
27 |
fixes lub :: "'a set \<Rightarrow> 'a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
28 |
and leq :: "('a \<times> 'a) set" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
29 |
and f :: "'a \<Rightarrow> 'a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
30 |
assumes po: "Partial_order leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
31 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
32 |
and lub_upper: "\<lbrakk> M \<in> Chains leq; x \<in> M \<rbrakk> \<Longrightarrow> (x, lub M) \<in> leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
33 |
and lub_in_Field: "\<lbrakk> M \<in> Chains leq; M \<noteq> {} \<rbrakk> \<Longrightarrow> lub M \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
34 |
and increasing: "\<And>x. x \<in> Field leq \<Longrightarrow> (x, f x) \<in> leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
35 |
begin |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
36 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
37 |
lemma leq_trans: "\<lbrakk> (x, y) \<in> leq; (y, z) \<in> leq \<rbrakk> \<Longrightarrow> (x, z) \<in> leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
38 |
by(rule partial_order_on_trans[OF po]) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
39 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
40 |
lemma leq_refl: "x \<in> Field leq \<Longrightarrow> (x, x) \<in> leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
41 |
using po by(simp add: order_on_defs refl_on_def) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
42 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
43 |
lemma leq_antisym: "\<lbrakk> (x, y) \<in> leq; (y, x) \<in> leq \<rbrakk> \<Longrightarrow> x = y" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
44 |
using po by(simp add: order_on_defs antisym_def) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
45 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
46 |
inductive_set iterates_above :: "'a \<Rightarrow> 'a set" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
47 |
for a |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
48 |
where |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
49 |
base: "a \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
50 |
| step: "x \<in> iterates_above a \<Longrightarrow> f x \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
51 |
| 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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
52 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
53 |
definition fixp_above :: "'a \<Rightarrow> 'a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
54 |
where "fixp_above a = lub (iterates_above a)" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
55 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
56 |
context |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
57 |
notes leq_refl [intro!, simp] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
58 |
and base [intro] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
59 |
and step [intro] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
60 |
and Sup [intro] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
61 |
and leq_trans [trans] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
62 |
begin |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
63 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
64 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
65 |
by(induction x rule: iterates_above.induct)(blast intro: increasing FieldI2 lub_in_Field)+ |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
66 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
67 |
lemma iterates_above_Field: "\<lbrakk> x \<in> iterates_above a; a \<in> Field leq \<rbrakk> \<Longrightarrow> x \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
68 |
by(drule (1) iterates_above_le_f)(rule FieldI1) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
69 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
70 |
lemma iterates_above_ge: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
71 |
assumes y: "y \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
72 |
and a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
73 |
shows "(a, y) \<in> leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
74 |
using y by(induction)(auto intro: a increasing iterates_above_le_f leq_trans leq_trans[OF _ lub_upper]) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
75 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
76 |
lemma iterates_above_lub: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
77 |
assumes M: "M \<in> Chains leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
78 |
and nempty: "M \<noteq> {}" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
79 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
80 |
shows "lub M \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
81 |
proof - |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
82 |
let ?M = "M \<inter> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
83 |
from M have M': "?M \<in> Chains leq" by(rule in_Chains_subset)simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
84 |
have "?M \<noteq> {}" using nempty by(auto dest: upper) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
85 |
with M' have "lub ?M \<in> iterates_above a" by(rule Sup) blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
86 |
also have "lub ?M = lub M" using nempty |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
87 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
88 |
finally show ?thesis . |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
89 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
90 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
91 |
lemma iterates_above_successor: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
92 |
assumes y: "y \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
93 |
and a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
94 |
shows "y = a \<or> y \<in> iterates_above (f a)" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
95 |
using y |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
96 |
proof induction |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
97 |
case base thus ?case by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
98 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
99 |
case (step x) thus ?case by auto |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
100 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
101 |
case (Sup M) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
102 |
show ?case |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
103 |
proof(cases "\<exists>x. M \<subseteq> {x}") |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
104 |
case True |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
105 |
with \<open>M \<noteq> {}\<close> obtain y where M: "M = {y}" by auto |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
106 |
have "lub M = y" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
107 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
108 |
with Sup.IH[of y] M show ?thesis by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
109 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
110 |
case False |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
111 |
from Sup(1-2) have "lub M \<in> iterates_above (f a)" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
112 |
proof(rule iterates_above_lub) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
113 |
fix y |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
114 |
assume y: "y \<in> M" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
115 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
116 |
proof |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
117 |
assume "y = a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
118 |
from y False obtain z where z: "z \<in> M" and neq: "y \<noteq> z" by (metis insertI1 subsetI) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
119 |
with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z] |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
120 |
show ?thesis by(auto dest: iterates_above_ge intro: a) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
121 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
122 |
assume "y \<in> iterates_above (f a)" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
123 |
moreover with increasing[OF a] have "y \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
124 |
by(auto dest!: iterates_above_Field intro: FieldI2) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
125 |
ultimately show ?thesis using y by(auto) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
126 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
127 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
128 |
thus ?thesis by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
129 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
130 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
131 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
132 |
lemma iterates_above_Sup_aux: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
133 |
assumes M: "M \<in> Chains leq" "M \<noteq> {}" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
134 |
and M': "M' \<in> Chains leq" "M' \<noteq> {}" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
135 |
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 Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
136 |
shows "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
137 |
proof(cases "\<exists>x \<in> M. x \<in> iterates_above (lub M')") |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
138 |
case True |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
139 |
then obtain x where x: "x \<in> M" "x \<in> iterates_above (lub M')" by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
140 |
have lub_M': "lub M' \<in> Field leq" using M' by(rule lub_in_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
141 |
have "lub M \<in> iterates_above (lub M')" using M |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
142 |
proof(rule iterates_above_lub) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
143 |
fix y |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
144 |
assume y: "y \<in> M" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
145 |
from comp[OF y] show "\<exists>z\<in>M. (y, z) \<in> leq \<and> z \<in> iterates_above (lub M')" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
146 |
proof |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
147 |
assume "y \<in> iterates_above (lub M')" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
148 |
from this iterates_above_Field[OF this] y lub_M' show ?thesis by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
149 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
150 |
assume "lub M' \<in> iterates_above y" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
151 |
hence "(y, lub M') \<in> leq" using Chains_FieldD[OF M(1) y] by(rule iterates_above_ge) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
152 |
also have "(lub M', x) \<in> leq" using x(2) lub_M' by(rule iterates_above_ge) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
153 |
finally show ?thesis using x by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
154 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
155 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
156 |
thus ?thesis .. |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
157 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
158 |
case False |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
159 |
have "(lub M, lub M') \<in> leq" using M |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
160 |
proof(rule lub_least) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
161 |
fix x |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
162 |
assume x: "x \<in> M" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
163 |
from comp[OF x] x False have "lub M' \<in> iterates_above x" by auto |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
164 |
moreover from M(1) x have "x \<in> Field leq" by(rule Chains_FieldD) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
165 |
ultimately show "(x, lub M') \<in> leq" by(rule iterates_above_ge) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
166 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
167 |
thus ?thesis .. |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
168 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
169 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
170 |
lemma iterates_above_triangle: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
171 |
assumes x: "x \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
172 |
and y: "y \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
173 |
and a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
174 |
shows "x \<in> iterates_above y \<or> y \<in> iterates_above x" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
175 |
using x y |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
176 |
proof(induction arbitrary: y) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
177 |
case base then show ?case by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
178 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
179 |
case (step x) thus ?case using a |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
180 |
by(auto dest: iterates_above_successor intro: iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
181 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
182 |
case x: (Sup M) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
183 |
hence lub: "lub M \<in> iterates_above a" by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
184 |
from \<open>y \<in> iterates_above a\<close> show ?case |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
185 |
proof(induction) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
186 |
case base show ?case using lub by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
187 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
188 |
case (step y) thus ?case using a |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
189 |
by(auto dest: iterates_above_successor intro: iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
190 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
191 |
case y: (Sup M') |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
192 |
hence lub': "lub M' \<in> iterates_above a" by blast |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
193 |
have *: "x \<in> iterates_above (lub M') \<or> lub M' \<in> iterates_above x" if "x \<in> M" for x |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
194 |
using that lub' by(rule x.IH) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
195 |
with x(1-2) y(1-2) have "(lub M, lub M') \<in> leq \<or> lub M \<in> iterates_above (lub M')" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
196 |
by(rule iterates_above_Sup_aux) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
197 |
moreover from y(1-2) x(1-2) have "(lub M', lub M) \<in> leq \<or> lub M' \<in> iterates_above (lub M)" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
198 |
by(rule iterates_above_Sup_aux)(blast dest: y.IH) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
199 |
ultimately show ?case by(auto 4 3 dest: leq_antisym) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
200 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
201 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
202 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
203 |
lemma chain_iterates_above: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
204 |
assumes a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
205 |
shows "iterates_above a \<in> Chains leq" (is "?C \<in> _") |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
206 |
proof (rule ChainsI) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
207 |
fix x y |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
208 |
assume "x \<in> ?C" "y \<in> ?C" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
209 |
hence "x \<in> iterates_above y \<or> y \<in> iterates_above x" using a by(rule iterates_above_triangle) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
210 |
moreover from \<open>x \<in> ?C\<close> a have "x \<in> Field leq" by(rule iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
211 |
moreover from \<open>y \<in> ?C\<close> a have "y \<in> Field leq" by(rule iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
212 |
ultimately show "(x, y) \<in> leq \<or> (y, x) \<in> leq" by(auto dest: iterates_above_ge) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
213 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
214 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
215 |
lemma fixp_iterates_above: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
216 |
unfolding fixp_above_def by(rule iterates_above.Sup)(blast intro: chain_iterates_above)+ |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
217 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
218 |
lemma |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
219 |
assumes b: "b \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
220 |
and fb: "f b = b" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
221 |
and x: "x \<in> iterates_above a" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
222 |
and a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
223 |
shows "b \<in> iterates_above x" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
224 |
using x |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
225 |
proof(induction) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
226 |
case base show ?case using b by simp |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
227 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
228 |
case (step x) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
229 |
from step.hyps a have "x \<in> Field leq" by(rule iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
230 |
from iterates_above_successor[OF step.IH this] fb |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
231 |
show ?case by(auto) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
232 |
next |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
233 |
case (Sup M) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
234 |
oops |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
235 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
236 |
lemma fixp_above_Field: "a \<in> Field leq \<Longrightarrow> fixp_above a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
237 |
using fixp_iterates_above by(rule iterates_above_Field) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
238 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
239 |
lemma fixp_above_unfold: |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
240 |
assumes a: "a \<in> Field leq" |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
241 |
shows "fixp_above a = f (fixp_above a)" (is "?a = f ?a") |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
242 |
proof(rule leq_antisym) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
243 |
show "(?a, f ?a) \<in> leq" using fixp_above_Field[OF a] by(rule increasing) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
244 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
245 |
have "f ?a \<in> iterates_above a" using fixp_iterates_above[OF a] by(rule iterates_above.step) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
246 |
with chain_iterates_above[OF a] show "(f ?a, ?a) \<in> leq" unfolding fixp_above_def by(rule lub_upper) |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
247 |
qed |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
248 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
249 |
end |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
250 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
251 |
end |
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
252 |
|
507b39df1a57
add formalisation of Bourbaki-Witt fixpoint theorem
Andreas Lochbihler
parents:
diff
changeset
|
253 |
end |