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