theory Demo7 imports Main begin

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

text {* Isar *}

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> A \<and> B"
proof (rule conjI)
  assume A: "A"
  from A show "A" by assumption
next
  assume "B"
  from `B` show "B" by assumption
qed


lemma 
  assumes A: "A"
  assumes B: "B"
  shows "A \<and> B"
proof (rule conjI)
  from A show "A" by assumption
  from B show "B" by assumption
qed


lemma "(x::nat) + 1 = 1 + x"
proof -
  have A: "x + 1 = Suc x" by simp
  have B: "1 + x = Suc x" by simp
  show "x + 1 = 1 + x" by (simp only: A B)
qed
  
-- ------------------------------------------------------------------

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"
  apply (simp split: nat.splits)
  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"
  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"
  apply (simp cong: if_cong)
  oops

thm add_ac
thm 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"
  apply (simp cong: conj_cong)
  oops

-- "single stepping: subst"

thm add_commute

lemma "a + b = x + (y::nat)"
  apply (subst add_commute) 
  back
  -- "since Isabelle2005 also: apply (subst (asm) some_thm)" 
  oops

end