src/HOL/Complete_Partial_Order.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 63979 95c3ae4baba8 child 67399 eab6ce8368fa permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
```     1 (*  Title:      HOL/Complete_Partial_Order.thy
```
```     2     Author:     Brian Huffman, Portland State University
```
```     3     Author:     Alexander Krauss, TU Muenchen
```
```     4 *)
```
```     5
```
```     6 section \<open>Chain-complete partial orders and their fixpoints\<close>
```
```     7
```
```     8 theory Complete_Partial_Order
```
```     9   imports Product_Type
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Monotone functions\<close>
```
```    13
```
```    14 text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close>
```
```    15
```
```    16 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
```
```    17   where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
```
```    18
```
```    19 lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
```
```    20   unfolding monotone_def by iprover
```
```    21
```
```    22 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
```
```    23   unfolding monotone_def by iprover
```
```    24
```
```    25
```
```    26 subsection \<open>Chains\<close>
```
```    27
```
```    28 text \<open>
```
```    29   A chain is a totally-ordered set. Chains are parameterized over
```
```    30   the order for maximal flexibility, since type classes are not enough.
```
```    31 \<close>
```
```    32
```
```    33 definition chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
```
```    34   where "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)"
```
```    35
```
```    36 lemma chainI:
```
```    37   assumes "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> ord x y \<or> ord y x"
```
```    38   shows "chain ord S"
```
```    39   using assms unfolding chain_def by fast
```
```    40
```
```    41 lemma chainD:
```
```    42   assumes "chain ord S" and "x \<in> S" and "y \<in> S"
```
```    43   shows "ord x y \<or> ord y x"
```
```    44   using assms unfolding chain_def by fast
```
```    45
```
```    46 lemma chainE:
```
```    47   assumes "chain ord S" and "x \<in> S" and "y \<in> S"
```
```    48   obtains "ord x y" | "ord y x"
```
```    49   using assms unfolding chain_def by fast
```
```    50
```
```    51 lemma chain_empty: "chain ord {}"
```
```    52   by (simp add: chain_def)
```
```    53
```
```    54 lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
```
```    55   by (auto simp add: chain_def)
```
```    56
```
```    57 lemma chain_subset: "chain ord A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> chain ord B"
```
```    58   by (rule chainI) (blast dest: chainD)
```
```    59
```
```    60 lemma chain_imageI:
```
```    61   assumes chain: "chain le_a Y"
```
```    62     and mono: "\<And>x y. x \<in> Y \<Longrightarrow> y \<in> Y \<Longrightarrow> le_a x y \<Longrightarrow> le_b (f x) (f y)"
```
```    63   shows "chain le_b (f ` Y)"
```
```    64   by (blast intro: chainI dest: chainD[OF chain] mono)
```
```    65
```
```    66
```
```    67 subsection \<open>Chain-complete partial orders\<close>
```
```    68
```
```    69 text \<open>
```
```    70   A \<open>ccpo\<close> has a least upper bound for any chain.  In particular, the
```
```    71   empty set is a chain, so every \<open>ccpo\<close> must have a bottom element.
```
```    72 \<close>
```
```    73
```
```    74 class ccpo = order + Sup +
```
```    75   assumes ccpo_Sup_upper: "chain (op \<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A"
```
```    76   assumes ccpo_Sup_least: "chain (op \<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
```
```    77 begin
```
```    78
```
```    79 lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
```
```    80   by (rule chainI) simp
```
```    81
```
```    82 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
```
```    83   by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
```
```    84
```
```    85
```
```    86 subsection \<open>Transfinite iteration of a function\<close>
```
```    87
```
```    88 context notes [[inductive_internals]]
```
```    89 begin
```
```    90
```
```    91 inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
```
```    92   for f :: "'a \<Rightarrow> 'a"
```
```    93   where
```
```    94     step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
```
```    95   | Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
```
```    96
```
```    97 end
```
```    98
```
```    99 lemma iterates_le_f: "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
```
```   100   by (induct x rule: iterates.induct)
```
```   101     (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
```
```   102
```
```   103 lemma chain_iterates:
```
```   104   assumes f: "monotone (op \<le>) (op \<le>) f"
```
```   105   shows "chain (op \<le>) (iterates f)" (is "chain _ ?C")
```
```   106 proof (rule chainI)
```
```   107   fix x y
```
```   108   assume "x \<in> ?C" "y \<in> ?C"
```
```   109   then show "x \<le> y \<or> y \<le> x"
```
```   110   proof (induct x arbitrary: y rule: iterates.induct)
```
```   111     fix x y
```
```   112     assume y: "y \<in> ?C"
```
```   113       and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x"
```
```   114     from y show "f x \<le> y \<or> y \<le> f x"
```
```   115     proof (induct y rule: iterates.induct)
```
```   116       case (step y)
```
```   117       with IH f show ?case by (auto dest: monotoneD)
```
```   118     next
```
```   119       case (Sup M)
```
```   120       then have chM: "chain (op \<le>) M"
```
```   121         and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto
```
```   122       show "f x \<le> Sup M \<or> Sup M \<le> f x"
```
```   123       proof (cases "\<exists>z\<in>M. f x \<le> z")
```
```   124         case True
```
```   125         then have "f x \<le> Sup M"
```
```   126           apply rule
```
```   127           apply (erule order_trans)
```
```   128           apply (rule ccpo_Sup_upper[OF chM])
```
```   129           apply assumption
```
```   130           done
```
```   131         then show ?thesis ..
```
```   132       next
```
```   133         case False
```
```   134         with IH' show ?thesis
```
```   135           by (auto intro: ccpo_Sup_least[OF chM])
```
```   136       qed
```
```   137     qed
```
```   138   next
```
```   139     case (Sup M y)
```
```   140     show ?case
```
```   141     proof (cases "\<exists>x\<in>M. y \<le> x")
```
```   142       case True
```
```   143       then have "y \<le> Sup M"
```
```   144         apply rule
```
```   145         apply (erule order_trans)
```
```   146         apply (rule ccpo_Sup_upper[OF Sup(1)])
```
```   147         apply assumption
```
```   148         done
```
```   149       then show ?thesis ..
```
```   150     next
```
```   151       case False with Sup
```
```   152       show ?thesis by (auto intro: ccpo_Sup_least)
```
```   153     qed
```
```   154   qed
```
```   155 qed
```
```   156
```
```   157 lemma bot_in_iterates: "Sup {} \<in> iterates f"
```
```   158   by (auto intro: iterates.Sup simp add: chain_empty)
```
```   159
```
```   160
```
```   161 subsection \<open>Fixpoint combinator\<close>
```
```   162
```
```   163 definition fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
```
```   164   where "fixp f = Sup (iterates f)"
```
```   165
```
```   166 lemma iterates_fixp:
```
```   167   assumes f: "monotone (op \<le>) (op \<le>) f"
```
```   168   shows "fixp f \<in> iterates f"
```
```   169   unfolding fixp_def
```
```   170   by (simp add: iterates.Sup chain_iterates f)
```
```   171
```
```   172 lemma fixp_unfold:
```
```   173   assumes f: "monotone (op \<le>) (op \<le>) f"
```
```   174   shows "fixp f = f (fixp f)"
```
```   175 proof (rule antisym)
```
```   176   show "fixp f \<le> f (fixp f)"
```
```   177     by (intro iterates_le_f iterates_fixp f)
```
```   178   have "f (fixp f) \<le> Sup (iterates f)"
```
```   179     by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
```
```   180   then show "f (fixp f) \<le> fixp f"
```
```   181     by (simp only: fixp_def)
```
```   182 qed
```
```   183
```
```   184 lemma fixp_lowerbound:
```
```   185   assumes f: "monotone (op \<le>) (op \<le>) f"
```
```   186     and z: "f z \<le> z"
```
```   187   shows "fixp f \<le> z"
```
```   188   unfolding fixp_def
```
```   189 proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
```
```   190   fix x
```
```   191   assume "x \<in> iterates f"
```
```   192   then show "x \<le> z"
```
```   193   proof (induct x rule: iterates.induct)
```
```   194     case (step x)
```
```   195     from f \<open>x \<le> z\<close> have "f x \<le> f z" by (rule monotoneD)
```
```   196     also note z
```
```   197     finally show "f x \<le> z" .
```
```   198   next
```
```   199     case (Sup M)
```
```   200     then show ?case
```
```   201       by (auto intro: ccpo_Sup_least)
```
```   202   qed
```
```   203 qed
```
```   204
```
```   205 end
```
```   206
```
```   207
```
```   208 subsection \<open>Fixpoint induction\<close>
```
```   209
```
```   210 setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
```
```   211
```
```   212 definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
```
```   213   where "admissible lub ord P \<longleftrightarrow> (\<forall>A. chain ord A \<longrightarrow> A \<noteq> {} \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
```
```   214
```
```   215 lemma admissibleI:
```
```   216   assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
```
```   217   shows "ccpo.admissible lub ord P"
```
```   218   using assms unfolding ccpo.admissible_def by fast
```
```   219
```
```   220 lemma admissibleD:
```
```   221   assumes "ccpo.admissible lub ord P"
```
```   222   assumes "chain ord A"
```
```   223   assumes "A \<noteq> {}"
```
```   224   assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
```
```   225   shows "P (lub A)"
```
```   226   using assms by (auto simp: ccpo.admissible_def)
```
```   227
```
```   228 setup \<open>Sign.map_naming Name_Space.parent_path\<close>
```
```   229
```
```   230 lemma (in ccpo) fixp_induct:
```
```   231   assumes adm: "ccpo.admissible Sup (op \<le>) P"
```
```   232   assumes mono: "monotone (op \<le>) (op \<le>) f"
```
```   233   assumes bot: "P (Sup {})"
```
```   234   assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
```
```   235   shows "P (fixp f)"
```
```   236   unfolding fixp_def
```
```   237   using adm chain_iterates[OF mono]
```
```   238 proof (rule ccpo.admissibleD)
```
```   239   show "iterates f \<noteq> {}"
```
```   240     using bot_in_iterates by auto
```
```   241 next
```
```   242   fix x
```
```   243   assume "x \<in> iterates f"
```
```   244   then show "P x"
```
```   245   proof (induct rule: iterates.induct)
```
```   246     case prems: (step x)
```
```   247     from this(2) show ?case by (rule step)
```
```   248   next
```
```   249     case (Sup M)
```
```   250     then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm)
```
```   251   qed
```
```   252 qed
```
```   253
```
```   254 lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
```
```   255   unfolding ccpo.admissible_def by simp
```
```   256
```
```   257 (*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
```
```   258 unfolding ccpo.admissible_def chain_def by simp
```
```   259 *)
```
```   260 lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
```
```   261   by (auto intro: ccpo.admissibleI)
```
```   262
```
```   263 lemma admissible_conj:
```
```   264   assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
```
```   265   assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
```
```   266   shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
```
```   267   using assms unfolding ccpo.admissible_def by simp
```
```   268
```
```   269 lemma admissible_all:
```
```   270   assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
```
```   271   shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
```
```   272   using assms unfolding ccpo.admissible_def by fast
```
```   273
```
```   274 lemma admissible_ball:
```
```   275   assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
```
```   276   shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
```
```   277   using assms unfolding ccpo.admissible_def by fast
```
```   278
```
```   279 lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
```
```   280   unfolding chain_def by fast
```
```   281
```
```   282 context ccpo
```
```   283 begin
```
```   284
```
```   285 lemma admissible_disj:
```
```   286   fixes P Q :: "'a \<Rightarrow> bool"
```
```   287   assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
```
```   288   assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
```
```   289   shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
```
```   290 proof (rule ccpo.admissibleI)
```
```   291   fix A :: "'a set"
```
```   292   assume chain: "chain (op \<le>) A"
```
```   293   assume A: "A \<noteq> {}" and P_Q: "\<forall>x\<in>A. P x \<or> Q x"
```
```   294   have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
```
```   295     (is "?P \<or> ?Q" is "?P1 \<and> ?P2 \<or> _")
```
```   296   proof (rule disjCI)
```
```   297     assume "\<not> ?Q"
```
```   298     then consider "\<forall>x\<in>A. \<not> Q x" | a where "a \<in> A" "\<forall>y\<in>A. a \<le> y \<longrightarrow> \<not> Q y"
```
```   299       by blast
```
```   300     then show ?P
```
```   301     proof cases
```
```   302       case 1
```
```   303       with P_Q have "\<forall>x\<in>A. P x" by blast
```
```   304       with A show ?P by blast
```
```   305     next
```
```   306       case 2
```
```   307       note a = \<open>a \<in> A\<close>
```
```   308       show ?P
```
```   309       proof
```
```   310         from P_Q 2 have *: "\<forall>y\<in>A. a \<le> y \<longrightarrow> P y" by blast
```
```   311         with a have "P a" by blast
```
```   312         with a show ?P1 by blast
```
```   313         show ?P2
```
```   314         proof
```
```   315           fix x
```
```   316           assume x: "x \<in> A"
```
```   317           with chain a show "\<exists>y\<in>A. x \<le> y \<and> P y"
```
```   318           proof (rule chainE)
```
```   319             assume le: "a \<le> x"
```
```   320             with * a x have "P x" by blast
```
```   321             with x le show ?thesis by blast
```
```   322           next
```
```   323             assume "a \<ge> x"
```
```   324             with a \<open>P a\<close> show ?thesis by blast
```
```   325           qed
```
```   326         qed
```
```   327       qed
```
```   328     qed
```
```   329   qed
```
```   330   moreover
```
```   331   have "Sup A = Sup {x \<in> A. P x}" if "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y" for P
```
```   332   proof (rule antisym)
```
```   333     have chain_P: "chain (op \<le>) {x \<in> A. P x}"
```
```   334       by (rule chain_compr [OF chain])
```
```   335     show "Sup A \<le> Sup {x \<in> A. P x}"
```
```   336       apply (rule ccpo_Sup_least [OF chain])
```
```   337       apply (drule that [rule_format])
```
```   338       apply clarify
```
```   339       apply (erule order_trans)
```
```   340       apply (simp add: ccpo_Sup_upper [OF chain_P])
```
```   341       done
```
```   342     show "Sup {x \<in> A. P x} \<le> Sup A"
```
```   343       apply (rule ccpo_Sup_least [OF chain_P])
```
```   344       apply clarify
```
```   345       apply (simp add: ccpo_Sup_upper [OF chain])
```
```   346       done
```
```   347   qed
```
```   348   ultimately
```
```   349   consider "\<exists>x. x \<in> A \<and> P x" "Sup A = Sup {x \<in> A. P x}"
```
```   350     | "\<exists>x. x \<in> A \<and> Q x" "Sup A = Sup {x \<in> A. Q x}"
```
```   351     by blast
```
```   352   then show "P (Sup A) \<or> Q (Sup A)"
```
```   353     apply cases
```
```   354      apply simp_all
```
```   355      apply (rule disjI1)
```
```   356      apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp)
```
```   357     apply (rule disjI2)
```
```   358     apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp)
```
```   359     done
```
```   360 qed
```
```   361
```
```   362 end
```
```   363
```
```   364 instance complete_lattice \<subseteq> ccpo
```
```   365   by standard (fast intro: Sup_upper Sup_least)+
```
```   366
```
```   367 lemma lfp_eq_fixp:
```
```   368   assumes mono: "mono f"
```
```   369   shows "lfp f = fixp f"
```
```   370 proof (rule antisym)
```
```   371   from mono have f': "monotone (op \<le>) (op \<le>) f"
```
```   372     unfolding mono_def monotone_def .
```
```   373   show "lfp f \<le> fixp f"
```
```   374     by (rule lfp_lowerbound, subst fixp_unfold [OF f'], rule order_refl)
```
```   375   show "fixp f \<le> lfp f"
```
```   376     by (rule fixp_lowerbound [OF f']) (simp add: lfp_fixpoint [OF mono])
```
```   377 qed
```
```   378
```
```   379 hide_const (open) iterates fixp
```
```   380
```
```   381 end
```