add lemmas contributed by Peter Gammie
authorAndreas Lochbihler
Fri Jul 29 09:49:23 2016 +0200 (2016-07-29)
changeset 63561fba08009ff3e
parent 63559 113cee845044
child 63562 6f7a9d48a828
add lemmas contributed by Peter Gammie
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/BNF_Wellorder_Constructions.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Groups_Big.thy
src/HOL/HOL.thy
src/HOL/Inductive.thy
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/While_Combinator.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Order_Relation.thy
src/HOL/Partial_Function.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Jul 28 20:39:51 2016 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Fri Jul 29 09:49:23 2016 +0200
     1.3 @@ -37,9 +37,6 @@
     1.4  lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
     1.5    unfolding underS_def Field_def by auto
     1.6  
     1.7 -lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
     1.8 -  unfolding Field_def by auto
     1.9 -
    1.10  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    1.11    unfolding bij_betw_def by auto
    1.12  
     2.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Jul 28 20:39:51 2016 +0200
     2.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri Jul 29 09:49:23 2016 +0200
     2.3 @@ -36,6 +36,10 @@
     2.4  lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)"
     2.5  unfolding refl_on_def Field_def by auto
     2.6  
     2.7 +lemma linear_order_on_Restr:
     2.8 +  "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))"
     2.9 +by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast)
    2.10 +
    2.11  lemma antisym_Restr:
    2.12  "antisym r \<Longrightarrow> antisym(Restr r A)"
    2.13  unfolding antisym_def Field_def by auto
     3.1 --- a/src/HOL/Finite_Set.thy	Thu Jul 28 20:39:51 2016 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Jul 29 09:49:23 2016 +0200
     3.3 @@ -602,6 +602,33 @@
     3.4    then show ?case by simp
     3.5  qed
     3.6  
     3.7 +lemma finite_subset_induct' [consumes 2, case_names empty insert]:
     3.8 +  assumes "finite F" and "F \<subseteq> A"
     3.9 +  and empty: "P {}"
    3.10 +  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)"
    3.11 +  shows "P F"
    3.12 +proof -
    3.13 +  from \<open>finite F\<close>
    3.14 +  have "F \<subseteq> A \<Longrightarrow> ?thesis"
    3.15 +  proof induct
    3.16 +    show "P {}" by fact
    3.17 +  next
    3.18 +    fix x F
    3.19 +    assume "finite F" and "x \<notin> F" and
    3.20 +      P: "F \<subseteq> A \<Longrightarrow> P F" and i: "insert x F \<subseteq> A"
    3.21 +    show "P (insert x F)"
    3.22 +    proof (rule insert)
    3.23 +      from i show "x \<in> A" by blast
    3.24 +      from i have "F \<subseteq> A" by blast
    3.25 +      with P show "P F" .
    3.26 +      show "finite F" by fact
    3.27 +      show "x \<notin> F" by fact
    3.28 +      show "F \<subseteq> A" by fact
    3.29 +    qed
    3.30 +  qed
    3.31 +  with \<open>F \<subseteq> A\<close> show ?thesis by blast
    3.32 +qed
    3.33 +
    3.34  
    3.35  subsection \<open>Class \<open>finite\<close>\<close>
    3.36  
     4.1 --- a/src/HOL/Fun.thy	Thu Jul 28 20:39:51 2016 +0200
     4.2 +++ b/src/HOL/Fun.thy	Fri Jul 29 09:49:23 2016 +0200
     4.3 @@ -666,6 +666,12 @@
     4.4  lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
     4.5    by (simp add:override_on_def)
     4.6  
     4.7 +lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
     4.8 +unfolding override_on_def by (simp add: fun_eq_iff)
     4.9 +
    4.10 +lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
    4.11 +unfolding override_on_def by (simp add: fun_eq_iff)
    4.12 +
    4.13  
    4.14  subsection \<open>\<open>swap\<close>\<close>
    4.15  
     5.1 --- a/src/HOL/Groups_Big.thy	Thu Jul 28 20:39:51 2016 +0200
     5.2 +++ b/src/HOL/Groups_Big.thy	Fri Jul 29 09:49:23 2016 +0200
     5.3 @@ -602,6 +602,21 @@
     5.4    finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
     5.5  qed
     5.6  
     5.7 +lemma setsum_mono_inv:
     5.8 +  fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add"
     5.9 +  assumes eq: "setsum f I = setsum g I"
    5.10 +  assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i"
    5.11 +  assumes i: "i \<in> I"
    5.12 +  assumes I: "finite I"
    5.13 +  shows "f i = g i"
    5.14 +proof(rule ccontr)
    5.15 +  assume "f i \<noteq> g i"
    5.16 +  with le[OF i] have "f i < g i" by simp
    5.17 +  hence "\<exists>i\<in>I. f i < g i" using i ..
    5.18 +  from setsum_strict_mono_ex1[OF I _ this] le have "setsum f I < setsum g I" by blast
    5.19 +  with eq show False by simp
    5.20 +qed
    5.21 +
    5.22  lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
    5.23  proof (cases "finite A")
    5.24    case True thus ?thesis by (induct set: finite) auto
     6.1 --- a/src/HOL/HOL.thy	Thu Jul 28 20:39:51 2016 +0200
     6.2 +++ b/src/HOL/HOL.thy	Fri Jul 29 09:49:23 2016 +0200
     6.3 @@ -989,6 +989,7 @@
     6.4  lemma disj_not2: "(P \<or> \<not> Q) = (Q \<longrightarrow> P)"  \<comment> \<open>changes orientation :-(\<close>
     6.5    by blast
     6.6  lemma imp_conv_disj: "(P \<longrightarrow> Q) = ((\<not> P) \<or> Q)" by blast
     6.7 +lemma disj_imp: "P \<or> Q \<longleftrightarrow> \<not> P \<longrightarrow> Q" by blast
     6.8  
     6.9  lemma iff_conv_conj_imp: "(P = Q) = ((P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P))" by iprover
    6.10  
     7.1 --- a/src/HOL/Inductive.thy	Thu Jul 28 20:39:51 2016 +0200
     7.2 +++ b/src/HOL/Inductive.thy	Fri Jul 29 09:49:23 2016 +0200
     7.3 @@ -50,6 +50,9 @@
     7.4  lemma lfp_const: "lfp (\<lambda>x. t) = t"
     7.5    by (rule lfp_unfold) (simp add: mono_def)
     7.6  
     7.7 +lemma lfp_eqI: "\<lbrakk> mono F; F x = x; \<And>z. F z = z \<Longrightarrow> x \<le> z \<rbrakk> \<Longrightarrow> lfp F = x"
     7.8 +by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric])
     7.9 +
    7.10  
    7.11  subsection \<open>General induction rules for least fixed points\<close>
    7.12  
    7.13 @@ -140,6 +143,12 @@
    7.14  lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
    7.15    by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
    7.16  
    7.17 +lemma gfp_const: "gfp (\<lambda>x. t) = t"
    7.18 +by (rule gfp_unfold) (simp add: mono_def)
    7.19 +
    7.20 +lemma gfp_eqI: "\<lbrakk> mono F; F x = x; \<And>z. F z = z \<Longrightarrow> z \<le> x \<rbrakk> \<Longrightarrow> gfp F = x"
    7.21 +by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
    7.22 +
    7.23  
    7.24  subsection \<open>Coinduction rules for greatest fixed points\<close>
    7.25  
     8.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Thu Jul 28 20:39:51 2016 +0200
     8.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 29 09:49:23 2016 +0200
     8.3 @@ -8,7 +8,7 @@
     8.4  section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
     8.5  
     8.6  theory Bourbaki_Witt_Fixpoint
     8.7 -  imports Main
     8.8 +  imports While_Combinator
     8.9  begin
    8.10  
    8.11  lemma ChainsI [intro?]:
    8.12 @@ -18,8 +18,8 @@
    8.13  lemma in_Chains_subset: "\<lbrakk> M \<in> Chains r; M' \<subseteq> M \<rbrakk> \<Longrightarrow> M' \<in> Chains r"
    8.14  by(auto simp add: Chains_def)
    8.15  
    8.16 -lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
    8.17 -  unfolding Field_def by auto
    8.18 +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"
    8.19 +unfolding Chains_def by fast
    8.20  
    8.21  lemma Chains_FieldD: "\<lbrakk> M \<in> Chains r; x \<in> M \<rbrakk> \<Longrightarrow> x \<in> Field r"
    8.22  by(auto simp add: Chains_def intro: FieldI1 FieldI2)
    8.23 @@ -245,7 +245,7 @@
    8.24  
    8.25  end
    8.26  
    8.27 -lemma fixp_induct [case_names adm base step]:
    8.28 +lemma fixp_above_induct [case_names adm base step]:
    8.29    assumes adm: "ccpo.admissible lub (\<lambda>x y. (x, y) \<in> leq) P"
    8.30    and base: "P a"
    8.31    and step: "\<And>x. P x \<Longrightarrow> P (f x)"
    8.32 @@ -264,4 +264,142 @@
    8.33  
    8.34  end
    8.35  
    8.36 +subsection \<open>Connect with the while combinator for executability on chain-finite lattices.\<close>
    8.37 +
    8.38 +context bourbaki_witt_fixpoint begin
    8.39 +
    8.40 +lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}. }\<close>
    8.41 +  assumes "M \<in> Chains leq"
    8.42 +  and "M \<noteq> {}"
    8.43 +  and "finite M"
    8.44 +  shows "lub M \<in> M"
    8.45 +using assms(3,1,2)
    8.46 +proof induction
    8.47 +  case empty thus ?case by simp
    8.48 +next
    8.49 +  case (insert x M)
    8.50 +  note chain = \<open>insert x M \<in> Chains leq\<close>
    8.51 +  show ?case
    8.52 +  proof(cases "M = {}")
    8.53 +    case True thus ?thesis
    8.54 +      using chain in_ChainsD leq_antisym lub_least lub_upper by fastforce
    8.55 +  next
    8.56 +    case False
    8.57 +    from chain have chain': "M \<in> Chains leq"
    8.58 +      using in_Chains_subset subset_insertI by blast
    8.59 +    hence "lub M \<in> M" using False by(rule insert.IH)
    8.60 +    show ?thesis
    8.61 +    proof(cases "(x, lub M) \<in> leq")
    8.62 +      case True
    8.63 +      have "(lub (insert x M), lub M) \<in> leq" using chain
    8.64 +        by (rule lub_least) (auto simp: True intro: lub_upper[OF chain'])
    8.65 +      with False have "lub (insert x M) = lub M"
    8.66 +        using lub_upper[OF chain] lub_least[OF chain'] by (blast intro: leq_antisym)
    8.67 +      with \<open>lub M \<in> M\<close> show ?thesis by simp
    8.68 +    next
    8.69 +      case False
    8.70 +      with in_ChainsD[OF chain, of x "lub M"] \<open>lub M \<in> M\<close>
    8.71 +      have "lub (insert x M) = x"
    8.72 +        by - (rule leq_antisym, (blast intro: FieldI2 chain chain' insert.prems(2) leq_refl leq_trans lub_least lub_upper)+)
    8.73 +      thus ?thesis by simp
    8.74 +    qed
    8.75 +  qed
    8.76 +qed
    8.77 +
    8.78 +lemma fun_pow_iterates_above: "(f ^^ k) a \<in> iterates_above a"
    8.79 +using iterates_above.base iterates_above.step by (induct k) simp_all
    8.80 +
    8.81 +lemma chfin_iterates_above_fun_pow:
    8.82 +  assumes "x \<in> iterates_above a"
    8.83 +  assumes "\<forall>M \<in> Chains leq. finite M"
    8.84 +  shows "\<exists>j. x = (f ^^ j) a"
    8.85 +using assms(1)
    8.86 +proof induct
    8.87 +  case base then show ?case by (simp add: exI[where x=0])
    8.88 +next
    8.89 +  case (step x) then obtain j where "x = (f ^^ j) a" by blast
    8.90 +  with step(1) show ?case by (simp add: exI[where x="Suc j"])
    8.91 +next
    8.92 +  case (Sup M) with in_Chains_finite assms(2) show ?case by blast
    8.93 +qed
    8.94 +
    8.95 +lemma Chain_finite_iterates_above_fun_pow_iff:
    8.96 +  assumes "\<forall>M \<in> Chains leq. finite M"
    8.97 +  shows "x \<in> iterates_above a \<longleftrightarrow> (\<exists>j. x = (f ^^ j) a)"
    8.98 +using chfin_iterates_above_fun_pow fun_pow_iterates_above assms by blast
    8.99 +
   8.100 +lemma fixp_above_Kleene_iter_ex:
   8.101 +  assumes "(\<forall>M \<in> Chains leq. finite M)"
   8.102 +  obtains k where "fixp_above a = (f ^^ k) a"
   8.103 +using assms by atomize_elim (simp add: chfin_iterates_above_fun_pow fixp_iterates_above)
   8.104 +
   8.105 +context fixes a assumes a: "a \<in> Field leq" begin
   8.106 +
   8.107 +lemma funpow_Field_leq: "(f ^^ k) a \<in> Field leq"
   8.108 +using a by (induct k) (auto intro: increasing FieldI2)
   8.109 +
   8.110 +lemma funpow_prefix: "j < k \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   8.111 +proof(induct k)
   8.112 +  case (Suc k)
   8.113 +  with leq_trans[OF _ increasing[OF funpow_Field_leq]] funpow_Field_leq increasing a
   8.114 +  show ?case by simp (metis less_antisym)
   8.115 +qed simp
   8.116 +
   8.117 +lemma funpow_suffix: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ (j + k)) a, (f ^^ k) a) \<in> leq"
   8.118 +using funpow_Field_leq
   8.119 +by (induct j) (simp_all del: funpow.simps add: funpow_Suc_right funpow_add leq_refl)
   8.120 +
   8.121 +lemma funpow_stability: "(f ^^ Suc k) a = (f ^^ k) a \<Longrightarrow> ((f ^^ j) a, (f ^^ k) a) \<in> leq"
   8.122 +using funpow_prefix funpow_suffix[where j="j - k" and k=k] by (cases "j < k") simp_all
   8.123 +
   8.124 +lemma funpow_in_Chains: "{(f ^^ k) a |k. True} \<in> Chains leq"
   8.125 +using chain_iterates_above[OF a] fun_pow_iterates_above
   8.126 +by (blast intro: ChainsI dest: in_ChainsD)
   8.127 +
   8.128 +lemma fixp_above_Kleene_iter:
   8.129 +  assumes "\<forall>M \<in> Chains leq. finite M" (* convenient but surely not necessary *)
   8.130 +  assumes "(f ^^ Suc k) a = (f ^^ k) a"
   8.131 +  shows "fixp_above a = (f ^^ k) a"
   8.132 +proof(rule leq_antisym)
   8.133 +  show "(fixp_above a, (f ^^ k) a) \<in> leq" using assms a
   8.134 +    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)
   8.135 +  show "((f ^^ k) a, fixp_above a) \<in> leq" using a
   8.136 +    by(auto simp add: fixp_above_def chain_iterates_above fun_pow_iterates_above intro!: lub_upper)
   8.137 +qed
   8.138 +
   8.139 +context assumes chfin: "\<forall>M \<in> Chains leq. finite M" begin
   8.140 +
   8.141 +lemma Chain_finite_wf: "wf {(f ((f ^^ k) a), (f ^^ k) a) |k. f ((f ^^ k) a) \<noteq> (f ^^ k) a}"
   8.142 +apply(rule wf_measure[where f="\<lambda>b. card {(f ^^ j) a |j. (b, (f ^^ j) a) \<in> leq}", THEN wf_subset])
   8.143 +apply(auto simp: set_eq_iff intro!: psubset_card_mono[OF finite_subset[OF _ bspec[OF chfin funpow_in_Chains]]])
   8.144 +apply(metis funpow_Field_leq increasing leq_antisym leq_trans leq_refl)+
   8.145 +done
   8.146 +
   8.147 +lemma while_option_finite_increasing: "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   8.148 +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"])
   8.149 +  (auto simp: a increasing chfin FieldI2 chfin_iterates_above_fun_pow fun_pow_iterates_above iterates_above.step intro: exI[where x=0])
   8.150 +
   8.151 +lemma fixp_above_the_while_option: "fixp_above a = the (while_option (\<lambda>A. f A \<noteq> A) f a)"
   8.152 +proof -
   8.153 +  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f a = Some P"
   8.154 +    using while_option_finite_increasing by blast
   8.155 +  with while_option_stop2[OF this] fixp_above_Kleene_iter[OF chfin]
   8.156 +  show ?thesis by fastforce
   8.157 +qed
   8.158 +
   8.159 +lemma fixp_above_conv_while: "fixp_above a = while (\<lambda>A. f A \<noteq> A) f a"
   8.160 +unfolding while_def by (rule fixp_above_the_while_option)
   8.161 +
   8.162  end
   8.163 +
   8.164 +end
   8.165 +
   8.166 +end
   8.167 +
   8.168 +lemma bourbaki_witt_fixpoint_complete_latticeI:
   8.169 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   8.170 +  assumes "\<And>x. x \<le> f x"
   8.171 +  shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
   8.172 +by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
   8.173 +
   8.174 +end
   8.175 \ No newline at end of file
     9.1 --- a/src/HOL/Library/Product_Order.thy	Thu Jul 28 20:39:51 2016 +0200
     9.2 +++ b/src/HOL/Library/Product_Order.thy	Fri Jul 29 09:49:23 2016 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  section \<open>Pointwise order on product types\<close>
     9.5  
     9.6  theory Product_Order
     9.7 -imports Product_plus Conditionally_Complete_Lattices
     9.8 +imports Product_plus
     9.9  begin
    9.10  
    9.11  subsection \<open>Pointwise ordering\<close>
    9.12 @@ -243,5 +243,74 @@
    9.13      by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    9.14  qed
    9.15  
    9.16 +subsection \<open>Bekic's Theorem\<close>
    9.17 +text \<open>
    9.18 +  Simultaneous fixed points over pairs can be written in terms of separate fixed points.
    9.19 +  Transliterated from HOLCF.Fix by Peter Gammie
    9.20 +\<close>
    9.21 +
    9.22 +lemma lfp_prod:
    9.23 +  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
    9.24 +  assumes "mono F"
    9.25 +  shows "lfp F = (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))),
    9.26 +                 (lfp (\<lambda>y. snd (F (lfp (\<lambda>x. fst (F (x, lfp (\<lambda>y. snd (F (x, y)))))), y)))))"
    9.27 +  (is "lfp F = (?x, ?y)")
    9.28 +proof(rule lfp_eqI[OF assms])
    9.29 +  have 1: "fst (F (?x, ?y)) = ?x"
    9.30 +    by (rule trans [symmetric, OF lfp_unfold])
    9.31 +       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
    9.32 +  have 2: "snd (F (?x, ?y)) = ?y"
    9.33 +    by (rule trans [symmetric, OF lfp_unfold])
    9.34 +       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono lfp_mono)+
    9.35 +  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
    9.36 +next
    9.37 +  fix z assume F_z: "F z = z"
    9.38 +  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
    9.39 +  from F_z z have F_x: "fst (F (x, y)) = x" by simp
    9.40 +  from F_z z have F_y: "snd (F (x, y)) = y" by simp
    9.41 +  let ?y1 = "lfp (\<lambda>y. snd (F (x, y)))"
    9.42 +  have "?y1 \<le> y" by (rule lfp_lowerbound, simp add: F_y)
    9.43 +  hence "fst (F (x, ?y1)) \<le> fst (F (x, y))"
    9.44 +    by (simp add: assms fst_mono monoD)
    9.45 +  hence "fst (F (x, ?y1)) \<le> x" using F_x by simp
    9.46 +  hence 1: "?x \<le> x" by (simp add: lfp_lowerbound)
    9.47 +  hence "snd (F (?x, y)) \<le> snd (F (x, y))"
    9.48 +    by (simp add: assms snd_mono monoD)
    9.49 +  hence "snd (F (?x, y)) \<le> y" using F_y by simp
    9.50 +  hence 2: "?y \<le> y" by (simp add: lfp_lowerbound)
    9.51 +  show "(?x, ?y) \<le> z" using z 1 2 by simp
    9.52 +qed
    9.53 +
    9.54 +lemma gfp_prod:
    9.55 +  fixes F :: "'a::complete_lattice \<times> 'b::complete_lattice \<Rightarrow> 'a \<times> 'b"
    9.56 +  assumes "mono F"
    9.57 +  shows "gfp F = (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))),
    9.58 +                 (gfp (\<lambda>y. snd (F (gfp (\<lambda>x. fst (F (x, gfp (\<lambda>y. snd (F (x, y)))))), y)))))"
    9.59 +  (is "gfp F = (?x, ?y)")
    9.60 +proof(rule gfp_eqI[OF assms])
    9.61 +  have 1: "fst (F (?x, ?y)) = ?x"
    9.62 +    by (rule trans [symmetric, OF gfp_unfold])
    9.63 +       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
    9.64 +  have 2: "snd (F (?x, ?y)) = ?y"
    9.65 +    by (rule trans [symmetric, OF gfp_unfold])
    9.66 +       (blast intro!: monoI monoD[OF assms(1)] fst_mono snd_mono Pair_mono gfp_mono)+
    9.67 +  from 1 2 show "F (?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff)
    9.68 +next
    9.69 +  fix z assume F_z: "F z = z"
    9.70 +  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
    9.71 +  from F_z z have F_x: "fst (F (x, y)) = x" by simp
    9.72 +  from F_z z have F_y: "snd (F (x, y)) = y" by simp
    9.73 +  let ?y1 = "gfp (\<lambda>y. snd (F (x, y)))"
    9.74 +  have "y \<le> ?y1" by (rule gfp_upperbound, simp add: F_y)
    9.75 +  hence "fst (F (x, y)) \<le> fst (F (x, ?y1))"
    9.76 +    by (simp add: assms fst_mono monoD)
    9.77 +  hence "x \<le> fst (F (x, ?y1))" using F_x by simp
    9.78 +  hence 1: "x \<le> ?x" by (simp add: gfp_upperbound)
    9.79 +  hence "snd (F (x, y)) \<le> snd (F (?x, y))"
    9.80 +    by (simp add: assms snd_mono monoD)
    9.81 +  hence "y \<le> snd (F (?x, y))" using F_y by simp
    9.82 +  hence 2: "y \<le> ?y" by (simp add: gfp_upperbound)
    9.83 +  show "z \<le> (?x, ?y)" using z 1 2 by simp
    9.84 +qed
    9.85 +
    9.86  end
    9.87 -
    10.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Jul 28 20:39:51 2016 +0200
    10.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Jul 29 09:49:23 2016 +0200
    10.3 @@ -300,6 +300,65 @@
    10.4    shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
    10.5  unfolding while_def using assms by (rule lfp_the_while_option) blast
    10.6  
    10.7 +lemma wf_finite_less:
    10.8 +  assumes "finite (C :: 'a::order set)"
    10.9 +  shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
   10.10 +by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
   10.11 +   (fastforce simp: less_eq assms intro: psubset_card_mono)
   10.12 +
   10.13 +lemma wf_finite_greater:
   10.14 +  assumes "finite (C :: 'a::order set)"
   10.15 +  shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
   10.16 +by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
   10.17 +   (fastforce simp: less_eq assms intro: psubset_card_mono)
   10.18 +
   10.19 +lemma while_option_finite_increasing_Some:
   10.20 +  fixes f :: "'a::order \<Rightarrow> 'a"
   10.21 +  assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
   10.22 +  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
   10.23 +by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
   10.24 +   (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])
   10.25 +
   10.26 +lemma lfp_the_while_option_lattice:
   10.27 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   10.28 +  assumes "mono f" and "finite (UNIV :: 'a set)"
   10.29 +  shows "lfp f = the (while_option (\<lambda>A. f A \<noteq> A) f bot)"
   10.30 +proof -
   10.31 +  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
   10.32 +    using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
   10.33 +  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
   10.34 +  show ?thesis by auto
   10.35 +qed
   10.36 +
   10.37 +lemma lfp_while_lattice:
   10.38 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   10.39 +  assumes "mono f" and "finite (UNIV :: 'a set)"
   10.40 +  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
   10.41 +unfolding while_def using assms by (rule lfp_the_while_option_lattice)
   10.42 +
   10.43 +lemma while_option_finite_decreasing_Some:
   10.44 +  fixes f :: "'a::order \<Rightarrow> 'a"
   10.45 +  assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
   10.46 +  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
   10.47 +by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
   10.48 +   (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])
   10.49 +
   10.50 +lemma gfp_the_while_option_lattice:
   10.51 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   10.52 +  assumes "mono f" and "finite (UNIV :: 'a set)"
   10.53 +  shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
   10.54 +proof -
   10.55 +  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
   10.56 +    using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
   10.57 +  with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
   10.58 +  show ?thesis by auto
   10.59 +qed
   10.60 +
   10.61 +lemma gfp_while_lattice:
   10.62 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   10.63 +  assumes "mono f" and "finite (UNIV :: 'a set)"
   10.64 +  shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
   10.65 +unfolding while_def using assms by (rule gfp_the_while_option_lattice)
   10.66  
   10.67  text\<open>Computing the reflexive, transitive closure by iterating a successor
   10.68  function. Stops when an element is found that dos not satisfy the test.
    11.1 --- a/src/HOL/List.thy	Thu Jul 28 20:39:51 2016 +0200
    11.2 +++ b/src/HOL/List.thy	Fri Jul 29 09:49:23 2016 +0200
    11.3 @@ -4443,6 +4443,23 @@
    11.4    qed
    11.5  qed
    11.6  
    11.7 +lemma sublists_refl: "xs \<in> set (sublists xs)"
    11.8 +by (induct xs) (simp_all add: Let_def)
    11.9 +
   11.10 +lemma subset_sublists: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (sublists xs)"
   11.11 +unfolding sublists_powset by simp
   11.12 +
   11.13 +lemma Cons_in_sublistsD:
   11.14 +  "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
   11.15 +by (induct xs) (auto simp: Let_def)
   11.16 +
   11.17 +lemma sublists_distinctD: "\<lbrakk> ys \<in> set (sublists xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
   11.18 +proof(induct xs arbitrary: ys)
   11.19 +  case (Cons x xs ys)
   11.20 +  then show ?case
   11.21 +    by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI sublists_powset)
   11.22 +qed simp
   11.23 +
   11.24  
   11.25  subsubsection \<open>@{const splice}\<close>
   11.26  
    12.1 --- a/src/HOL/Nat.thy	Thu Jul 28 20:39:51 2016 +0200
    12.2 +++ b/src/HOL/Nat.thy	Fri Jul 29 09:49:23 2016 +0200
    12.3 @@ -1336,10 +1336,32 @@
    12.4    by (induct n) simp_all
    12.5  
    12.6  lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
    12.7 -  for f :: "'a \<Rightarrow> ('a::lattice)"
    12.8 +  for f :: "'a \<Rightarrow> ('a::order)"
    12.9    by (induct n arbitrary: A B)
   12.10       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
   12.11  
   12.12 +lemma funpow_mono2:
   12.13 +  assumes "mono f"
   12.14 +  assumes "i \<le> j"
   12.15 +  assumes "x \<le> y"
   12.16 +  assumes "x \<le> f x"
   12.17 +  shows "(f ^^ i) x \<le> (f ^^ j) y"
   12.18 +using assms(2,3)
   12.19 +proof(induct j arbitrary: y)
   12.20 +  case (Suc j)
   12.21 +  show ?case
   12.22 +  proof(cases "i = Suc j")
   12.23 +    case True
   12.24 +    with assms(1) Suc show ?thesis
   12.25 +      by (simp del: funpow.simps add: funpow_simps_right monoD funpow_mono)
   12.26 +  next
   12.27 +    case False
   12.28 +    with assms(1,4) Suc show ?thesis
   12.29 +      by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le)
   12.30 +         (simp add: Suc.hyps monoD order_subst1)
   12.31 +  qed
   12.32 +qed simp
   12.33 +
   12.34  
   12.35  subsection \<open>Kleene iteration\<close>
   12.36  
   12.37 @@ -1406,6 +1428,30 @@
   12.38      by (intro gfp_upperbound) (simp del: funpow.simps)
   12.39  qed
   12.40  
   12.41 +lemma Kleene_iter_gpfp:
   12.42 +  assumes "mono f"
   12.43 +  and "p \<le> f p"
   12.44 +  shows "p \<le> (f ^^ k) (top::'a::order_top)"
   12.45 +proof(induction k)
   12.46 +  case 0 show ?case by simp
   12.47 +next
   12.48 +  case Suc
   12.49 +  from monoD[OF assms(1) Suc] assms(2)
   12.50 +  show ?case by simp
   12.51 +qed
   12.52 +
   12.53 +lemma gfp_Kleene_iter:
   12.54 +  assumes "mono f"
   12.55 +  and "(f ^^ Suc k) top = (f ^^ k) top"
   12.56 +  shows "gfp f = (f ^^ k) top" (is "?lhs = ?rhs")
   12.57 +proof(rule antisym)
   12.58 +  have "?rhs \<le> f ?rhs" using assms(2) by simp
   12.59 +  then show "?rhs \<le> ?lhs" by(rule gfp_upperbound)
   12.60 +
   12.61 +  show "?lhs \<le> ?rhs"
   12.62 +    using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
   12.63 +qed
   12.64 +
   12.65  
   12.66  subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
   12.67  
    13.1 --- a/src/HOL/Order_Relation.thy	Thu Jul 28 20:39:51 2016 +0200
    13.2 +++ b/src/HOL/Order_Relation.thy	Fri Jul 29 09:49:23 2016 +0200
    13.3 @@ -55,6 +55,21 @@
    13.4    "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
    13.5  by(simp add: order_on_defs trans_diff_Id)
    13.6  
    13.7 +lemma linear_order_on_singleton [iff]: "linear_order_on {x} {(x, x)}"
    13.8 +unfolding order_on_defs by simp
    13.9 +
   13.10 +lemma linear_order_on_acyclic:
   13.11 +  assumes "linear_order_on A r"
   13.12 +  shows "acyclic (r - Id)"
   13.13 +using strict_linear_order_on_diff_Id[OF assms] 
   13.14 +by(auto simp add: acyclic_irrefl strict_linear_order_on_def)
   13.15 +
   13.16 +lemma linear_order_on_well_order_on:
   13.17 +  assumes "finite r"
   13.18 +  shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
   13.19 +unfolding well_order_on_def
   13.20 +using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
   13.21 +
   13.22  
   13.23  subsection\<open>Orders on the field\<close>
   13.24  
   13.25 @@ -306,6 +321,22 @@
   13.26    order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   13.27  qed
   13.28  
   13.29 +lemma finite_Linear_order_induct[consumes 3, case_names step]:
   13.30 +  assumes "Linear_order r"
   13.31 +  and "x \<in> Field r"
   13.32 +  and "finite r"
   13.33 +  and step: "\<And>x. \<lbrakk>x \<in> Field r; \<And>y. y \<in> aboveS r x \<Longrightarrow> P y\<rbrakk> \<Longrightarrow> P x"
   13.34 +  shows "P x"
   13.35 +using assms(2)
   13.36 +proof(induct rule: wf_induct[of "r\<inverse> - Id"])
   13.37 +  from assms(1,3) show "wf (r\<inverse> - Id)"
   13.38 +    using linear_order_on_well_order_on linear_order_on_converse
   13.39 +    unfolding well_order_on_def by blast
   13.40 +next
   13.41 +  case (2 x) then show ?case
   13.42 +    by - (rule step; auto simp: aboveS_def intro: FieldI2)
   13.43 +qed
   13.44 +
   13.45  
   13.46  subsection \<open>Variations on Well-Founded Relations\<close>
   13.47  
    14.1 --- a/src/HOL/Partial_Function.thy	Thu Jul 28 20:39:51 2016 +0200
    14.2 +++ b/src/HOL/Partial_Function.thy	Fri Jul 29 09:49:23 2016 +0200
    14.3 @@ -47,6 +47,11 @@
    14.4    qed
    14.5  qed
    14.6  
    14.7 +lemma (in ccpo) admissible_chfin:
    14.8 +  "(\<forall>S. Complete_Partial_Order.chain op \<le> S \<longrightarrow> finite S)
    14.9 +  \<Longrightarrow> ccpo.admissible Sup op \<le> P"
   14.10 +using in_chain_finite by (blast intro: ccpo.admissibleI)
   14.11 +
   14.12  subsection \<open>Axiomatic setup\<close>
   14.13  
   14.14  text \<open>This techical locale constains the requirements for function
    15.1 --- a/src/HOL/Relation.thy	Thu Jul 28 20:39:51 2016 +0200
    15.2 +++ b/src/HOL/Relation.thy	Fri Jul 29 09:49:23 2016 +0200
    15.3 @@ -206,6 +206,9 @@
    15.4  lemma refl_on_empty [simp]: "refl_on {} {}"
    15.5    by (simp add: refl_on_def)
    15.6  
    15.7 +lemma refl_on_singleton [iff]: "refl_on {x} {(x, x)}"
    15.8 +by (blast intro: refl_onI)
    15.9 +
   15.10  lemma refl_on_def' [nitpick_unfold, code]:
   15.11    "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)"
   15.12    by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
   15.13 @@ -335,6 +338,9 @@
   15.14  lemma antisymP_equality [simp]: "antisymP op ="
   15.15    by (auto intro: antisymI)
   15.16  
   15.17 +lemma antisym_singleton [iff]: "antisym {x}"
   15.18 +by (blast intro: antisymI)
   15.19 +
   15.20  
   15.21  subsubsection \<open>Transitivity\<close>
   15.22  
   15.23 @@ -393,17 +399,34 @@
   15.24  lemma transp_equality [simp]: "transp op ="
   15.25    by (auto intro: transpI)
   15.26  
   15.27 +lemma trans_empty [iff]: "trans {}"
   15.28 +by (blast intro: transI)
   15.29 +
   15.30 +lemma transp_empty [iff]: "transp (\<lambda>x y. False)"
   15.31 +using trans_empty[to_pred] by(simp add: bot_fun_def)
   15.32 +
   15.33 +lemma trans_singleton [iff]: "trans {(a, a)}"
   15.34 +by (blast intro: transI)
   15.35 +
   15.36 +lemma transp_singleton [iff]: "transp (\<lambda>x y. x = a \<and> y = a)"
   15.37 +by(simp add: transp_def)
   15.38  
   15.39  subsubsection \<open>Totality\<close>
   15.40  
   15.41  definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   15.42    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)"
   15.43  
   15.44 +lemma total_onI [intro?]:
   15.45 +  "(\<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"
   15.46 +unfolding total_on_def by blast
   15.47 +
   15.48  abbreviation "total \<equiv> total_on UNIV"
   15.49  
   15.50  lemma total_on_empty [simp]: "total_on {} r"
   15.51    by (simp add: total_on_def)
   15.52  
   15.53 +lemma total_on_singleton [iff]: "total_on {x} {(x, x)}"
   15.54 +unfolding total_on_def by blast
   15.55  
   15.56  subsubsection \<open>Single valued relations\<close>
   15.57  
   15.58 @@ -776,6 +799,12 @@
   15.59  definition Field :: "'a rel \<Rightarrow> 'a set"
   15.60    where "Field r = Domain r \<union> Range r"
   15.61  
   15.62 +lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
   15.63 +unfolding Field_def by blast
   15.64 +
   15.65 +lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
   15.66 +  unfolding Field_def by auto
   15.67 +
   15.68  lemma Domain_fst [code]: "Domain r = fst ` r"
   15.69    by force
   15.70  
   15.71 @@ -902,6 +931,9 @@
   15.72  lemma Domain_unfold: "Domain r = {x. \<exists>y. (x, y) \<in> r}"
   15.73    by blast
   15.74  
   15.75 +lemma Field_square [iff]: "Field (x \<times> x) = x"
   15.76 +unfolding Field_def by blast
   15.77 +
   15.78  
   15.79  subsubsection \<open>Image of a set under a relation\<close>
   15.80