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