Dear all,
in preparation for the next release I refactored one of our AFP entries
(Abstract-Rewriting). There was an underlying theory Util.thy (quite
big), which essentially turned out to be unused in the rest of the AFP
entry ;) (but we heavily rely on it in IsaFoR, which is not in the AFP).
While refactoring I saw that some lemmas from Util.thy have found their
way (either by moving or independently) into the main Isabelle
distribution (mostly List.thy) -- but without being removed from the AFP
entry.
Still there are many definitions and lemmas left that are not part of
the main distribution (some of which are ugly and ad hoc, but others
quite useful and maybe deserving to end up in the distribution or library).
After this rather long story ;) my actual question: Is there some way to
propose definitions/lemmas for the main distribution/library? If not,
maybe someone of the developers feels like reading through the attached
theory-file and picking out whatever he/she likes?
cheers
chris
On 02/28/2012 10:21 PM, Makarius wrote:
Dear all,
4 months after Isabelle2011-1 we are roughly in the middle between two
official releases. This is a good point to recollect things for the
coming release, better than a few weeks before actual rollout (which
will the time for testing the integrated system, not adding new features).
After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working
through my mail folders like crazy, I still have issues in the pipeline
that need to be reanimated. I also need to figure out which essential
things of the Prover IDE can make it into the release ...
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
theory Collect
imports
Main
"~~/src/HOL/Library/Infinite_Set"
begin
section {* Auxiliary Lemmas *}
lemma set_not_empty: "xs \<noteq> [] \<longleftrightarrow> set xs \<noteq> {}"
by simp
lemma set_subset_insertI: "set xs \<subseteq> set (List.insert x xs)" by auto
lemma set_removeAll_subset: "set (removeAll x xs) \<subseteq> set xs" by auto
lemma ballI2[Pure.intro]:
assumes "\<And>x y. (x, y) \<in> A \<Longrightarrow> P x y"
shows "\<forall>(x, y)\<in>A. P x y"
using assms by auto
lemma all_Suc_conv[simp]:
"(\<forall>i<Suc n. P i) \<longleftrightarrow> P 0 \<and> (\<forall>i<n. P
(Suc i))" (is "?l = ?r")
proof
assume ?l thus ?r by auto
next
assume ?r show ?l
proof (intro allI impI)
fix i
assume "i < Suc n"
with `?r` show "P i" by (cases i, auto)
qed
qed
lemma ex_Suc_conv[simp]:
"(\<exists>i<Suc n. P i) \<longleftrightarrow> P 0 \<or> (\<exists>i<n. P
(Suc i))" (is "?l = ?r")
using all_Suc_conv[of n "\<lambda>i. \<not> P i"] by blast
subsection {* Induction Rules *}
text {* Induction over a finite set of natural numbers. *}
lemma bound_nat_induct[consumes 1]:
assumes "n \<in> {l..u}" and "P l" and "\<And>n. \<lbrakk>P n; n \<in>
{l..<u}\<rbrakk> \<Longrightarrow> P (Suc n)"
shows "P n"
using assms
proof (induct n)
case (Suc n) thus ?case by (cases "Suc n = l") auto
qed simp
subsection {* Functions on Lists *}
primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a
option" where
"find _ [] = None"
| "find P (x#xs) = (if P x then Some x else find P xs)"
lemma find_NoneE:
assumes "find P xs = None" shows "\<not> (\<exists>x. x \<in> set xs \<and> P
x)"
using assms
proof (induct xs)
case (Cons x xs)
hence "\<not> (P x)" by auto
with Cons show ?case by auto
qed simp
lemma find_NoneI:
assumes "\<not> (\<exists>x. x \<in> set xs \<and> P x)" shows "find P xs =
None"
using assms
proof (induct xs)
case (Cons x xs)
assume "\<not> (\<exists>y. y \<in> set (x#xs) \<and> P y)"
hence "\<not> (P x)" by auto
with Cons show ?case by auto
qed simp
lemma not_mem_find_None_conv: "\<not> (\<exists>x. x \<in> set xs \<and> P x)
\<longleftrightarrow> find P xs = None"
using find_NoneI find_NoneE by blast
lemma find_SomeD:
assumes "find P xs = Some x"
shows "\<exists>i<length xs. P (xs ! i) \<and> x = (xs ! i) \<and>
(\<forall>j<i. \<not> P (xs ! j))"
using assms
proof (induct xs)
case (Cons y ys)
show ?case
proof (cases "P y")
case True with Cons show ?thesis by auto
next
case False with Cons have "find P ys = Some x" by simp
with Cons have "\<exists>i<length ys. P (ys ! i) \<and> x = ys ! i \<and>
(\<forall>j<i. \<not> P (ys ! j))" by simp
then obtain i where "i < length ys" and "P (ys ! i)" and "x = ys ! i"
and "\<forall>j<i. \<not> P (ys ! j)" by auto
from `i < length ys` have "Suc i < length (y#ys)" by simp
moreover from `P (ys ! i)` have "P ((y#ys) ! Suc i)" by simp
moreover from `x = ys ! i` have "x = (y#ys) ! Suc i" by simp
moreover have "\<forall>j<Suc i. \<not> P ((y#ys) ! j)"
proof (intro allI impI)
fix j assume "j < Suc i" thus "\<not> P ((y#ys) ! j)" using
`\<forall>j<i. \<not> P (ys ! j)` False
by (induct j) auto
qed
ultimately show ?thesis by best
qed
qed simp
lemma find_SomeI:
assumes "\<exists>i<length xs. P (xs ! i) \<and> x = (xs ! i) \<and>
(\<forall>j<i. \<not> P (xs ! j))"
shows "find P xs = Some x"
using assms
proof (induct xs)
case (Cons y ys)
with `\<exists>i<length (y#ys). P ((y#ys) ! i) \<and> x = (y#ys) ! i \<and>
(\<forall>j<i. \<not> P ((y#ys) ! j))`
obtain i where "i < length (y#ys)" and "P ((y#ys) ! i)"
and "x = (y#ys) ! i" and "\<forall>j<i. \<not> P ((y#ys) ! j)" by force
show ?case
proof (cases i)
case 0
with `P ((y#ys) ! i)` have "P y" by simp
with `x = (y#ys) ! i` 0 have "y = x" by simp
with `P y` show ?thesis by simp
next
case (Suc k)
from Suc `\<forall>j<i. \<not> P ((y#ys) ! j)` have "\<not> P y" by auto
hence rec: "find P (y#ys) = find P ys" by simp
from Suc `i < length (y#ys)` have k1: "k < length ys" by simp
from Suc `P ((y#ys) ! i)` have k2: "P (ys ! k)" by simp
from Suc `x = (y#ys) ! i` have k3:"x = (ys ! k)" by simp
from Suc `\<forall>j<i. \<not> P ((y#ys) ! j)` have "\<forall>j<k. \<not> P
(ys ! j)" by auto
with k1 k2 k3 have "\<exists>i<length ys. P (ys ! i) \<and> x = ys ! i
\<and> (\<forall>j<i. \<not> P (ys ! j))" by auto
with Cons have "find P ys = Some x" by auto
with rec show ?thesis by simp
qed
qed simp
lemma ex_find_Some_conv:
"(\<exists>i<length xs. P (xs ! i) \<and> x = xs ! i \<and> (\<forall>j<i.
\<not> P (xs ! j))) \<longleftrightarrow> find P xs = Some x"
by (blast intro: find_SomeI dest: find_SomeD)
lemma find_cong[fundef_cong]:
assumes xs: "xs = ys" and set: "\<And>x. x \<in> set ys \<Longrightarrow> f x
= g x"
shows "find f xs = find g ys"
proof (cases "find f xs")
case None
hence "find f ys = None" using xs by simp
hence "\<not>(\<exists> x. x \<in> set ys \<and> f x)" using find_NoneE by
auto
hence "\<not>(\<exists> x. x \<in> set ys \<and> g x)" using set by best
hence "find g ys = None" using find_NoneI by auto
thus ?thesis using None by auto
next
case (Some x)
hence "find f ys = Some x" using xs by simp
hence "\<exists>i<length ys. f(ys!i) \<and> (x = (ys!i)) \<and>
(\<forall>j<i. \<not> f (ys!j))" by (rule find_SomeD)
hence "\<exists>i<length ys. g(ys!i) \<and> (x = (ys!i)) \<and>
(\<forall>j<i. \<not> g (ys!j))" using set by auto
hence "find g ys = Some x" by (rule find_SomeI)
thus ?thesis using Some by auto
qed
primrec
list_union :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"list_union [] ys = ys"
| "list_union (x # xs) ys = (let zs = list_union xs ys in if x \<in> set zs
then zs else x # zs)"
lemma set_list_union[simp]: "set (list_union xs ys) = set xs \<union> set ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "x \<in> set (list_union xs ys)") (auto)
qed simp
declare list_union.simps[simp del]
(*Why was list_inter thrown out of List.thy?*)
fun list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"list_inter [] bs = []"
| "list_inter (a#as) bs =
(if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
lemma set_list_inter[simp]:
"set (list_inter xs ys) = set xs \<inter> set ys"
by (induct rule: list_inter.induct) simp_all
declare list_inter.simps[simp del]
primrec list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"list_diff [] ys = []"
| "list_diff (x # xs) ys = (let zs = list_diff xs ys in if x \<in> set ys then
zs else x # zs)"
lemma set_list_diff[simp]:
"set (list_diff xs ys) = set xs - set ys"
proof (induct xs)
case (Cons x xs) thus ?case by (cases "x \<in> set ys") (auto)
qed simp
declare list_diff.simps[simp del]
fun lookup :: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b option"
where
"lookup x [] = None"
| "lookup x ((y, v)#xs) = (if x = y then Some v else lookup x xs)"
lemma lookup_NoneD:
assumes "lookup x xs = None"
shows "\<not> (\<exists>v. (x, v) \<in> set xs)"
using assms
proof (induct xs)
case (Cons yv xs)
show ?case
proof (cases yv)
case (Pair y v)
with Cons show ?thesis by (cases "x = y") auto
qed
qed simp
lemma lookup_SomeD:
assumes "lookup x xs = Some v"
shows "(x, v) \<in> set xs"
using assms
proof (induct xs)
case (Cons yv xs)
show ?case
proof (cases yv)
case (Pair y v)
with Cons show ?thesis by (cases "x = y") auto
qed
qed simp
subsection {* Lists and Sets *}
lemma nth_append_take:
assumes "i \<le> length xs" shows "(take i xs @ y#ys)!i = y"
proof -
from assms have a: "length(take i xs) = i" by simp
have "(take i xs @ y#ys)!(length(take i xs)) = y" by (rule nth_append_length)
thus ?thesis unfolding a .
qed
lemma nth_append_take_is_nth_conv:
assumes "i < j" and "j \<le> length xs" shows "(take j xs @ ys)!i = xs!i"
proof -
from assms have "i < length(take j xs)" by simp
hence "(take j xs @ ys)!i = take j xs ! i" unfolding nth_append by simp
thus ?thesis unfolding nth_take[OF assms(1)] .
qed
lemma nth_append_drop_is_nth_conv:
assumes "j < i" and "j \<le> length xs" and "i \<le> length xs"
shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
from assms have j: "length(take j xs) = j" by auto
from `j < i` obtain n where "Suc(j + n) = i" using less_imp_Suc_add by auto
with assms have i: "i = length(take j xs) + Suc n" by auto
have len: "Suc j + n \<le> length xs" using assms i by auto
have "(take j xs @ y # drop (Suc j) xs)!i =
(y # drop (Suc j) xs)!(i - length(take j xs))" unfolding nth_append i by
auto
also have "\<dots> = (y # drop (Suc j) xs)!(Suc n)" unfolding i by simp
also have "\<dots> = (drop (Suc j) xs)!n" by simp
finally show ?thesis unfolding nth_drop[OF len] using i j by simp
qed
lemma nth_append_take_drop_is_nth_conv:
assumes "i \<le> length xs" and "j \<le> length xs" and "i \<noteq> j"
shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i"
proof -
from assms have "i < j \<or> i > j" by auto
thus ?thesis
proof
assume "i < j" thus ?thesis using assms by (auto simp:
nth_append_take_is_nth_conv)
next
assume "j < i" thus ?thesis using assms by (auto simp:
nth_append_drop_is_nth_conv)
qed
qed
lemma take_drop_imp_nth: "\<lbrakk>take i ss @ x # drop (Suc i) ss =
ss\<rbrakk> \<Longrightarrow> x = ss!i"
proof (induct ss arbitrary: i)
case Nil thus ?case by auto
next
case (Cons s ss)
from `take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss)` show ?case
proof (induct i)
case 0 thus ?case by auto
next
case (Suc i)
from Cons have IH: "take i ss @ x # drop (Suc i) ss = ss \<Longrightarrow> x
= ss!i" by auto
from Suc have "take i ss @ x # drop (Suc i) ss = ss" by auto
with IH show ?case by auto
qed
qed
lemma nth_take_prefix:
"length ys \<le> length xs \<Longrightarrow> \<forall>i < length ys. xs!i =
ys!i \<Longrightarrow> take (length ys) xs = ys"
proof (induct ys arbitrary: xs)
case Nil thus ?case by auto
next
case (Cons y ys) note IH = this
show ?case
proof (cases xs)
case Nil thus ?thesis using Cons by simp
next
case (Cons z zs)
hence "xs!0 = z" by simp
with IH have "z = y" by auto
from IH have "\<forall>i < length ys. xs!(Suc i) = ys!i" by auto
hence A:"\<forall>i < length ys. zs!i = ys!i" using Cons by auto
have B:"length ys \<le> length zs" using IH Cons by auto
have C:"take (length ys) zs = ys" using IH A B by simp
have "take (length (y#ys)) (z#zs) = z#(take (length ys) zs)" by simp
also have "\<dots> = z#ys" using C by simp
finally show ?thesis unfolding `z = y` `xs = z#zs` .
qed
qed
lemma nth_drop_0: "0 < length ss \<Longrightarrow> (ss!0)#drop (Suc 0) ss = ss"
by (induct ss) auto
lemma map_nth_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda> i. f (Suc i)) [0
..< n]"
by (induct n arbitrary: f, auto)
lemma zip_nth_conv: "length xs = length ys \<Longrightarrow> zip xs ys = map
(\<lambda> i. (xs ! i, ys ! i)) [0 ..< length ys]"
proof (induct xs arbitrary: ys, simp)
case (Cons x xs)
then obtain y yys where ys: "ys = y # yys" by (cases ys, auto)
with Cons have len: "length xs = length yys" by simp
show ?case unfolding ys
by (simp del: upt_Suc add: map_nth_Suc, unfold Cons(1)[OF len], simp)
qed
lemma append_Cons_nth_left:
assumes "i < length xs"
shows "(xs @ u # ys) ! i = xs ! i"
using assms nth_append[of xs _ i] by simp
lemma append_Cons_nth_middle:
assumes "i = length xs"
shows "(xs @ y # zs) ! i = y"
using assms by auto
lemma append_Cons_nth_right:
assumes "i > length xs"
shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
proof -
from assms have "i - length xs > 0" by auto
then obtain j where j: "i - length xs = Suc j" by (cases "i - length xs",
auto)
thus ?thesis by (simp add: nth_append)
qed
lemma append_Cons_nth_not_middle:
assumes "i \<noteq> length xs"
shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i"
proof (cases "i < length xs")
case True
thus ?thesis by (simp add: append_Cons_nth_left)
next
case False
with assms have "i > length xs" by arith
thus ?thesis by (rule append_Cons_nth_right)
qed
lemmas append_Cons_nth = append_Cons_nth_middle append_Cons_nth_not_middle
lemma map_id[simp]: "map id xs = xs" by (induct xs) auto
lemma map_nth_conv: "map f ss = map g ts \<Longrightarrow> \<forall>i < length
ss. f(ss!i) = g(ts!i)"
proof (intro allI impI)
fix i show "map f ss = map g ts \<Longrightarrow> i < length ss
\<Longrightarrow> f(ss!i) = g(ts!i)"
proof (induct ss arbitrary: i ts)
case Nil thus ?case by (induct ts) auto
next
case (Cons s ss) thus ?case
proof (induct ts)
case Nil thus ?case by simp
next
case (Cons t ts) thus ?case by (cases i) auto
qed
qed
qed
lemma replicate_prop:
assumes "P x"
shows "\<forall>y\<in>set (replicate n x). P y"
using assms by (induct n) simp_all
lemma set_foldr_remdups_set_map_conv[simp]:
"set (foldr (\<lambda>x xs. remdups (f x @ xs)) xs []) = \<Union>set (map
(set \<circ> f) xs)"
by (induct xs) auto
lemma nth_map_conv:
assumes "length xs = length ys"
and "\<forall>i<length xs. f (xs ! i) = g (ys ! i)"
shows "map f xs = map g ys"
using assms
proof (induct xs arbitrary: ys)
case (Cons x xs) thus ?case
proof (induct ys)
case (Cons y ys)
have "\<forall>i<length xs. f (xs ! i) = g (ys ! i)"
proof (intro allI impI)
fix i assume "i < length xs" thus "f (xs ! i) = g (ys ! i)" using Cons(4)
by force
qed
with Cons show ?case by auto
qed simp
qed simp
lemma map_nth_eq_conv:
assumes len: "length xs = length ys"
shows "(map f xs = ys) = (\<forall>i<length ys. f (xs ! i) = ys ! i)" (is "?l
= ?r")
proof -
have "(map f xs = ys) = (map f xs = map id ys)" by auto
also have "... = (\<forall> i < length ys. f (xs ! i) = id (ys ! i))" using
map_nth_conv[of f xs id ys] nth_map_conv[OF len, of f id] unfolding len
by blast
finally show ?thesis by auto
qed
lemma eq_length_concat_nth:
assumes "length xs = length ys"
and "\<And>i. i < length xs \<Longrightarrow> length (xs ! i) = length (ys
! i)"
shows "length (concat xs) = length (concat ys)"
using assms
proof (induct xs arbitrary: ys)
case Nil
thus ?case by auto
next
case (Cons x xs zs)
from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto)
note Cons = Cons[unfolded zs]
from Cons(2) have len: "length xs = length ys" by simp
from Cons(3)[of 0] have xy: "length x = length y" by simp
{
fix i
assume "i < length xs"
with Cons(3)[of "Suc i"]
have "length (xs ! i) = length (ys ! i)" by simp
}
from Cons(1)[OF len this] have ind: "length (concat xs) = length (concat ys)"
by simp
show ?case unfolding zs using xy ind by auto
qed
lemma concat_all_nth:
assumes "length xs = length ys"
and "\<And>i. i < length xs \<Longrightarrow> length (xs ! i) = length (ys
! i)"
and "\<And>i j. i < length xs \<Longrightarrow> j < length (xs ! i)
\<Longrightarrow> P (xs ! i ! j) (ys ! i ! j)"
shows "\<forall>k<length (concat xs). P (concat xs ! k) (concat ys ! k)"
using assms
proof (induct xs arbitrary: ys)
case Nil
thus ?case by auto
next
case (Cons x xs zs)
from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto)
note Cons = Cons[unfolded zs]
from Cons(2) have len: "length xs = length ys" by simp
from Cons(3)[of 0] have xy: "length x = length y" by simp
from Cons(4)[of 0] xy have pxy: "\<And> j. j < length x \<Longrightarrow> P
(x ! j) (y ! j)" by auto
{
fix i
assume i: "i < length xs"
with Cons(3)[of "Suc i"]
have len: "length (xs ! i) = length (ys ! i)" by simp
from Cons(4)[of "Suc i"] i len have "\<And> j. j < length (xs ! i)
\<Longrightarrow> P (xs ! i ! j) (ys ! i ! j)"
by auto
note len and this
}
from Cons(1)[OF len this] have ind: "\<And> k. k < length (concat xs)
\<Longrightarrow> P (concat xs ! k) (concat ys ! k)"
by auto
show ?case unfolding zs concat.simps
proof (intro allI impI)
fix k
assume k: "k < length (x @ concat xs)"
show "P ((x @ concat xs) ! k) ((y @ concat ys) ! k)"
proof (cases "k < length x")
case True
show ?thesis unfolding nth_append using True xy pxy[OF True]
by simp
next
case False
with k have "k - (length x) < length (concat xs)" by auto
then obtain n where n: "k - length x = n" and nxs: "n < length (concat
xs)" by auto
show ?thesis unfolding nth_append n n[unfolded xy] using False xy ind[OF
nxs]
by auto
qed
qed
qed
lemma [code_unfold]: "set xs \<subseteq> set ys \<longleftrightarrow> list_all
(\<lambda>x. x \<in> set ys) xs"
unfolding list_all_iff by auto
fun concat_lists :: "'a list list \<Rightarrow> 'a list list" where
"concat_lists [] = [[]]"
| "concat_lists (as # xs) = (let rec = concat_lists xs in concat (map
(\<lambda>vec. map (\<lambda>a. a # vec) as) rec))"
lemma set_concat_lists[simp]:
shows "set (concat_lists xs) = {as. length as = length xs \<and>
(\<forall>i<length xs. as ! i \<in> set (xs ! i))}"
proof (induct xs)
case Nil
show ?case by auto
next
case (Cons as xs)
have id: "set (concat_lists (as # xs)) =
{(a # bs) | a bs. length (a # bs) = length (as # xs) \<and> (\<forall>i<Suc
(length xs). (a # bs) ! i \<in> set ((as # xs) ! i))}" (is "?L = ?M")
by (auto simp: Cons)
show ?case (is "_ = ?R")
proof -
have one: "?M \<subseteq> ?R" by auto
{
fix cs
assume cs: "cs \<in> ?R"
then obtain c bs where cbs: "cs = c # bs" by (cases cs, auto)
from cs have "cs \<in> ?M" unfolding cbs by auto
}
with one show ?thesis unfolding id by auto
qed
qed
declare concat_lists.simps[simp del]
fun max_list :: "nat list \<Rightarrow> nat" where
"max_list [] = 0"
| "max_list (x # xs) = max x (max_list xs)"
lemma max_list: "x \<in> set xs \<Longrightarrow> x \<le> max_list xs"
by (induct xs) auto
fun max_f :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
"max_f f 0 = 0"
| "max_f f (Suc i) = max (f i) (max_f f i)"
lemma max_f: "i < n \<Longrightarrow> f i \<le> max_f f n"
proof (induct n)
case (Suc n)
thus ?case by (cases "i = n", auto)
qed simp
lemma max_list_mem: "xs \<noteq> [] \<Longrightarrow> max_list xs \<in> set xs"
proof (induct xs)
case (Cons x xs)
show ?case
proof (cases "x \<ge> max_list xs")
case True
thus ?thesis by auto
next
case False
hence max: "max_list xs > x" by auto
hence nil: "xs \<noteq> []" by (cases xs, auto)
from max have max: "max x (max_list xs) = max_list xs" by auto
from Cons(1)[OF nil] max show ?thesis by auto
qed
qed simp
lemma max_list_set: "max_list xs = (if set xs = {} then 0 else (THE x. x \<in>
set xs \<and> (\<forall> y \<in> set xs. y \<le> x)))"
proof (cases "xs = []")
case True thus ?thesis by simp
next
case False
note p = max_list_mem[OF this] max_list[of _ xs]
from False have id: "(set xs = {}) = False" by simp
show ?thesis unfolding id if_False
proof (rule the_equality[symmetric], intro conjI ballI, rule p, rule p)
fix x
assume "x \<in> set xs \<and> (\<forall> y \<in> set xs. y \<le> x)"
hence mem: "x \<in> set xs" and le: "\<And> y. y \<in> set xs
\<Longrightarrow> y \<le> x" by auto
from max_list[OF mem] le[OF max_list_mem[OF False]]
show "x = max_list xs" by simp
qed
qed
lemma max_list_eq_set: "set xs = set ys \<Longrightarrow> max_list xs =
max_list ys"
unfolding max_list_set by simp
fun min_list :: "('a :: linorder) list \<Rightarrow> 'a" where
"min_list [x] = x"
| "min_list (x # xs) = min x (min_list xs)"
lemma min_list: "(x :: 'a :: linorder) \<in> set xs \<Longrightarrow> min_list
xs \<le> x"
proof (induct xs, simp)
case (Cons y ys) note oCons = this
show ?case
proof (cases ys)
case Nil
thus ?thesis using Cons by auto
next
case (Cons z zs)
hence id: "min_list (y # ys) = min y (min_list ys)"
by auto
show ?thesis
proof (cases "x = y")
case True
show ?thesis unfolding id True by auto
next
case False
have "min y (min_list ys) \<le> min_list ys" by auto
also have "... \<le> x" using oCons False by auto
finally show ?thesis unfolding id .
qed
qed
qed
lemma min_list_Cons:
assumes xy: "x \<le> y"
and len: "length xs = length ys"
and xsys: "min_list xs \<le> min_list ys"
shows "min_list (x # xs) \<le> min_list (y # ys)"
proof (cases xs)
case Nil
with len have ys: "ys = []" by simp
with xy Nil show ?thesis by simp
next
case (Cons x' xs')
with len obtain y' ys' where ys: "ys = y' # ys'" by (cases ys, auto)
from Cons have one: "min_list (x # xs) = min x (min_list xs)" by auto
from ys have two: "min_list (y # ys) = min y (min_list ys)" by auto
show ?thesis unfolding one two using xy xsys
unfolding min_def by auto
qed
lemma min_list_nth:
assumes "length xs = length ys"
and "\<And>i. i < length ys \<Longrightarrow> xs ! i \<le> ys ! i"
shows "min_list xs \<le> min_list ys"
using assms
proof (induct xs arbitrary: ys)
case Nil
thus ?case by auto
next
case (Cons x xs zs)
from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto)
note Cons = Cons[unfolded zs]
from Cons(2) have len: "length xs = length ys" by simp
from Cons(3)[of 0] have xy: "x \<le> y" by simp
{
fix i
assume "i < length xs"
with Cons(3)[of "Suc i"] Cons(2)
have "xs ! i \<le> ys ! i" by simp
}
from Cons(1)[OF len this] Cons(2) have ind: "min_list xs \<le> min_list ys"
by simp
show ?case unfolding zs
by (rule min_list_Cons[OF xy len ind])
qed
lemma min_list_ex:
assumes "xs \<noteq> []" shows "\<exists>x\<in>set xs. min_list xs = x"
using assms
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs) note oCons = this
show ?case
proof (cases xs)
case Nil
thus ?thesis by auto
next
case (Cons y ys)
hence id: "min_list (x # xs) = min x (min_list xs)" and nNil: "xs \<noteq>
[]" by auto
show ?thesis
proof (cases "x \<le> min_list xs")
case True
show ?thesis unfolding id
by (rule bexI[of _ x], insert True, auto simp: min_def)
next
case False
show ?thesis unfolding id min_def
using oCons(1)[OF nNil] False by auto
qed
qed
qed
lemma min_list_subset:
assumes subset: "set ys \<subseteq> set xs" and mem: "min_list xs \<in> set
ys"
shows "min_list xs = min_list ys"
proof -
from subset mem have "xs \<noteq> []" by auto
from min_list_ex[OF this] obtain x where x: "x \<in> set xs" and mx:
"min_list xs = x" by auto
from min_list[OF mem] have two: "min_list ys \<le> min_list xs" by auto
from mem have "ys \<noteq> []" by auto
from min_list_ex[OF this] obtain y where y: "y \<in> set ys" and my:
"min_list ys = y" by auto
from y subset have "y \<in> set xs" by auto
from min_list[OF this] have one: "min_list xs \<le> y" by auto
from one two
show ?thesis unfolding mx my by auto
qed
lemma lookup_None[simp]:
assumes "V \<inter> set vs = {}" and "x \<in> V" shows "lookup x (zip vs ts)
= None"
using assms proof (induct vs arbitrary: ts)
case Nil show ?case by simp
next
case (Cons v vs)
note IH = this
hence neq: "v \<noteq> x" by auto
show ?case
proof (cases ts)
case Nil show ?thesis unfolding Nil by simp
next
case (Cons t ts')
from IH have IH': "lookup x (zip vs ts') = None" by auto
have "lookup x (zip (v#vs) ts) = lookup x ((v,t)#zip vs ts')" unfolding
Cons by simp
also have "\<dots> = lookup x (zip vs ts')" using neq by simp
also have "\<dots> = None" unfolding IH' by simp
finally show ?thesis .
qed
qed
lemma lookup_Some[simp]:
assumes "distinct vs" and "length vs \<le> length ts" and "i < length vs"
shows "lookup (vs!i) (zip vs ts) = Some(ts!i)"
using assms proof (induct i arbitrary: vs ts)
case 0 thus ?case by (induct ts) (induct vs,auto)+
next
case (Suc i) show ?case
proof (cases ts)
case Nil with Suc show ?thesis unfolding Nil by simp
next
case (Cons t ts')
note Cons' = this
show ?thesis
proof (cases vs)
case Nil from Suc show ?thesis unfolding Cons' Nil by simp
next
case (Cons v vs') from Suc show ?thesis unfolding Cons Cons' by auto
qed
qed
qed
lemma lookup_append_Some: "lookup x ps = Some y \<Longrightarrow> lookup x (ps
@ qs) = Some y"
by (induct ps, auto)
lemma lookup_append_None: "lookup x ps = None \<Longrightarrow> lookup x (ps @
qs) = lookup x qs"
by (induct ps, auto)
lemma take_drop_update_first: assumes "j < length ds" and "length cs = length
ds"
shows "(take j ds @ drop j cs)[j := ds ! j] = take (Suc j) ds @ drop (Suc j)
cs"
using assms
proof (induct j arbitrary: ds cs)
case 0
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by
(cases ds, simp, cases cs, auto)
show ?case unfolding ds cs by auto
next
case (Suc j)
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by
(cases ds, simp, cases cs, auto)
from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed
lemma take_drop_update_second: assumes "j < length ds" and "length cs = length
ds"
shows "(take j ds @ drop j cs)[j := cs ! j] = take j ds @ drop j cs"
using assms
proof (induct j arbitrary: ds cs)
case 0
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by
(cases ds, simp, cases cs, auto)
show ?case unfolding ds cs by auto
next
case (Suc j)
then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by
(cases ds, simp, cases cs, auto)
from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto
qed
lemma distinct_take_drop:
assumes dist: "distinct vs" and len: "i < length vs" shows "distinct(take i
vs @ drop (Suc i) vs)" (is "distinct(?xs@?ys)")
proof -
from id_take_nth_drop[OF len] have vs[symmetric]: "vs = ?xs @ vs!i # ?ys" .
with dist have "distinct ?xs" and "distinct(vs!i#?ys)" and "set ?xs \<inter>
set(vs!i#?ys) = {}" using distinct_append[of ?xs "vs!i#?ys"] by auto
hence "distinct ?ys" and "set ?xs \<inter> set ?ys = {}" by auto
with `distinct ?xs` show ?thesis using distinct_append[of ?xs ?ys] vs by simp
qed
primrec option_to_list :: "'a option \<Rightarrow> 'a list" where
"option_to_list (Some a) = [a]"
| "option_to_list None = []"
lemma option_to_list_sound[simp]: "set (option_to_list t) \<equiv> Option.set t"
by (induct t) auto
subsection {* size estimations *}
lemma list_size_pointwise2: assumes "length xs = length ys"
and "\<And> i. i < length ys \<Longrightarrow> f (xs ! i) \<le> g (ys ! i)"
shows "list_size f xs \<le> list_size g ys"
proof -
have id: "(list_size f xs \<le> list_size g ys) = (listsum (map f xs) \<le>
listsum (map g ys))"
unfolding list_size_conv_listsum assms(1) by auto
have "map f xs = map f (map (op ! xs) [0..<length xs])" using map_nth[of xs]
by simp
also have "... = map (\<lambda> i. f (xs ! i)) [0..<length xs]" (is "_ =
?xs") by simp
finally have xs: "map f xs = ?xs" .
have "map g ys = map g (map (op ! ys) [0..<length ys])" using map_nth[of ys]
by simp
also have "... = map (\<lambda> i. g (ys ! i)) [0..<length xs]" (is "_ =
?ys") using assms by simp
finally have ys: "map g ys = ?ys" .
show ?thesis
unfolding id unfolding xs ys
by (rule listsum_mono, insert assms, auto)
qed
lemma size_simp1: "t \<in> set ts \<Longrightarrow> size t < Suc (list_size
size ts)"
by (induct ts) auto
lemma size_simp2: "t \<in> set ts \<Longrightarrow> size t < Suc (Suc(size s +
list_size size ts))"
by (induct ts) auto
lemma size_simp3: assumes mem: "(x,y) \<in> set (zip xs ys)"
shows "size x < Suc (list_size size xs)"
using set_zip_leftD[OF mem] size_simp1 by auto
lemma size_simp4: assumes mem: "(x,y) \<in> set (zip xs ys)"
shows "size y < Suc (list_size size ys)"
using set_zip_rightD[OF mem] using size_simp1 by auto
subsection {* Partitions *}
text {* Check whether a list of sets forms a partition, i.e.,
whether the sets are pairwise disjoint. *}
definition is_partition :: "('a set)list \<Rightarrow> bool"
where "is_partition cs = (\<forall>j<length cs. \<forall>i<j. cs!i \<inter>
cs!j = {})"
(* and an equivalent but more symmetric version *)
definition is_partition_alt :: "('a set)list \<Rightarrow> bool"
where "is_partition_alt cs = (\<forall> i j. i < length cs \<and> j < length cs
\<and> i \<noteq> j \<longrightarrow> cs!i \<inter> cs!j = {})"
lemma is_partition_alt: "is_partition = is_partition_alt"
proof (intro ext)
fix cs
{
assume "is_partition_alt cs"
hence "is_partition cs" unfolding is_partition_def is_partition_alt_def by
auto
}
moreover
{
assume part: "is_partition cs"
have "is_partition_alt cs" unfolding is_partition_alt_def
proof (intro allI impI)
fix i j
assume "i < length cs \<and> j < length cs \<and> i \<noteq> j"
with part show "cs ! i \<inter> cs ! j = {}"
unfolding is_partition_def
by (cases "i < j", simp, cases "j < i", force, simp)
qed
}
ultimately
show "is_partition cs = is_partition_alt cs" by auto
qed
lemma is_partition_Nil: "is_partition [] = True" unfolding is_partition_def by
auto
lemma is_partition_Cons:
"is_partition(x#xs) = (is_partition xs \<and> x \<inter> \<Union>set xs = {})"
(is "?l = ?r")
proof
assume ?l
have one: "is_partition xs"
proof (unfold is_partition_def, intro allI impI)
fix j i assume "j < length xs" and "i < j"
hence "Suc j < length(x#xs)" and "Suc i < Suc j" by auto
from `?l`[unfolded is_partition_def,THEN spec,THEN mp,THEN spec,THEN mp,OF
this]
have "(x#xs)!(Suc i) \<inter> (x#xs)!(Suc j) = {}" .
thus "xs!i \<inter> xs!j = {}" by simp
qed
have two: "x \<inter> \<Union>set xs = {}"
proof (rule ccontr)
assume "x \<inter> \<Union>set xs \<noteq> {}"
then obtain y where "y \<in> x" and "y \<in> \<Union>set xs" by auto
then obtain z where "z \<in> set xs" and "y \<in> z" by auto
then obtain i where "i < length xs" and "xs!i = z" using in_set_conv_nth[of
z xs] by auto
with `y \<in> z` have "y \<in> (x#xs)!Suc i" by auto
moreover with `y \<in> x` have "y \<in> (x#xs)!0" by simp
ultimately have "(x#xs)!0 \<inter> (x#xs)!Suc i \<noteq> {}" by auto
moreover from `i < length xs` have "Suc i < length(x#xs)" by simp
ultimately show False using `?l`[unfolded is_partition_def] by best
qed
from one two show ?r ..
next
assume ?r
show ?l
proof (unfold is_partition_def, intro allI impI)
fix j i
assume j: "j < length (x # xs)"
assume i: "i < j"
from i obtain j' where j': "j = Suc j'" by (cases j, auto)
with j have j'len: "j' < length xs" and j'elem: "(x # xs) ! j = xs ! j'" by
auto
show "(x # xs) ! i \<inter> (x # xs) ! j = {}"
proof (cases i)
case 0
with j'elem have "(x # xs) ! i \<inter> (x # xs) ! j = x \<inter> xs !
j'" by auto
also have "\<dots> \<subseteq> x \<inter> \<Union>set xs" using j'len by
force
finally show ?thesis using `?r` by auto
next
case (Suc i')
with i j' have i'j': "i' < j'" by auto
from Suc j' have "(x # xs) ! i \<inter> (x # xs) ! j = xs ! i' \<inter>
xs ! j'" by auto
with `?r` i'j' j'len show ?thesis unfolding is_partition_def by auto
qed
qed
qed
subsection {*merging functions*}
definition fun_merge :: "('a \<Rightarrow> 'b)list \<Rightarrow> 'a set list
\<Rightarrow> 'a \<Rightarrow> 'b"
where "fun_merge fs as a \<equiv> (fs ! (LEAST i. i < length as \<and> a
\<in> as ! i)) a"
lemma fun_merge: assumes
i: "i < length as"
and a: "a \<in> as ! i"
and ident: "\<And> i j a. i < length as \<Longrightarrow> j < length as
\<Longrightarrow> a \<in> as ! i \<Longrightarrow> a \<in> as ! j
\<Longrightarrow> (fs ! i) a = (fs ! j) a"
shows "fun_merge fs as a = (fs ! i) a"
proof -
let ?p = "\<lambda> i. i < length as \<and> a \<in> as ! i"
let ?l = "LEAST i. ?p i"
have p: "?p ?l"
by (rule LeastI, insert i a, auto)
show ?thesis unfolding fun_merge_def
by (rule ident[OF _ i _ a], insert p, auto)
qed
lemma fun_merge_part: assumes
part: "is_partition as"
and i: "i < length as"
and a: "a \<in> as ! i"
shows "fun_merge fs as a = (fs ! i) a"
proof(rule fun_merge[OF i a])
fix i j a
assume "i < length as" and "j < length as" and "a \<in> as ! i" and "a \<in>
as ! j"
hence "i = j" using part[unfolded is_partition_alt is_partition_alt_def] by
(cases "i = j", auto)
thus "(fs ! i) a = (fs ! j) a" by simp
qed
subsection {* assignments from key-value pairs *}
fun enum_vectors :: "'c list \<Rightarrow> 'v list \<Rightarrow> ('v \<times>
'c)list list"
where "enum_vectors C [] = [[]]"
| "enum_vectors C (x # xs) = (let rec = enum_vectors C xs in concat (map
(\<lambda> vec. map (\<lambda> c. (x,c) # vec) C) rec))"
definition fun_of :: "('v \<times> 'c)list \<Rightarrow> 'v \<Rightarrow> 'c"
where [simp]: "fun_of vec x = the (lookup x vec)"
lemma enum_vectors_complete: assumes "C \<noteq> []"
shows "\<exists> vec \<in> set (enum_vectors C xs). \<forall> x \<in> set xs.
\<forall> c \<in> set C. \<alpha> x = c \<longrightarrow> fun_of vec x = c"
proof (induct xs, simp)
case (Cons x xs)
from this obtain vec where enum: "vec \<in> set (enum_vectors C xs)" and eq:
"\<forall> x \<in> set xs. \<forall> c \<in> set C. \<alpha> x = c
\<longrightarrow> fun_of vec x = c" by auto
from enum have res: "set (map (\<lambda> c. (x,c) # vec) C) \<subseteq> set
(enum_vectors C (x # xs)) " (is "_ \<subseteq> ?res") by auto
show ?case
proof (cases "\<alpha> x \<in> set C")
case False
from assms have "hd C \<in> set C" by auto
with res have elem: "(x,hd C) # vec \<in> ?res" (is "?vec \<in> _") by auto
from eq False have "\<forall> y \<in> set (x # xs). \<forall> c \<in> set
C. \<alpha> y = c \<longrightarrow> fun_of ?vec y = c" by auto
with elem show ?thesis by blast
next
case True
with res have elem: "(x, \<alpha> x) # vec \<in> ?res" (is "?vec \<in> _")
by auto
from eq True have "\<forall> y \<in> set (x # xs). \<forall> c \<in> set C.
\<alpha> y = c \<longrightarrow> fun_of ?vec y = c" by auto
with elem show ?thesis by blast
qed
qed
lemma enum_vectors_sound: assumes "y \<in> set xs" and "vec \<in> set
(enum_vectors C xs)"
shows "fun_of vec y \<in> set C"
using assms
proof (induct xs arbitrary: vec, simp)
case (Cons x xs vec)
from Cons(3) obtain v vecc where vec: "vec = v # vecc" by auto
note C3 = Cons(3)[unfolded vec enum_vectors.simps Let_def]
from C3 have vecc: "vecc \<in> set (enum_vectors C xs)" by auto
from C3 obtain c where v: "v = (x,c)" and c: "c \<in> set C" by auto
show ?case
proof (cases "y = x")
case True
show ?thesis unfolding vec v True using c by auto
next
case False
with Cons(2) have y: "y \<in> set xs" by auto
from False have id: "fun_of vec y = fun_of vecc y"
unfolding vec v by auto
show ?thesis unfolding id
by (rule Cons(1)[OF y vecc])
qed
qed
declare fun_of_def[simp del]
lemma fun_of_concat: assumes mem: "x \<in> set (map fst (\<tau>s i))"
and i: "i < n"
and ident: "\<And> i j. i < n \<Longrightarrow> j < n \<Longrightarrow> x
\<in> set (map fst (\<tau>s i)) \<Longrightarrow> x \<in> set (map fst (\<tau>s
j)) \<Longrightarrow> fun_of (\<tau>s i) x = fun_of (\<tau>s j) x"
shows "fun_of (concat (map \<tau>s [0..<n])) x = fun_of (\<tau>s i) x"
using assms
proof (induct n arbitrary: i \<tau>s)
case 0
thus ?case by simp
next
case (Suc n i \<tau>s) note IH = this
let ?\<tau>s = "\<lambda>i. \<tau>s (Suc i)"
have id: "concat (map \<tau>s [0..<Suc n]) = \<tau>s 0 @ concat (map ?\<tau>s
[0..<n])" unfolding map_nth_Suc by simp
let ?l = "lookup x (\<tau>s 0)"
show ?case
proof (cases i)
case 0
with IH(2) have x: "x \<in> set (map fst (\<tau>s 0))" by auto
then obtain y where xy: "(x,y) \<in> set (\<tau>s 0)" by auto
from lookup_NoneD[of x "\<tau>s 0"] xy have "?l \<noteq> None" by auto
then obtain y where look: "?l = Some y" by (cases "\<tau>s 0", auto)
show ?thesis unfolding 0 fun_of_def id look lookup_append_Some[OF look] by
simp
next
case (Suc j)
with IH(3)
have 0: "0 < i" and j: "j < n" by auto
show ?thesis
proof (cases "x \<in> set (map fst (\<tau>s 0))")
case False
have l: "?l = None"
proof (cases "?l")
case (Some y)
from lookup_SomeD[OF this] False show ?thesis by force
qed simp
show ?thesis unfolding fun_of_def id lookup_append_None[OF l]
unfolding fun_of_def[symmetric] Suc
proof (rule IH(1)[OF _ j])
show "x \<in> set (map fst (\<tau>s (Suc j)))" using IH(2) unfolding
Suc .
next
fix i j
assume "i < n" and "j < n" and "x \<in> set (map fst (\<tau>s (Suc
i)))" and "x \<in> set (map fst (\<tau>s (Suc j)))"
thus "fun_of (\<tau>s (Suc i)) x = fun_of (\<tau>s (Suc j)) x"
using IH(4)[of "Suc i" "Suc j"] by auto
qed
next
case True
then obtain y where xy: "(x,y) \<in> set (\<tau>s 0)" by auto
from lookup_NoneD[of x "\<tau>s 0"] xy have "?l \<noteq> None" by auto
then obtain y where look: "?l = Some y" by (cases "\<tau>s 0", auto)
have "fun_of (concat (map \<tau>s [0..<Suc n])) x = fun_of (\<tau>s 0) x"
unfolding id fun_of_def look
lookup_append_Some[OF look] by simp
also have "... = fun_of (\<tau>s i) x"
proof (rule IH(4)[OF _ IH(3)])
from xy show "x \<in> set (map fst (\<tau>s 0))" by force
next
from IH(2) show "x \<in> set (map fst (\<tau>s i))" by force
qed simp
finally show ?thesis .
qed
qed
qed
lemma fun_of_concat_part: assumes mem: "x \<in> set (map fst (\<tau>s i))"
and i: "i < n"
and partition: "is_partition (map (\<lambda> i. set (map fst (\<tau>s i)))
[0..<n])"
shows "fun_of (concat (map \<tau>s [0..<n])) x = fun_of (\<tau>s i) x"
proof (rule fun_of_concat, rule mem, rule i)
fix i j
assume "i < n" and "j < n" and "x \<in> set (map fst (\<tau>s i))" and "x
\<in> set (map fst (\<tau>s j))"
hence "i = j" using partition[unfolded is_partition_alt is_partition_alt_def]
by (cases "i = j", auto)
thus "fun_of (\<tau>s i) x = fun_of (\<tau>s j) x" by simp
qed
lemma fun_of_concat_merge: assumes "\<And> i. i < length ts \<Longrightarrow> x
\<in> h (ts ! i) \<Longrightarrow> fun_of (f i) x = (g ! i) x"
and "length ts = length g"
and "\<And> i. i < length ts \<Longrightarrow> (lookup x (f i) \<noteq> None)
= (x \<in> h (ts ! i))"
and "x \<in> h (ts ! i)"
and "i < length ts"
shows "fun_of (concat (map f [0..<length ts])) x = fun_merge g (map h ts) x"
using assms
unfolding fun_merge_def fun_of_def
proof (induct ts arbitrary: i f g)
case Nil
thus ?case by simp
next
case (Cons xy ts)
let ?p' = "\<lambda> ts i. i < length (map h ts) \<and> x \<in> map h ts ! i"
let ?p = "?p' (xy # ts)"
let ?P = "?p' ts"
let ?L = "LEAST i. ?p i"
have id: "the (lookup x (concat (map f [0..<length (xy # ts)]))) =
the (lookup x (f 0 @ concat (map (\<lambda> i. f (Suc i)) [0..<length
ts])))" (is "?l = the (lookup x ( _ @ ?l'))")
by (simp add: map_nth_Suc del: upt_Suc)
show ?case
proof (cases "lookup x (f 0)")
case (Some y)
from lookup_append_Some[OF Some]
have ly: "?l = y" unfolding id Some by simp
have "?p 0" using Cons(4)[of 0] using Some by auto
hence L0: "?L = 0"
by (rule Least_equality, simp)
from Cons(4)[of 0] Some have x: "x \<in> h xy" by auto
show ?thesis unfolding ly L0 using Cons(2)[of 0, unfolded Some] x by simp
next
case None
from lookup_append_None[OF None]
have ll: "?l = the (lookup x ?l')" unfolding id by simp
from Cons(4)[of 0] None have x: "x \<notin> h xy" by auto
hence p0: "\<not> ?p 0" by simp
from Cons(5) Cons(6) have pI: "?p i" unfolding nth_map[OF Cons(6)] by simp
from Least_Suc[of ?p, OF pI p0] have L: "?L = Suc (LEAST m. ?P m)" by simp
from Cons(3) obtain a g' where g: "g = a # g'" by (cases g, auto)
from Cons(5) x obtain j where i: "i = Suc j" by (cases i, auto)
show ?thesis unfolding ll L g nth_Cons_Suc
proof (rule Cons(1))
from g Cons(3) show "length ts = length g'" by auto
next
from Cons(5) i show "x \<in> h (ts ! j)" by auto
next
from Cons(6) i show "j < length ts" by auto
next
fix m
assume "m < length ts"
thus "(lookup x (f (Suc m)) \<noteq> None) = (x \<in> h (ts ! m))"
using Cons(4)[of "Suc m"] by auto
next
fix m
assume "m < length ts" and "x \<in> h (ts ! m)"
thus "the (lookup x (f (Suc m))) = (g' ! m) x"
using Cons(2)[of "Suc m"] unfolding g by auto
qed
qed
qed
subsection {* Miscellaneous *}
lemma infinite_imp_elem: "\<not> finite A \<Longrightarrow> \<exists> x. x
\<in> A"
by (cases "A = {}", auto)
lemma inf_pigeonhole_principle:
assumes "\<forall>k::nat. \<exists>i<n::nat. f k i"
shows "\<exists>i<n. \<forall>k. \<exists>k'\<ge>k. f k' i"
proof -
have nfin: "~ finite (UNIV :: nat set)" by auto
have fin: "finite ({i. i < n})" by auto
from pigeonhole_infinite_rel[OF nfin fin] assms
obtain i where i: "i < n" and nfin: "\<not> finite {a. f a i}" by auto
show ?thesis
proof (intro exI conjI, rule i, intro allI)
fix k
have "finite {a. f a i \<and> a < k}" by auto
with nfin have "\<not> finite ({a. f a i} - {a. f a i \<and> a < k})" by
auto
from infinite_imp_elem[OF this]
obtain a where "f a i" and "a \<ge> k" by auto
thus "\<exists> k' \<ge> k. f k' i" by force
qed
qed
subsection {*Combinators*}
definition const :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
"const \<equiv> (\<lambda>x y. x)"
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('b
\<Rightarrow> 'a \<Rightarrow> 'c)" where
"flip f \<equiv> (\<lambda>x y. f y x)"
declare flip_def[simp]
lemma const_apply[simp]: "const x y = x"
by (simp add: const_def)
lemma foldr_Cons [simp]:
"foldr op # xs ys = xs @ ys"
by (induct xs) simp_all
lemma foldl_flip_Cons[simp]:
"foldl (flip op #) xs ys = rev ys @ xs"
by (induct ys arbitrary: xs) simp_all
(*FIXME: already present as List.foldl_foldr, but
direction seems odd.*)
lemma foldr_flip_rev[simp]:
"foldr (flip f) (rev xs) a = foldl f a xs"
by (simp add: foldr_foldl)
(*FIXME: already present as List.foldr_foldr, but
direction seems odd.*)
lemma foldl_flip_rev[simp]:
"foldl (flip f) a (rev xs) = foldr f xs a"
by (simp add: foldl_foldr)
(*FIXME: available in HOL library?*)
interpretation o!: semigroup_add "op \<circ>"
by (unfold_locales) (simp add: o_assoc)
lemma foldl_assoc:
fixes b :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)
\<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 55)
assumes "\<And>f g h. f \<cdot> (g \<cdot> h) = f \<cdot> g \<cdot> h"
shows "foldl op \<cdot> (x \<cdot> y) zs = x \<cdot> foldl op \<cdot> y zs"
proof -
interpret semigroup_add b by (unfold_locales) (simp add: assms)
show ?thesis by (simp add: foldl_assoc)
qed
lemma foldr_assoc:
assumes "\<And>f g h. b (b f g) h = b f (b g h)"
shows "foldr b xs (b y z) = b (foldr b xs y) z"
using assms by (induct xs) simp_all
lemma foldl_foldr_o_id:
"foldl op \<circ> id fs = foldr op \<circ> fs id"
proof (induct fs)
case Nil show ?case by simp
next
case (Cons f fs)
have "id \<circ> f = f \<circ> id" by simp
with Cons [symmetric] show ?case
by (simp only: foldl_Cons List.foldr_Cons o_apply [of _ _ id] foldl_assoc
o_assoc)
qed
lemma foldr_o_o_id[simp]:
"foldr (op \<circ> \<circ> f) xs id a = foldr f xs a"
by (induct xs) simp_all
subsection {* For IsaFoR *}
fun debug :: "string \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> 'a"
where "debug i t x = x"
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
