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