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
```