--- a/src/HOL/Library/More_List.thy Mon Nov 04 22:05:20 2024 +0100
+++ b/src/HOL/Library/More_List.thy Mon Nov 04 22:36:42 2024 +0100
@@ -14,7 +14,7 @@
lemma strip_while_rev [simp]:
"strip_while P (rev xs) = rev (dropWhile P xs)"
by (simp add: strip_while_def)
-
+
lemma strip_while_Nil [simp]:
"strip_while P [] = []"
by (simp add: strip_while_def)
@@ -281,7 +281,7 @@
assumes "xs \<noteq> []"
shows "last xs = nth_default dflt xs (length xs - 1)"
using assms by (simp add: nth_default_def last_conv_nth)
-
+
lemma nth_default_map_eq:
"f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
by (simp add: nth_default_def)
@@ -332,15 +332,18 @@
"nth_default dflt xs = nth_default dflt ys
\<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
proof
- let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+ let ?strip_while = \<open>strip_while (HOL.eq dflt)\<close>
+ let ?xs = "?strip_while xs"
+ let ?ys = "?strip_while ys"
assume ?P
then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
by simp
have len: "length ?xs = length ?ys"
proof (rule ccontr)
- assume len: "length ?xs \<noteq> length ?ys"
+ assume neq: "\<not> ?thesis"
{ fix xs ys :: "'a list"
- let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+ let ?xs = "?strip_while xs"
+ let ?ys = "?strip_while ys"
assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
assume len: "length ?xs < length ?ys"
then have "length ?ys > 0" by arith
@@ -354,8 +357,8 @@
using eq by simp
moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
ultimately have False by (simp only: nth_default_beyond) simp
- }
- from this [of xs ys] this [of ys xs] len eq show False
+ }
+ from this [of xs ys] this [of ys xs] neq eq show False
by (auto simp only: linorder_class.neq_iff)
qed
then show ?Q
--- a/src/HOL/Library/While_Combinator.thy Mon Nov 04 22:05:20 2024 +0100
+++ b/src/HOL/Library/While_Combinator.thy Mon Nov 04 22:36:42 2024 +0100
@@ -33,7 +33,7 @@
also have "... = Suc (LEAST l. \<not> b ((c ^^ l) (c s)))"
by (simp add: funpow_swap1)
finally
- show ?thesis
+ show ?thesis
using True 2 \<open>b s\<close> by (simp add: funpow_swap1 while_option_def)
next
case False
@@ -46,9 +46,9 @@
assume [simp]: "\<not> b s"
have least: "(LEAST k. \<not> b ((c ^^ k) s)) = 0"
by (rule Least_equality) auto
- moreover
+ moreover
have "\<exists>k. \<not> b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
- ultimately show ?thesis unfolding while_option_def by auto
+ ultimately show ?thesis unfolding while_option_def by auto
qed
lemma while_option_stop2:
@@ -60,23 +60,22 @@
by(metis while_option_stop2)
theorem while_option_rule:
- assumes step: "!!s. P s ==> b s ==> P (c s)"
+ assumes step: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
and result: "while_option b c s = Some t"
and init: "P s"
shows "P t"
proof -
define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
from assms have t: "t = (c ^^ k) s"
- by (simp add: while_option_def k_def split: if_splits)
+ by (simp add: while_option_def k_def split: if_splits)
have 1: "\<forall>i<k. b ((c ^^ i) s)"
by (auto simp: k_def dest: not_less_Least)
-
- { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
- by (induct i) (auto simp: init step 1) }
+ have "P ((c ^^ i) s)" if "i \<le> k" for i
+ using that by (induct i) (auto simp: init step 1)
thus "P t" by (auto simp: t)
qed
-lemma funpow_commute:
+lemma funpow_commute:
"\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
by (induct k arbitrary: s) auto
@@ -138,23 +137,26 @@
have "\<not> b' ((c' ^^ Suc k') (f s))"
unfolding Suc[symmetric] by (rule LeastI) (rule k)
moreover
- { fix k assume "k \<le> k'"
- hence "k < ?k'" unfolding Suc by simp
- hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
- }
- note b' = this
- { fix k assume "k \<le> k'"
- hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
- and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
- and "P ((c ^^ k) s)"
+ have b': "b' ((c' ^^ k) (f s))" if "k \<le> k'" for k
+ proof -
+ from that have "k < ?k'" unfolding Suc by simp
+ thus ?thesis by (rule iffD1[OF not_not, OF not_less_Least])
+ qed
+ have b: "b ((c ^^ k) s)"
+ and body: "f ((c ^^ k) s) = (c' ^^ k) (f s)"
+ and inv: "P ((c ^^ k) s)"
+ if "k \<le> k'" for k
+ proof -
+ from that have "f ((c ^^ k) s) = (c' ^^ k) (f s)"
+ and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
+ and "P ((c ^^ k) s)"
by (induct k) (auto simp: b' assms)
with \<open>k \<le> k'\<close>
- have "b ((c ^^ k) s)"
- and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
- and "P ((c ^^ k) s)"
+ show "b ((c ^^ k) s)"
+ and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
+ and "P ((c ^^ k) s)"
by (auto simp: b')
- }
- note b = this(1) and body = this(2) and inv = this(3)
+ qed
hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
ultimately show ?thesis unfolding Suc using b
proof (intro Least_equality[symmetric], goal_cases)
@@ -188,7 +190,7 @@
qed
lemma while_option_commute:
- assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)"
+ assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)"
shows "map_option f (while_option b c s) = while_option b' c' (f s)"
by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
(auto simp add: assms)
@@ -213,8 +215,8 @@
\<close>
theorem while_rule_lemma:
- assumes invariant: "!!s. P s ==> b s ==> P (c s)"
- and terminate: "!!s. P s ==> \<not> b s ==> Q s"
+ assumes invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
+ and terminate: "\<And>s. P s \<Longrightarrow> \<not> b s \<Longrightarrow> Q s"
and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
shows "P s \<Longrightarrow> Q (while b c s)"
using wf
@@ -225,11 +227,11 @@
done
theorem while_rule:
- "[| P s;
- !!s. [| P s; b s |] ==> P (c s);
- !!s. [| P s; \<not> b s |] ==> Q s;
+ "\<lbrakk>P s;
+ \<And>s. \<lbrakk>P s; b s\<rbrakk> \<Longrightarrow> P (c s);
+ \<And>s. \<lbrakk>P s; \<not> b s\<rbrakk> \<Longrightarrow> Q s;
wf r;
- !!s. [| P s; b s |] ==> (c s, s) \<in> r |] ==>
+ \<And>s. \<lbrakk>P s; b s\<rbrakk> \<Longrightarrow> (c s, s) \<in> r\<rbrakk> \<Longrightarrow>
Q (while b c s)"
apply (rule while_rule_lemma)
prefer 4 apply assumption
@@ -241,10 +243,10 @@
text \<open>Combine invariant preservation and variant decrease in one goal:\<close>
theorem while_rule2:
- "[| P s;
- !!s. [| P s; b s |] ==> P (c s) \<and> (c s, s) \<in> r;
- !!s. [| P s; \<not> b s |] ==> Q s;
- wf r |] ==>
+ "\<lbrakk>P s;
+ \<And>s. \<lbrakk>P s; b s\<rbrakk> \<Longrightarrow> P (c s) \<and> (c s, s) \<in> r;
+ \<And>s. \<lbrakk>P s; \<not> b s\<rbrakk> \<Longrightarrow> Q s;
+ wf r\<rbrakk> \<Longrightarrow>
Q (while b c s)"
using while_rule[of P] by metis
@@ -281,7 +283,7 @@
bounding set:\<close>
lemma while_option_finite_subset_Some: fixes C :: "'a set"
- assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
+ assumes "mono f" and "\<And>X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
proof(rule measure_while_option_Some[where
f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
@@ -289,13 +291,13 @@
show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
(is "?L \<and> ?R")
proof
- show ?L by(metis A(1) assms(2) monoD[OF \<open>mono f\<close>])
+ show ?L by (metis A(1) assms(2) monoD[OF \<open>mono f\<close>])
show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
qed
qed simp
lemma lfp_the_while_option:
- assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
+ assumes "mono f" and "\<And>X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
proof-
obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
@@ -305,7 +307,7 @@
qed
lemma lfp_while:
- assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
+ assumes "mono f" and "\<And>X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
unfolding while_def using assms by (rule lfp_the_while_option) blast
@@ -377,9 +379,9 @@
and the AFP article Executable Transitive Closures by René Thiemann.\<close>
context
-fixes p :: "'a \<Rightarrow> bool"
-and f :: "'a \<Rightarrow> 'a list"
-and x :: 'a
+ fixes p :: "'a \<Rightarrow> bool"
+ and f :: "'a \<Rightarrow> 'a list"
+ and x :: 'a
begin
qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
@@ -398,32 +400,35 @@
(x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
Z \<subseteq> {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
-qualified lemma rtrancl_while_invariant:
+qualified lemma rtrancl_while_invariant:
assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
shows "rtrancl_while_invariant (rtrancl_while_step st)"
proof (cases st)
- fix ws Z assume st: "st = (ws, Z)"
+ fix ws Z
+ assume st: "st = (ws, Z)"
with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
qed
-lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
-shows "if ws = []
- then Z = {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z. p z)
- else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}\<^sup>* `` {x}"
+lemma rtrancl_while_Some:
+ assumes "rtrancl_while = Some(ws,Z)"
+ shows "if ws = []
+ then Z = {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z. p z)
+ else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}\<^sup>* `` {x}"
proof -
have "rtrancl_while_invariant ([x],{x})" by simp
with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
- { assume "ws = []"
- hence ?thesis using I
+ show ?thesis
+ proof (cases "ws = []")
+ case True
+ thus ?thesis using I
by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
- } moreover
- { assume "ws \<noteq> []"
- hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
+ next
+ case False
+ thus ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
by (simp add: subset_iff)
- }
- ultimately show ?thesis by simp
+ qed
qed
lemma rtrancl_while_finite_Some:
@@ -434,26 +439,29 @@
have "wf ?R" by (blast intro: wf_mlex)
then show ?thesis unfolding rtrancl_while_def
proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
- fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
+ fix st
+ assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
by (blast intro: rtrancl_while_invariant)
show "(rtrancl_while_step st, st) \<in> ?R"
proof (cases st)
- fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
+ fix ws Z
+ let ?ws = "fst (rtrancl_while_step st)"
+ let ?Z = "snd (rtrancl_while_step st)"
assume st: "st = (ws, Z)"
with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
- { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
+ show ?thesis
+ proof (cases "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []")
+ case False
then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
- with st ws have ?thesis unfolding mlex_prod_def by simp
- }
- moreover
- { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
+ with st ws show ?thesis unfolding mlex_prod_def by simp
+ next
+ case True
with st ws have "?Z = Z" "?ws = t" by (auto simp: filter_empty_conv)
- with st ws have ?thesis unfolding mlex_prod_def by simp
- }
- ultimately show ?thesis by blast
+ with st ws show ?thesis unfolding mlex_prod_def by simp
+ qed
qed
qed (simp_all add: rtrancl_while_invariant)
qed