huffman@31349: (* Title : Limits.thy
huffman@31349: Author : Brian Huffman
huffman@31349: *)
huffman@31349:
huffman@31349: header {* Filters and Limits *}
huffman@31349:
huffman@31349: theory Limits
huffman@36822: imports RealVector
huffman@31349: begin
huffman@31349:
huffman@44081: subsection {* Filters *}
huffman@31392:
huffman@31392: text {*
huffman@44081: This definition also allows non-proper filters.
huffman@31392: *}
huffman@31392:
huffman@36358: locale is_filter =
huffman@44081: fixes F :: "('a \ bool) \ bool"
huffman@44081: assumes True: "F (\x. True)"
huffman@44081: assumes conj: "F (\x. P x) \ F (\x. Q x) \ F (\x. P x \ Q x)"
huffman@44081: assumes mono: "\x. P x \ Q x \ F (\x. P x) \ F (\x. Q x)"
huffman@36358:
wenzelm@49834: typedef 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}"
huffman@31392: proof
huffman@44081: show "(\x. True) \ ?filter" by (auto intro: is_filter.intro)
huffman@31392: qed
huffman@31349:
huffman@44195: lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"
huffman@44195: using Rep_filter [of F] by simp
huffman@31392:
huffman@44081: lemma Abs_filter_inverse':
huffman@44081: assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"
huffman@44081: using assms by (simp add: Abs_filter_inverse)
huffman@31392:
huffman@31392:
huffman@31392: subsection {* Eventually *}
huffman@31349:
huffman@44081: definition eventually :: "('a \ bool) \ 'a filter \ bool"
huffman@44195: where "eventually P F \ Rep_filter F P"
huffman@36358:
huffman@44081: lemma eventually_Abs_filter:
huffman@44081: assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
huffman@44081: unfolding eventually_def using assms by (simp add: Abs_filter_inverse)
huffman@31349:
huffman@44081: lemma filter_eq_iff:
huffman@44195: shows "F = F' \ (\P. eventually P F = eventually P F')"
huffman@44081: unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
huffman@36360:
huffman@44195: lemma eventually_True [simp]: "eventually (\x. True) F"
huffman@44081: unfolding eventually_def
huffman@44081: by (rule is_filter.True [OF is_filter_Rep_filter])
huffman@31349:
huffman@44195: lemma always_eventually: "\x. P x \ eventually P F"
huffman@36630: proof -
huffman@36630: assume "\x. P x" hence "P = (\x. True)" by (simp add: ext)
huffman@44195: thus "eventually P F" by simp
huffman@36630: qed
huffman@36630:
huffman@31349: lemma eventually_mono:
huffman@44195: "(\x. P x \ Q x) \ eventually P F \ eventually Q F"
huffman@44081: unfolding eventually_def
huffman@44081: by (rule is_filter.mono [OF is_filter_Rep_filter])
huffman@31349:
huffman@31349: lemma eventually_conj:
huffman@44195: assumes P: "eventually (\x. P x) F"
huffman@44195: assumes Q: "eventually (\x. Q x) F"
huffman@44195: shows "eventually (\x. P x \ Q x) F"
huffman@44081: using assms unfolding eventually_def
huffman@44081: by (rule is_filter.conj [OF is_filter_Rep_filter])
huffman@31349:
huffman@31349: lemma eventually_mp:
huffman@44195: assumes "eventually (\x. P x \ Q x) F"
huffman@44195: assumes "eventually (\x. P x) F"
huffman@44195: shows "eventually (\x. Q x) F"
huffman@31349: proof (rule eventually_mono)
huffman@31349: show "\x. (P x \ Q x) \ P x \ Q x" by simp
huffman@44195: show "eventually (\x. (P x \ Q x) \ P x) F"
huffman@31349: using assms by (rule eventually_conj)
huffman@31349: qed
huffman@31349:
huffman@31349: lemma eventually_rev_mp:
huffman@44195: assumes "eventually (\x. P x) F"
huffman@44195: assumes "eventually (\x. P x \ Q x) F"
huffman@44195: shows "eventually (\x. Q x) F"
huffman@31349: using assms(2) assms(1) by (rule eventually_mp)
huffman@31349:
huffman@31349: lemma eventually_conj_iff:
huffman@44195: "eventually (\x. P x \ Q x) F \ eventually P F \ eventually Q F"
huffman@44081: by (auto intro: eventually_conj elim: eventually_rev_mp)
huffman@31349:
huffman@31349: lemma eventually_elim1:
huffman@44195: assumes "eventually (\i. P i) F"
huffman@31349: assumes "\i. P i \ Q i"
huffman@44195: shows "eventually (\i. Q i) F"
huffman@44081: using assms by (auto elim!: eventually_rev_mp)
huffman@31349:
huffman@31349: lemma eventually_elim2:
huffman@44195: assumes "eventually (\i. P i) F"
huffman@44195: assumes "eventually (\i. Q i) F"
huffman@31349: assumes "\i. P i \ Q i \ R i"
huffman@44195: shows "eventually (\i. R i) F"
huffman@44081: using assms by (auto elim!: eventually_rev_mp)
huffman@31349:
noschinl@45892: lemma eventually_subst:
noschinl@45892: assumes "eventually (\n. P n = Q n) F"
noschinl@45892: shows "eventually P F = eventually Q F" (is "?L = ?R")
noschinl@45892: proof -
noschinl@45892: from assms have "eventually (\x. P x \ Q x) F"
noschinl@45892: and "eventually (\x. Q x \ P x) F"
noschinl@45892: by (auto elim: eventually_elim1)
noschinl@45892: then show ?thesis by (auto elim: eventually_elim2)
noschinl@45892: qed
noschinl@45892:
noschinl@46886: ML {*
wenzelm@47432: fun eventually_elim_tac ctxt thms thm =
wenzelm@47432: let
noschinl@46886: val thy = Proof_Context.theory_of ctxt
noschinl@46886: val mp_thms = thms RL [@{thm eventually_rev_mp}]
noschinl@46886: val raw_elim_thm =
noschinl@46886: (@{thm allI} RS @{thm always_eventually})
noschinl@46886: |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
noschinl@46886: |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
noschinl@46886: val cases_prop = prop_of (raw_elim_thm RS thm)
noschinl@46886: val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
noschinl@46886: in
noschinl@46886: CASES cases (rtac raw_elim_thm 1) thm
noschinl@46886: end
noschinl@46886: *}
noschinl@46886:
wenzelm@47432: method_setup eventually_elim = {*
wenzelm@47432: Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
wenzelm@47432: *} "elimination of eventually quantifiers"
noschinl@45892:
noschinl@45892:
huffman@36360: subsection {* Finer-than relation *}
huffman@36360:
huffman@44195: text {* @{term "F \ F'"} means that filter @{term F} is finer than
huffman@44195: filter @{term F'}. *}
huffman@36360:
huffman@44081: instantiation filter :: (type) complete_lattice
huffman@36360: begin
huffman@36360:
huffman@44081: definition le_filter_def:
huffman@44195: "F \ F' \ (\P. eventually P F' \ eventually P F)"
huffman@36360:
huffman@36360: definition
huffman@44195: "(F :: 'a filter) < F' \ F \ F' \ \ F' \ F"
huffman@36360:
huffman@36360: definition
huffman@44081: "top = Abs_filter (\P. \x. P x)"
huffman@36630:
huffman@36630: definition
huffman@44081: "bot = Abs_filter (\P. True)"
huffman@36360:
huffman@36630: definition
huffman@44195: "sup F F' = Abs_filter (\P. eventually P F \ eventually P F')"
huffman@36630:
huffman@36630: definition
huffman@44195: "inf F F' = Abs_filter
huffman@44195: (\P. \Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))"
huffman@36630:
huffman@36630: definition
huffman@44195: "Sup S = Abs_filter (\P. \F\S. eventually P F)"
huffman@36630:
huffman@36630: definition
huffman@44195: "Inf S = Sup {F::'a filter. \F'\S. F \ F'}"
huffman@36630:
huffman@36630: lemma eventually_top [simp]: "eventually P top \ (\x. P x)"
huffman@44081: unfolding top_filter_def
huffman@44081: by (rule eventually_Abs_filter, rule is_filter.intro, auto)
huffman@36630:
huffman@36629: lemma eventually_bot [simp]: "eventually P bot"
huffman@44081: unfolding bot_filter_def
huffman@44081: by (subst eventually_Abs_filter, rule is_filter.intro, auto)
huffman@36360:
huffman@36630: lemma eventually_sup:
huffman@44195: "eventually P (sup F F') \ eventually P F \ eventually P F'"
huffman@44081: unfolding sup_filter_def
huffman@44081: by (rule eventually_Abs_filter, rule is_filter.intro)
huffman@44081: (auto elim!: eventually_rev_mp)
huffman@36630:
huffman@36630: lemma eventually_inf:
huffman@44195: "eventually P (inf F F') \
huffman@44195: (\Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))"
huffman@44081: unfolding inf_filter_def
huffman@44081: apply (rule eventually_Abs_filter, rule is_filter.intro)
huffman@44081: apply (fast intro: eventually_True)
huffman@44081: apply clarify
huffman@44081: apply (intro exI conjI)
huffman@44081: apply (erule (1) eventually_conj)
huffman@44081: apply (erule (1) eventually_conj)
huffman@44081: apply simp
huffman@44081: apply auto
huffman@44081: done
huffman@36630:
huffman@36630: lemma eventually_Sup:
huffman@44195: "eventually P (Sup S) \ (\F\S. eventually P F)"
huffman@44081: unfolding Sup_filter_def
huffman@44081: apply (rule eventually_Abs_filter, rule is_filter.intro)
huffman@44081: apply (auto intro: eventually_conj elim!: eventually_rev_mp)
huffman@44081: done
huffman@36630:
huffman@36360: instance proof
huffman@44195: fix F F' F'' :: "'a filter" and S :: "'a filter set"
huffman@44195: { show "F < F' \ F \ F' \ \ F' \ F"
huffman@44195: by (rule less_filter_def) }
huffman@44195: { show "F \ F"
huffman@44195: unfolding le_filter_def by simp }
huffman@44195: { assume "F \ F'" and "F' \ F''" thus "F \ F''"
huffman@44195: unfolding le_filter_def by simp }
huffman@44195: { assume "F \ F'" and "F' \ F" thus "F = F'"
huffman@44195: unfolding le_filter_def filter_eq_iff by fast }
huffman@44195: { show "F \ top"
huffman@44195: unfolding le_filter_def eventually_top by (simp add: always_eventually) }
huffman@44195: { show "bot \ F"
huffman@44195: unfolding le_filter_def by simp }
huffman@44195: { show "F \ sup F F'" and "F' \ sup F F'"
huffman@44195: unfolding le_filter_def eventually_sup by simp_all }
huffman@44195: { assume "F \ F''" and "F' \ F''" thus "sup F F' \ F''"
huffman@44195: unfolding le_filter_def eventually_sup by simp }
huffman@44195: { show "inf F F' \ F" and "inf F F' \ F'"
huffman@44195: unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
huffman@44195: { assume "F \ F'" and "F \ F''" thus "F \ inf F' F''"
huffman@44081: unfolding le_filter_def eventually_inf
huffman@44195: by (auto elim!: eventually_mono intro: eventually_conj) }
huffman@44195: { assume "F \ S" thus "F \ Sup S"
huffman@44195: unfolding le_filter_def eventually_Sup by simp }
huffman@44195: { assume "\F. F \ S \ F \ F'" thus "Sup S \ F'"
huffman@44195: unfolding le_filter_def eventually_Sup by simp }
huffman@44195: { assume "F'' \ S" thus "Inf S \ F''"
huffman@44195: unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
huffman@44195: { assume "\F'. F' \ S \ F \ F'" thus "F \ Inf S"
huffman@44195: unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
huffman@36360: qed
huffman@36360:
huffman@36360: end
huffman@36360:
huffman@44081: lemma filter_leD:
huffman@44195: "F \ F' \ eventually P F' \ eventually P F"
huffman@44081: unfolding le_filter_def by simp
huffman@36360:
huffman@44081: lemma filter_leI:
huffman@44195: "(\P. eventually P F' \ eventually P F) \ F \ F'"
huffman@44081: unfolding le_filter_def by simp
huffman@36360:
huffman@36360: lemma eventually_False:
huffman@44195: "eventually (\x. False) F \ F = bot"
huffman@44081: unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
huffman@36360:
huffman@44342: abbreviation (input) trivial_limit :: "'a filter \ bool"
huffman@44342: where "trivial_limit F \ F = bot"
huffman@44342:
huffman@44342: lemma trivial_limit_def: "trivial_limit F \ eventually (\x. False) F"
huffman@44342: by (rule eventually_False [symmetric])
huffman@44342:
huffman@44342:
huffman@44081: subsection {* Map function for filters *}
huffman@36654:
huffman@44081: definition filtermap :: "('a \ 'b) \ 'a filter \ 'b filter"
huffman@44195: where "filtermap f F = Abs_filter (\P. eventually (\x. P (f x)) F)"
huffman@36654:
huffman@44081: lemma eventually_filtermap:
huffman@44195: "eventually P (filtermap f F) = eventually (\x. P (f x)) F"
huffman@44081: unfolding filtermap_def
huffman@44081: apply (rule eventually_Abs_filter)
huffman@44081: apply (rule is_filter.intro)
huffman@44081: apply (auto elim!: eventually_rev_mp)
huffman@44081: done
huffman@36654:
huffman@44195: lemma filtermap_ident: "filtermap (\x. x) F = F"
huffman@44081: by (simp add: filter_eq_iff eventually_filtermap)
huffman@36654:
huffman@44081: lemma filtermap_filtermap:
huffman@44195: "filtermap f (filtermap g F) = filtermap (\x. f (g x)) F"
huffman@44081: by (simp add: filter_eq_iff eventually_filtermap)
huffman@36654:
huffman@44195: lemma filtermap_mono: "F \ F' \ filtermap f F \ filtermap f F'"
huffman@44081: unfolding le_filter_def eventually_filtermap by simp
huffman@44081:
huffman@44081: lemma filtermap_bot [simp]: "filtermap f bot = bot"
huffman@44081: by (simp add: filter_eq_iff eventually_filtermap)
huffman@36654:
hoelzl@50247: subsection {* Order filters *}
huffman@31392:
hoelzl@50247: definition at_top :: "('a::order) filter"
hoelzl@50247: where "at_top = Abs_filter (\P. \k. \n\k. P n)"
huffman@31392:
hoelzl@50247: lemma eventually_at_top_linorder:
hoelzl@50247: fixes P :: "'a::linorder \ bool" shows "eventually P at_top \ (\N. \n\N. P n)"
hoelzl@50247: unfolding at_top_def
huffman@44081: proof (rule eventually_Abs_filter, rule is_filter.intro)
hoelzl@50247: fix P Q :: "'a \ bool"
huffman@36662: assume "\i. \n\i. P n" and "\j. \n\j. Q n"
huffman@36662: then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto
huffman@36662: then have "\n\max i j. P n \ Q n" by simp
huffman@36662: then show "\k. \n\k. P n \ Q n" ..
huffman@36662: qed auto
huffman@36662:
hoelzl@50247: lemma eventually_at_top_dense:
hoelzl@50247: fixes P :: "'a::dense_linorder \ bool" shows "eventually P at_top \ (\N. \n>N. P n)"
hoelzl@50247: unfolding eventually_at_top_linorder
hoelzl@50247: proof safe
hoelzl@50247: fix N assume "\n\N. P n" then show "\N. \n>N. P n" by (auto intro!: exI[of _ N])
hoelzl@50247: next
hoelzl@50247: fix N assume "\n>N. P n"
hoelzl@50247: moreover from gt_ex[of N] guess y ..
hoelzl@50247: ultimately show "\N. \n\N. P n" by (auto intro!: exI[of _ y])
hoelzl@50247: qed
hoelzl@50247:
hoelzl@50247: definition at_bot :: "('a::order) filter"
hoelzl@50247: where "at_bot = Abs_filter (\P. \k. \n\k. P n)"
hoelzl@50247:
hoelzl@50247: lemma eventually_at_bot_linorder:
hoelzl@50247: fixes P :: "'a::linorder \ bool" shows "eventually P at_bot \ (\N. \n\N. P n)"
hoelzl@50247: unfolding at_bot_def
hoelzl@50247: proof (rule eventually_Abs_filter, rule is_filter.intro)
hoelzl@50247: fix P Q :: "'a \ bool"
hoelzl@50247: assume "\i. \n\i. P n" and "\j. \n\j. Q n"
hoelzl@50247: then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto
hoelzl@50247: then have "\n\min i j. P n \ Q n" by simp
hoelzl@50247: then show "\k. \n\k. P n \ Q n" ..
hoelzl@50247: qed auto
hoelzl@50247:
hoelzl@50247: lemma eventually_at_bot_dense:
hoelzl@50247: fixes P :: "'a::dense_linorder \ bool" shows "eventually P at_bot \ (\N. \nn\N. P n" then show "\N. \nnN. \n\N. P n" by (auto intro!: exI[of _ y])
hoelzl@50247: qed
hoelzl@50247:
hoelzl@50247: subsection {* Sequentially *}
hoelzl@50247:
hoelzl@50247: abbreviation sequentially :: "nat filter"
hoelzl@50247: where "sequentially == at_top"
hoelzl@50247:
hoelzl@50247: lemma sequentially_def: "sequentially = Abs_filter (\P. \k. \