Theory Open_Induction
section ‹Open Induction›
theory Open_Induction
imports Restricted_Predicates
begin
subsection ‹(Greatest) Lower Bounds and Chains›
text ‹
A set ‹B› has the \emph{lower bound} ‹x› iff ‹x› is
less than or equal to every element of ‹B›.
›
definition "lb P B x ⟷ (∀y∈B. P⇧=⇧= x y)"
lemma lbI [Pure.intro]:
"(⋀y. y ∈ B ⟹ P⇧=⇧= x y) ⟹ lb P B x"
by (auto simp: lb_def)
text ‹
A set ‹B› has the \emph{greatest lower bound} ‹x› iff ‹x› is
a lower bound of ‹B› \emph{and} less than or equal to every
other lower bound of ‹B›.
›
definition "glb P B x ⟷ lb P B x ∧ (∀y. lb P B y ⟶ P⇧=⇧= y x)"
lemma glbI [Pure.intro]:
"lb P B x ⟹ (⋀y. lb P B y ⟹ P⇧=⇧= y x) ⟹ glb P B x"
by (auto simp: glb_def)
text ‹Antisymmetric relations have unique glbs.›
lemma glb_unique:
"antisymp_on A P ⟹ x ∈ A ⟹ y ∈ A ⟹ glb P B x ⟹ glb P B y ⟹ x = y"
by (auto simp: glb_def antisymp_on_def)
context pred_on
begin
lemma chain_glb:
assumes "transp_on A (⊏)"
shows "chain C ⟹ glb (⊏) C x ⟹ x ∈ A ⟹ y ∈ A ⟹ y ⊏ x ⟹ chain ({y} ∪ C)"
using assms [unfolded transp_on_def]
unfolding chain_def glb_def lb_def
by (cases "C = {}") blast+
subsection ‹Open Properties›
definition "open Q ⟷ (∀C. chain C ∧ C ≠ {} ∧ (∃x∈A. glb (⊏) C x ∧ Q x) ⟶ (∃y∈C. Q y))"
lemma openI [Pure.intro]:
"(⋀C. chain C ⟹ C ≠ {} ⟹ ∃x∈A. glb (⊏) C x ∧ Q x ⟹ ∃y∈C. Q y) ⟹ open Q"
by (auto simp: open_def)
lemma open_glb:
"⟦chain C; C ≠ {}; open Q; ∀x∈C. ¬ Q x; x ∈ A; glb (⊏) C x⟧ ⟹ ¬ Q x"
by (auto simp: open_def)
subsection ‹Downward Completeness›
text ‹
A relation ‹⊏› is \emph{downward-complete} iff
every non-empty ‹⊏›-chain has a greatest lower bound.
›
definition "downward_complete ⟷ (∀C. chain C ∧ C ≠ {} ⟶ (∃x∈A. glb (⊏) C x))"
lemma downward_completeI [Pure.intro]:
assumes "⋀C. chain C ⟹ C ≠ {} ⟹ ∃x∈A. glb (⊏) C x"
shows "downward_complete"
using assms by (auto simp: downward_complete_def)
end
abbreviation "open_on P Q A ≡ pred_on.open A P Q"
abbreviation "dc_on P A ≡ pred_on.downward_complete A P"
lemmas open_on_def = pred_on.open_def
and dc_on_def = pred_on.downward_complete_def
lemma dc_onI [Pure.intro]:
assumes "⋀C. chain_on P C A ⟹ C ≠ {} ⟹ ∃x∈A. glb P C x"
shows "dc_on P A"
using assms by (auto simp: dc_on_def)
lemma open_onI [Pure.intro]:
"(⋀C. chain_on P C A ⟹ C ≠ {} ⟹ ∃x∈A. glb P C x ∧ Q x ⟹ ∃y∈C. Q y) ⟹ open_on P Q A"
by (auto simp: open_on_def)
lemma chain_on_reflclp:
"chain_on P⇧=⇧= A C ⟷ chain_on P A C"
by (auto simp: pred_on.chain_def)
lemma lb_reflclp:
"lb P⇧=⇧= B x ⟷ lb P B x"
by (auto simp: lb_def)
lemma glb_reflclp:
"glb P⇧=⇧= B x ⟷ glb P B x"
by (auto simp: glb_def lb_reflclp)
lemma dc_on_reflclp:
"dc_on P⇧=⇧= A ⟷ dc_on P A"
by (auto simp: dc_on_def chain_on_reflclp glb_reflclp)
subsection ‹The Open Induction Principle›
lemma open_induct_on [consumes 4, case_names less]:
assumes qo: "qo_on P A" and "dc_on P A" and "open_on P Q A"
and "x ∈ A"
and ind: "⋀x. ⟦x ∈ A; ⋀y. ⟦y ∈ A; strict P y x⟧ ⟹ Q y⟧ ⟹ Q x"
shows "Q x"
proof (rule ccontr)
assume "¬ Q x"
let ?B = "{x∈A. ¬ Q x}"
have "?B ⊆ A" by blast
interpret B: pred_on ?B P .
from B.Hausdorff obtain M
where chain: "B.chain M"
and max: "⋀C. B.chain C ⟹ M ⊆ C ⟹ M = C" by (auto simp: B.maxchain_def)
then have "M ⊆ ?B" by (auto simp: B.chain_def)
show False
proof (cases "M = {}")
assume "M = {}"
moreover have "B.chain {x}" using ‹x ∈ A› and ‹¬ Q x› by (simp add: B.chain_def)
ultimately show False using max by blast
next
interpret A: pred_on A P .
assume "M ≠ {}"
have "A.chain M" using chain by (auto simp: A.chain_def B.chain_def)
moreover with ‹dc_on P A› and ‹M ≠ {}› obtain m
where "m ∈ A" and "glb P M m" by (auto simp: A.downward_complete_def)
ultimately have "¬ Q m" and "m ∈ ?B"
using A.open_glb [OF _ ‹M ≠ {}› ‹open_on P Q A› _ _ ‹glb P M m›]
and ‹M ⊆ ?B› by auto
from ind [OF ‹m ∈ A›] and ‹¬ Q m› obtain y
where "y ∈ A" and "strict P y m" and "¬ Q y" by blast
then have "P y m" and "y ∈ ?B" by simp+
from transp_on_subset [OF qo_on_imp_transp_on [OF qo] ‹?B ⊆ A›]
have "transp_on ?B P" .
from B.chain_glb [OF this chain ‹glb P M m› ‹m ∈ ?B› ‹y ∈ ?B› ‹P y m›]
have "B.chain ({y} ∪ M)" .
then show False
using ‹glb P M m› and ‹strict P y m› by (cases "y ∈ M") (auto dest: max simp: glb_def lb_def)
qed
qed
subsection ‹Open Induction on Universal Domains›
text ‹Open induction on quasi-orders (i.e., @{class preorder}).›
lemma (in preorder) dc_open_induct [consumes 2, case_names less]:
assumes "dc_on (≤) UNIV"
and "open_on (≤) Q UNIV"
and "⋀x. (⋀y. y < x ⟹ Q y) ⟹ Q x"
shows "Q x"
proof -
have "qo_on (≤) UNIV" by (auto simp: qo_on_def transp_on_def reflp_on_def dest: order_trans)
from open_induct_on [OF this assms(1,2)]
show "Q x" using assms(3) unfolding less_le_not_le by blast
qed
subsection ‹Type Class of Downward Complete Orders›
class dcorder = preorder +
assumes dc_on_UNIV: "dc_on (≤) UNIV"
begin
text ‹Open induction on downward-complete orders.›
lemmas open_induct [consumes 1, case_names less] = dc_open_induct [OF dc_on_UNIV]
end
end