# HG changeset patch
# User Andreas Lochbihler
# Date 1469797251 -7200
# Node ID eca71be9c94874ab9abfef65a39de4bfa204a8b7
# Parent  3e3097ac37d1e601bc25dd1674586402a4b6df39# Parent  0bcd79da075b0e2ffe65a1a47fee095cedc6ff62
merged

diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -37,9 +37,6 @@
 lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
   unfolding underS_def Field_def by auto
 
-lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
-  unfolding Field_def by auto
-
 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
   unfolding bij_betw_def by auto
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -36,6 +36,10 @@
 lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
 unfolding refl_on_def Field_def by auto
 
+lemma linear_order_on_Restr:
+  "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))"
+by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)
+
 lemma antisym_Restr:
 "antisym r \<Longrightarrow> antisym(Restr r A)"
 unfolding antisym_def Field_def by auto
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -602,6 +602,33 @@
   then show ?case by simp
 qed
 
+lemma finite_subset_induct' [consumes 2, case_names empty insert]:
+  assumes "finite F" and "F \<subseteq> A"
+  and empty: "P {}"
+  and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
+  shows "P F"
+proof -
+  from \<open>finite F\<close>
+  have "F \<subseteq> A \<Longrightarrow> ?thesis"
+  proof induct
+    show "P {}" by fact
+  next
+    fix x F
+    assume "finite F" and "x \<notin> F" and
+      P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
+    show "P (insert x F)"
+    proof (rule insert)
+      from i show "x \<in> A" by blast
+      from i have "F \<subseteq> A" by blast
+      with P show "P F" .
+      show "finite F" by fact
+      show "x \<notin> F" by fact
+      show "F \<subseteq> A" by fact
+    qed
+  qed
+  with \<open>F \<subseteq> A\<close> show ?thesis by blast
+qed
+
 
 subsection \<open>Class \<open>finite\<close>\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Fun.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -666,6 +666,12 @@
 lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
   by (simp add:override_on_def)
 
+lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
+unfolding override_on_def by (simp add: fun_eq_iff)
+
+lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
+unfolding override_on_def by (simp add: fun_eq_iff)
+
 
 subsection \<open>\<open>swap\<close>\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -602,6 +602,21 @@
   finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
 qed
 
+lemma setsum_mono_inv:
+  fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add"
+  assumes eq: "setsum f I = setsum g I"
+  assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i"
+  assumes i: "i \<in> I"
+  assumes I: "finite I"
+  shows "f i = g i"
+proof(rule ccontr)
+  assume "f i \<noteq> g i"
+  with le[OF i] have "f i < g i" by simp
+  hence "\<exists>i\<in>I. f i < g i" using i ..
+  from setsum_strict_mono_ex1[OF I _ this] le have "setsum f I < setsum g I" by blast
+  with eq show False by simp
+qed
+
 lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
 proof (cases "finite A")
   case True thus ?thesis by (induct set: finite) auto
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -989,6 +989,7 @@
 lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
   by blast
 lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
+lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
 
 lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Inductive.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -50,6 +50,9 @@
 lemma lfp_const: "lfp (\<lambda>x. t) = t"
   by (rule lfp_unfold) (simp add: mono_def)
 
+lemma lfp_eqI: "\<lbrakk> mono F; F x = x; \<And>z. F z = z \<Longrightarrow> x \<le> z \<rbrakk> \<Longrightarrow> lfp F = x"
+by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric])
+
 
 subsection \<open>General induction rules for least fixed points\<close>
 
@@ -140,6 +143,12 @@
 lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
 
+lemma gfp_const: "gfp (\<lambda>x. t) = t"
+by (rule gfp_unfold) (simp add: mono_def)
+
+lemma gfp_eqI: "\<lbrakk> mono F; F x = x; \<And>z. F z = z \<Longrightarrow> z \<le> x \<rbrakk> \<Longrightarrow> gfp F = x"
+by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
+
 
 subsection \<open>Coinduction rules for greatest fixed points\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -8,7 +8,7 @@
 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
 
 theory Bourbaki_Witt_Fixpoint
-  imports Main
+  imports While_Combinator
 begin
 
 lemma ChainsI [intro?]:
@@ -18,8 +18,8 @@
 lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
 by(auto simp add: Chains_def)
 
-lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
-  unfolding Field_def by auto
+lemma in_ChainsD: "\<lbrakk> M \<in> Chains r; x \<in> M; y \<in> M \<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r"
+unfolding Chains_def by fast
 
 lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
 by(auto simp add: Chains_def intro: FieldI1 FieldI2)
@@ -245,7 +245,7 @@
 
 end
 
-lemma fixp_induct [case_names adm base step]:
+lemma fixp_above_induct [case_names adm base step]:
   assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
   and base: "P a"
   and step: "\<And>x. P x \<Longrightarrow> P (f x)"
@@ -264,4 +264,142 @@
 
 end
 
+subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
+
+context bourbaki_witt_fixpoint begin
+
+lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}.\<close>
+  assumes "M \<in> Chains leq"
+  and "M \<noteq> {}"
+  and "finite M"
+  shows "lub M \<in> M"
+using assms(3,1,2)
+proof induction
+  case empty thus ?case by simp
+next
+  case (insert x M)
+  note chain = \<open>insert x M \<in> Chains leq\<close>
+  show ?case
+  proof(cases "M = {}")
+    case True thus ?thesis
+      using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
+  next
+    case False
+    from chain have chain': "M \<in> Chains leq"
+      using in_Chains_subset subset_insertI by blast
+    hence "lub M \<in> M" using False by(rule insert.IH)
+    show ?thesis
+    proof(cases "(x, lub M) \<in> leq")
+      case True
+      have "(lub (insert x M), lub M) \<in> leq" using chain
+        by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
+      with False have "lub (insert x M) = lub M"
+        using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
+      with \<open>lub M \<in> M\<close> show ?thesis by simp
+    next
+      case False
+      with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
+      have "lub (insert x M) = x"
+        by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
+      thus ?thesis by simp
+    qed
+  qed
+qed
+
+lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
+using iterates_above.base iterates_above.step by (induct k) simp_all
+
+lemma chfin_iterates_above_fun_pow:
+  assumes "x \<in> iterates_above a"
+  assumes "\<forall>M \<in> Chains leq. finite M"
+  shows "\<exists>j. x = (f ^^ j) a"
+using assms(1)
+proof induct
+  case base then show ?case by (simp add: exI[where x=0])
+next
+  case (step x) then obtain j where "x = (f ^^ j) a" by blast
+  with step(1) show ?case by (simp add: exI[where x="Suc j"])
+next
+  case (Sup M) with in_Chains_finite assms(2) show ?case by blast
+qed
+
+lemma Chain_finite_iterates_above_fun_pow_iff:
+  assumes "\<forall>M \<in> Chains leq. finite M"
+  shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
+using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
+
+lemma fixp_above_Kleene_iter_ex:
+  assumes "(\<forall>M \<in> Chains leq. finite M)"
+  obtains k where "fixp_above a = (f ^^ k) a"
+using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
+
+context fixes a assumes a: "a \<in> Field leq" begin
+
+lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
+using a by (induct k) (auto intro: increasing FieldI2)
+
+lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
+proof(induct k)
+  case (Suc k)
+  with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
+  show ?case by simp (metis less_antisym)
+qed simp
+
+lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
+using funpow_Field_leq
+by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
+
+lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
+using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
+
+lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
+using chain_iterates_above[OF a] fun_pow_iterates_above
+by (blast intro: ChainsI dest: in_ChainsD)
+
+lemma fixp_above_Kleene_iter:
+  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
+  assumes "(f ^^ Suc k) a = (f ^^ k) a"
+  shows "fixp_above a = (f ^^ k) a"
+proof(rule leq_antisym)
+  show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
+    by(auto simp add: fixp_above_def chain_iterates_above Chain_finite_iterates_above_fun_pow_iff funpow_stability[OF assms(2)] intro!: lub_least intro: iterates_above.base)
+  show "((f ^^ k) a, fixp_above a) \<in> leq" using a
+    by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
+qed
+
+context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
+
+lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
+apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
+apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
+apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
+done
+
+lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
+by(rule wf_rel_while_option_Some[OF Chain_finite_wf, where P="\<lambda>A. (\<exists>k. A = (f ^^ k) a) \<and> (A, f A) \<in> leq" and s="a"])
+  (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
+
+lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
+proof -
+  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
+    using while_option_finite_increasing by blast
+  with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
+  show ?thesis by fastforce
+qed
+
+lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
+unfolding while_def by (rule fixp_above_the_while_option)
+
 end
+
+end
+
+end
+
+lemma bourbaki_witt_fixpoint_complete_latticeI:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "\<And>x. x \<le> f x"
+  shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
+by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
+
+end
\ No newline at end of file
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Library/Product_Order.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Pointwise order on product types\<close>
 
 theory Product_Order
-imports Product_plus Conditionally_Complete_Lattices
+imports Product_plus
 begin
 
 subsection \<open>Pointwise ordering\<close>
@@ -243,5 +243,74 @@
     by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
 qed
 
+subsection \<open>Bekic's Theorem\<close>
+text \<open>
+  Simultaneous fixed points over pairs can be written in terms of separate fixed points.
+  Transliterated from HOLCF.Fix by Peter Gammie
+\<close>
+
+lemma lfp_prod:
+  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
+  assumes "mono F"
+  shows "lfp F = (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))),
+                 (lfp (\<lambda>y. snd (F (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))), y)))))"
+  (is "lfp F = (?x, ?y)")
+proof(rule lfp_eqI[OF assms])
+  have 1: "fst (F (?x, ?y)) = ?x"
+    by (rule trans [symmetric, OF lfp_unfold])
+       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
+  have 2: "snd (F (?x, ?y)) = ?y"
+    by (rule trans [symmetric, OF lfp_unfold])
+       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
+  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
+next
+  fix z assume F_z: "F z = z"
+  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
+  from F_z z have F_x: "fst (F (x, y)) = x" by simp
+  from F_z z have F_y: "snd (F (x, y)) = y" by simp
+  let ?y1 = "lfp (\<lambda>y. snd (F (x, y)))"
+  have "?y1 \<le> y" by (rule lfp_lowerbound, simp add: F_y)
+  hence "fst (F (x, ?y1)) \<le> fst (F (x, y))"
+    by (simp add: assms fst_mono monoD)
+  hence "fst (F (x, ?y1)) \<le> x" using F_x by simp
+  hence 1: "?x \<le> x" by (simp add: lfp_lowerbound)
+  hence "snd (F (?x, y)) \<le> snd (F (x, y))"
+    by (simp add: assms snd_mono monoD)
+  hence "snd (F (?x, y)) \<le> y" using F_y by simp
+  hence 2: "?y \<le> y" by (simp add: lfp_lowerbound)
+  show "(?x, ?y) \<le> z" using z 1 2 by simp
+qed
+
+lemma gfp_prod:
+  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
+  assumes "mono F"
+  shows "gfp F = (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))),
+                 (gfp (\<lambda>y. snd (F (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))), y)))))"
+  (is "gfp F = (?x, ?y)")
+proof(rule gfp_eqI[OF assms])
+  have 1: "fst (F (?x, ?y)) = ?x"
+    by (rule trans [symmetric, OF gfp_unfold])
+       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
+  have 2: "snd (F (?x, ?y)) = ?y"
+    by (rule trans [symmetric, OF gfp_unfold])
+       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
+  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
+next
+  fix z assume F_z: "F z = z"
+  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
+  from F_z z have F_x: "fst (F (x, y)) = x" by simp
+  from F_z z have F_y: "snd (F (x, y)) = y" by simp
+  let ?y1 = "gfp (\<lambda>y. snd (F (x, y)))"
+  have "y \<le> ?y1" by (rule gfp_upperbound, simp add: F_y)
+  hence "fst (F (x, y)) \<le> fst (F (x, ?y1))"
+    by (simp add: assms fst_mono monoD)
+  hence "x \<le> fst (F (x, ?y1))" using F_x by simp
+  hence 1: "x \<le> ?x" by (simp add: gfp_upperbound)
+  hence "snd (F (x, y)) \<le> snd (F (?x, y))"
+    by (simp add: assms snd_mono monoD)
+  hence "y \<le> snd (F (?x, y))" using F_y by simp
+  hence 2: "y \<le> ?y" by (simp add: gfp_upperbound)
+  show "z \<le> (?x, ?y)" using z 1 2 by simp
+qed
+
 end
-
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -300,6 +300,65 @@
   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
 unfolding while_def using assms by (rule lfp_the_while_option) blast
 
+lemma wf_finite_less:
+  assumes "finite (C :: 'a::order set)"
+  shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
+by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
+   (fastforce simp: less_eq assms intro: psubset_card_mono)
+
+lemma wf_finite_greater:
+  assumes "finite (C :: 'a::order set)"
+  shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
+by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
+   (fastforce simp: less_eq assms intro: psubset_card_mono)
+
+lemma while_option_finite_increasing_Some:
+  fixes f :: "'a::order \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
+  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
+by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
+   (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])
+
+lemma lfp_the_while_option_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "lfp f = the (while_option (\<lambda>A. f A \<noteq> A) f bot)"
+proof -
+  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
+    using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
+  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
+  show ?thesis by auto
+qed
+
+lemma lfp_while_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
+unfolding while_def using assms by (rule lfp_the_while_option_lattice)
+
+lemma while_option_finite_decreasing_Some:
+  fixes f :: "'a::order \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
+  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
+by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
+   (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])
+
+lemma gfp_the_while_option_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
+proof -
+  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
+    using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
+  with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
+  show ?thesis by auto
+qed
+
+lemma gfp_while_lattice:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f" and "finite (UNIV :: 'a set)"
+  shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
+unfolding while_def using assms by (rule gfp_the_while_option_lattice)
 
 text\<open>Computing the reflexive, transitive closure by iterating a successor
 function. Stops when an element is found that dos not satisfy the test.
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/List.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -4443,6 +4443,23 @@
   qed
 qed
 
+lemma sublists_refl: "xs \<in> set (sublists xs)"
+by (induct xs) (simp_all add: Let_def)
+
+lemma subset_sublists: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (sublists xs)"
+unfolding sublists_powset by simp
+
+lemma Cons_in_sublistsD:
+  "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
+by (induct xs) (auto simp: Let_def)
+
+lemma sublists_distinctD: "\<lbrakk> ys \<in> set (sublists xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
+proof(induct xs arbitrary: ys)
+  case (Cons x xs ys)
+  then show ?case
+    by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI sublists_powset)
+qed simp
+
 
 subsubsection \<open>@{const splice}\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -1336,10 +1336,32 @@
   by (induct n) simp_all
 
 lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
-  for f :: "'a \<Rightarrow> ('a::lattice)"
+  for f :: "'a \<Rightarrow> ('a::order)"
   by (induct n arbitrary: A B)
      (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
 
+lemma funpow_mono2:
+  assumes "mono f"
+  assumes "i \<le> j"
+  assumes "x \<le> y"
+  assumes "x \<le> f x"
+  shows "(f ^^ i) x \<le> (f ^^ j) y"
+using assms(2,3)
+proof(induct j arbitrary: y)
+  case (Suc j)
+  show ?case
+  proof(cases "i = Suc j")
+    case True
+    with assms(1) Suc show ?thesis
+      by (simp del: funpow.simps add: funpow_simps_right monoD funpow_mono)
+  next
+    case False
+    with assms(1,4) Suc show ?thesis
+      by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le)
+         (simp add: Suc.hyps monoD order_subst1)
+  qed
+qed simp
+
 
 subsection \<open>Kleene iteration\<close>
 
@@ -1406,6 +1428,30 @@
     by (intro gfp_upperbound) (simp del: funpow.simps)
 qed
 
+lemma Kleene_iter_gpfp:
+  assumes "mono f"
+  and "p \<le> f p"
+  shows "p \<le> (f ^^ k) (top::'a::order_top)"
+proof(induction k)
+  case 0 show ?case by simp
+next
+  case Suc
+  from monoD[OF assms(1) Suc] assms(2)
+  show ?case by simp
+qed
+
+lemma gfp_Kleene_iter:
+  assumes "mono f"
+  and "(f ^^ Suc k) top = (f ^^ k) top"
+  shows "gfp f = (f ^^ k) top" (is "?lhs = ?rhs")
+proof(rule antisym)
+  have "?rhs \<le> f ?rhs" using assms(2) by simp
+  then show "?rhs \<le> ?lhs" by(rule gfp_upperbound)
+
+  show "?lhs \<le> ?rhs"
+    using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
+qed
+
 
 subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Order_Relation.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -55,6 +55,21 @@
   "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
 by(simp add: order_on_defs trans_diff_Id)
 
+lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
+unfolding order_on_defs by simp
+
+lemma linear_order_on_acyclic:
+  assumes "linear_order_on A r"
+  shows "acyclic (r - Id)"
+using strict_linear_order_on_diff_Id[OF assms] 
+by(auto simp add: acyclic_irrefl strict_linear_order_on_def)
+
+lemma linear_order_on_well_order_on:
+  assumes "finite r"
+  shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
+unfolding well_order_on_def
+using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
+
 
 subsection\<open>Orders on the field\<close>
 
@@ -306,6 +321,22 @@
   order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
 qed
 
+lemma finite_Linear_order_induct[consumes 3, case_names step]:
+  assumes "Linear_order r"
+  and "x \<in> Field r"
+  and "finite r"
+  and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x"
+  shows "P x"
+using assms(2)
+proof(induct rule: wf_induct[of "r\<inverse> - Id"])
+  from assms(1,3) show "wf (r\<inverse> - Id)"
+    using linear_order_on_well_order_on linear_order_on_converse
+    unfolding well_order_on_def by blast
+next
+  case (2 x) then show ?case
+    by - (rule step; auto simp: aboveS_def intro: FieldI2)
+qed
+
 
 subsection \<open>Variations on Well-Founded Relations\<close>
 
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Partial_Function.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -47,6 +47,11 @@
   qed
 qed
 
+lemma (in ccpo) admissible_chfin:
+  "(\<forall>S. Complete_Partial_Order.chain op \<le> S \<longrightarrow> finite S)
+  \<Longrightarrow> ccpo.admissible Sup op \<le> P"
+using in_chain_finite by (blast intro: ccpo.admissibleI)
+
 subsection \<open>Axiomatic setup\<close>
 
 text \<open>This techical locale constains the requirements for function
diff -r 3e3097ac37d1 -r eca71be9c948 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Relation.thy	Fri Jul 29 15:00:51 2016 +0200
@@ -206,6 +206,9 @@
 lemma refl_on_empty [simp]: "refl_on {} {}"
   by (simp add: refl_on_def)
 
+lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
+by (blast intro: refl_onI)
+
 lemma refl_on_def' [nitpick_unfold, code]:
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
@@ -335,6 +338,9 @@
 lemma antisymP_equality [simp]: "antisymP op ="
   by (auto intro: antisymI)
 
+lemma antisym_singleton [simp]: "antisym {x}"
+by (blast intro: antisymI)
+
 
 subsubsection \<open>Transitivity\<close>
 
@@ -393,17 +399,34 @@
 lemma transp_equality [simp]: "transp op ="
   by (auto intro: transpI)
 
+lemma trans_empty [simp]: "trans {}"
+by (blast intro: transI)
+
+lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
+using trans_empty[to_pred] by(simp add: bot_fun_def)
+
+lemma trans_singleton [simp]: "trans {(a, a)}"
+by (blast intro: transI)
+
+lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
+by(simp add: transp_def)
 
 subsubsection \<open>Totality\<close>
 
 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   where "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)"
 
+lemma total_onI [intro?]:
+  "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r"
+unfolding total_on_def by blast
+
 abbreviation "total \<equiv> total_on UNIV"
 
 lemma total_on_empty [simp]: "total_on {} r"
   by (simp add: total_on_def)
 
+lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
+unfolding total_on_def by blast
 
 subsubsection \<open>Single valued relations\<close>
 
@@ -776,6 +799,12 @@
 definition Field :: "'a rel \<Rightarrow> 'a set"
   where "Field r = Domain r \<union> Range r"
 
+lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
+unfolding Field_def by blast
+
+lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
+  unfolding Field_def by auto
+
 lemma Domain_fst [code]: "Domain r = fst ` r"
   by force
 
@@ -902,6 +931,9 @@
 lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}"
   by blast
 
+lemma Field_square [simp]: "Field (x \<times> x) = x"
+unfolding Field_def by blast
+
 
 subsubsection \<open>Image of a set under a relation\<close>