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