Theory Open_Induction.Open_Induction

(*  Title:      Open Induction
    Author:     Mizuhito Ogawa
                Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

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  (yB. 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  {}  (xA. glb (⊏) C x  Q x)  (yC. Q y))"

lemma openI [Pure.intro]:
  "(C. chain C  C  {}  xA. glb (⊏) C x  Q x  yC. Q y)  open Q"
by (auto simp: open_def)

lemma open_glb:
  "chain C; C  {}; open Q; xC. ¬ 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  {}  (xA. glb (⊏) C x))"

lemma downward_completeI [Pure.intro]:
  assumes "C. chain C  C  {}  xA. 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  {}  xA. 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  {}  xA. glb P C x  Q x  yC. 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 = "{xA. ¬ 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