section ‹‹Wlog› -- Setting up the command›

theory Wlog
imports Main
keywords "wlog" :: prf_goal % "proof" (* and "goal" :: prf_decl % "proof" *)
  and "generalizing" and "keeping" and "goal"
begin

ML_file "wlog.ML"


text ‹For symmetric predicates involving 3--5 variables on a linearly ordered type,
 the following lemmas are very useful for wlog-proofs.
 
 For two variables, we already have @{thm [source] linorder_wlog}.›

lemma linorder_wlog_3:
  fixes x y z :: ‹'a :: linorder›
  assumes ‹∧x y z. P x y z ==> P y x z ∧ P x z y›
  assumes ‹∧x y z. x ≤ y ∧ y ≤ z ==> P x y z›
  shows ‹P x y z›
  using assms 
  by (metis linorder_le_cases)

lemma linorder_wlog_4:
  fixes x y z w :: ‹'a :: linorder›
  assumes ‹∧x y z w. P x y z w ==> P y x z w ∧ P x z y w ∧ P x y w z›
  assumes ‹∧x y z w. x ≤ y ∧ y ≤ z ∧ z ≤ w ==> P x y z w›
  shows ‹P x y z w›
  using assms 
  by (metis linorder_le_cases)

lemma linorder_wlog_5:
  fixes x y z w v :: ‹'a :: linorder›
  assumes ‹∧x y z w v. P x y z w v ==> P y x z w v ∧ P x z y w v ∧ P x y w z v ∧ P x y z v w›
  assumes ‹∧x y z w v. x ≤ y ∧ y ≤ z ∧ z ≤ w ∧ w ≤ v ==> P x y z w v›
  shows ‹P x y z w v›
  using assms
  by (smt (verit) linorder_le_cases)

end