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