Theory Wlog_Examples

section ‹‹Wlog_Examples› -- Examples how to use \texttt{wlog}›

theory Wlog_Examples
  imports Wlog Complex_Main
begin

text ‹The theorem @{thm [source] Complex.card_nth_roots} has the additional assumption \<^term>‹n > 0›.
  We use exactly the same proof except for stating that w.l.o.g., \<^term>‹n > 0›.›
lemma card_nth_roots_strengthened:
  assumes "c ≠ 0"
  shows   "card {z::complex. z ^ n = c} = n"
proof -
  wlog n_pos: "n > 0"
    using negation by (simp add: infinite_UNIV_char_0)
  have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}"
    by (rule sym, rule bij_betw_same_card, rule bij_betw_nth_root_unity) fact+
  also have "… = n" by (rule card_roots_unity_eq) fact+
  finally show ?thesis .
qed

text ‹This example very roughly follows Harrison \<^cite>‹"harrison-wlog"›:›
lemma schur_ineq:
  fixes a b c :: ‹'a :: linordered_idom› and k :: nat
  assumes a0: ‹a ≥ 0› and b0: ‹b ≥ 0› and c0: ‹c ≥ 0›
  shows ‹a^k * (a - b) * (a - c) + b^k * (b - a) * (b - c) + c^k * (c - a) * (c - b) ≥ 0›
    (is ‹?lhs ≥ 0›)
proof -
  wlog ordered[simp]: ‹a ≤ b› ‹b ≤ c› generalizing a b c keeping a0 b0 c0
    apply (rule rev_mp[OF c0]; rule rev_mp[OF b0]; rule rev_mp[OF a0])
    apply (rule linorder_wlog_3[of _ a b c])
     apply (simp add: algebra_simps)
    by (simp add: hypothesis)

  from ordered have [simp]: ‹a ≤ c›
    by linarith

  have ‹?lhs = (c - b) * (c^k * (c - a) - b^k * (b - a)) + a^k * (c - a) * (b - a)›
    by (simp add: algebra_simps)
  also have ‹… ≥ 0›
    by (auto intro!: add_nonneg_nonneg mult_nonneg_nonneg mult_mono power_mono zero_le_power simp: a0 b0 c0)
  finally show ‹?lhs ≥ 0›
    by -
qed

text ‹The following illustrates how facts already proven before a @{command wlog} can be still be used after the wlog.
  The example does not do anything useful.›
lemma ‹A ⟹ B ⟹ A ∧ B›
proof -
  have test1: ‹1=1› by simp
  assume a: ‹A›
  then have test2: ‹A ∨ 1≠2› by simp
      ― ‹Isabelle marks this as being potentially based on assumption @{thm [source] a}.
          (Note: this is not done by actual dependency tracking. Anything that is proven after the @{command assume} command can depend on the assumption.)›
  assume b: ‹B›
  with a have test3: ‹A ∧ B› by simp
      ― ‹Isabelle marks this as being potentially based on assumption @{thm [source] a}, @{thm [source] b}›
  wlog true: ‹True› generalizing A B keeping b
    ― ‹A pointless wlog: we can wlog assume \<^term>‹True›.
       Notice: we only keep the assumption @{thm [source] b} around.›
    using negation by blast
  text ‹The already proven theorems cannot be accessed directly anymore (wlog starts a new proof block).
        Recovered versions are available, however:›
  thm wlog_keep.test1
    ― ‹The fact is fully recovered since it did not depend on any assumptions.›
  thm wlog_keep.test2
    ― ‹This fact depended on assumption ‹a› which we did not keep. So the original fact might not hold anymore.
        Therefore, @{thm [source] wlog_keep.test2} becomes \<^term>‹A ⟹ A ∨ 1 ≠ 2›. (Note the added \<^term>‹A› premise.)›
  thm wlog_keep.test3
    ― ‹This fact depended on assumptions ‹a› and ‹b›. But we kept @{thm [source] b}.
        Therefore, @{thm [source] wlog_keep.test2} becomes \<^term>‹A ⟹ A ∧ B›. (Note that only \<^term>‹A› is added as a premise.)›
  oops
    ― ‹Aborting the proof here because we cannot prove \<^term>‹A ∧ B› anymore since we dropped assumption ‹a› for demonstration purposes.›

end