theory Demo8 imports Main begin

-- ------------------------------------------------------------------

text {* more automation *}

-- "clarsimp: repeated clarify and simp"
lemma "ys = []  \<Longrightarrow> \<forall>xs. xs @ ys = []"
  apply clarsimp
  oops

-- "auto: simplification, classical reasoning, more"
lemma "(\<exists>u::nat. x=y+u) \<longrightarrow> a*(b+c)+y \<le> x + a*b+a*c"
  apply (auto simp add: add_mult_distrib2)
  done

-- "also try: fastsimp and force"


text {* simplification with assumptions, more control: *}

lemma "\<forall>x. f x = g x \<and> g x = f x \<Longrightarrow> f [] = f [] @ []"
  -- "would diverge:"
  (*
  apply(simp)
  *)
  apply(simp (no_asm))
  done

-- ------------------------------------------------------

-- "let expressions"

lemma "let a = f x in g a = x"
  apply (simp add: Let_def)
  oops

thm Let_def

term "let a = f x in g a"

-- ------------------------------------------------------

-- "splitting case: manually"

lemma "(case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> x) = x"
  apply (simp only: split: nat.splits)
  apply simp
  done

-- "splitting if: automatic in conclusion"

lemma "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> (if x then A else B) = z"
  apply simp
  oops

lemma "\<lbrakk> (if x then A else B) = z; Q \<rbrakk> \<Longrightarrow> P"
  apply (simp split: split_if_asm)
  oops


thm conj_cong

lemma "A \<and> (A \<longrightarrow> B)"
  apply (simp cong: conj_cong)
  oops

thm if_cong

lemma "\<lbrakk> (if x then x \<longrightarrow> z else B) = z; Q \<rbrakk> \<Longrightarrow> P"
  apply (simp cong: if_cong)
  oops

thm add_ac
thm mult_ac

lemmas all_ac = add_ac mult_ac

lemma
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<odot>" 70)
  assumes A: "\<And>x y z. (x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
  assumes C: "\<And>x y. x \<odot> y = y \<odot> x"
  assumes AC: "\<And>x y z. x \<odot> (y \<odot> z) = y \<odot> (x \<odot> z)"
  shows "(z \<odot> x) \<odot> (y \<odot> v) = something"
  apply (simp only: C)
  apply (simp only: A C)
  apply (simp only: AC)
  oops
  
text {* when all else fails: tracing the simplifier
Isabelle/Isar -> Settings -> Trace Simplifier, then
Proof-General -> Buffers -> Trace *}

lemma "A \<and> (A \<longrightarrow> B)"
  apply (simp cong: conj_cong)
  oops

-- "single stepping: subst"

thm add_commute
declare add_assoc [simp]

lemma "a + b = x + ((y::nat) + z)"
  apply (simp add: add_assoc [symmetric] del: add_assoc)
  apply (subst add_commute [where a=x]) 
  oops


end