Theory Misc

theory Misc
  imports Main "Graph_Theory.Shortest_Path"
begin

text ‹These are some utility lemmas which are not directly concerned with the graph library.›

lemma Sup_in_set:
"⟦ finite (A::('a::complete_linorder) set); A ≠ {}; a = Sup A⟧
  ⟹ a ∈ A"
proof(induction A arbitrary: a rule: finite_induct)
  case (insert x F)
  show ?case
  proof(cases "F = {}")
    case False
    with insert.IH have "∃y. Sup F = y ∧ y ∈ F" by simp
    then obtain y where y_def: "Sup F = y" and y_in_F: "y ∈ F" by blast

    have [simp]: "Sup (insert x F) = sup x (Sup F)"
      using insert.hyps(1)
      by (induction F rule: finite_induct) (auto)

    with insert show ?thesis
    proof(cases "y ≤ x")
      case True
      then have "Sup (insert x F) = x"
        by (simp add: sup.absorb_iff1 y_def)
      with insert.prems(2) show ?thesis by blast
    next
      case False
      with y_def have "Sup (insert x F) = y"
        by (simp add: sup.absorb2)
      with insert.prems(2) y_in_F show ?thesis by blast
    qed
  qed (simp add: insert.prems)
qed simp

text ‹Analogous to the proof of @{thm Sup_in_set}.›
lemma Inf_in_set:
"⟦ finite (A::('a::complete_linorder) set); A ≠ {}; a = Inf A⟧
  ⟹ a ∈ A"
proof(induction A arbitrary: a rule: finite_induct)
  case (insert x F)
  show ?case
  proof(cases "F = {}")
    case False
    with insert.IH have "∃y. Inf F = y ∧ y ∈ F" by simp
    then obtain y where y_def: "Inf F = y" and y_in_F: "y ∈ F" by blast

    have [simp]: "Inf (insert x F) = inf x (Inf F)"
      using insert.hyps(1)
      by (induction F rule: finite_induct) (auto)

    with insert show ?thesis
    proof(cases "y ≥ x")
      case True
      then have "Inf (insert x F) = x"
        by (simp add: inf.absorb_iff1 y_def)
      with insert.prems(2) show ?thesis by blast
    next
      case False
      with y_def have "Inf (insert x F) = y"
        by (simp add: inf.absorb2)
      with insert.prems(2) y_in_F show ?thesis by blast
    qed
  qed (simp add: insert.prems)
qed simp

lemma mem_card1_singleton: "⟦ u ∈ U; card U = 1 ⟧ ⟹ U = {u}"
  by (metis card_1_singletonE singletonD)

lemma finite_Union: "⟦ finite A; ∀x ∈ A. finite (a x) ⟧ ⟹ finite (⋃{a x|x. x ∈ A})"
  by (induction A rule: finite_induct) (auto)

end