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