theory Demo8 imports Main begin

-- "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


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

section "More Isar"

text {* . = by assumption,  .. = by rule *}

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> B \<and> A"
proof 
  assume "A" and "B"
  show "A" .
  show "B" .
qed

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> B \<and> A" 
proof -  
  assume "A" and "B"
  show "B \<and> A" ..
qed


text {* backward/forward *}

lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB show "B \<and> A"
  proof
    assume "A" "B"
    show "B \<and> A" ..
  qed
qed


text{* fix *}

lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P (f x)"
proof                       
  fix a
  from P show "P (f a)" ..  
qed

text{* Proof text can only refer to global constants, free variables
in the lemma, and local names introduced via fix or obtain. *}

lemma assumes Pf: "\<exists>x. P (f x)" shows "\<exists>y. P y"
proof -
  from Pf show ?thesis
  proof              
    fix x
    assume "P (f x)"
    show ?thesis ..  
  qed
qed

text {* obtain *}

lemma assumes Pf: "\<exists>x. P (f x)" shows "\<exists>y. P y"
proof -
  from Pf obtain x where "P(f x)" ..
  thus "\<exists>y. P y" ..
qed


lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
proof
  fix y
  from ex obtain x where "\<forall>y. P x y" ..
  hence "P x y" ..
  thus "\<exists>x. P x y" ..
qed

lemma 
  assumes A: "\<forall>x y. P x y \<and> Q x y" 
  shows "\<exists>x y. P x y \<and> Q x y"
proof -
  from A obtain x y where P: "P x y" and Q: "Q x y" by blast
  thus ?thesis by blast
qed

lemma "\<exists>x. P x \<longrightarrow> (\<forall>x. P x)"
oops

text {* moreover *}

thm mono_def monoI

lemma 
  assumes mono_f: "mono (f::int\<Rightarrow>int)"
      and mono_g: "mono (g::int\<Rightarrow>int)"
  shows "mono (\<lambda>i. f i + g i)"
proof 
  fix i and j :: "int"
  assume A: "i \<le> j"
  from A mono_f have "f i \<le> f j" by (simp add: mono_def)
  moreover
  from A mono_g have "g i \<le> g j" by (simp add: mono_def)
  ultimately 
  show "f i + g i \<le> f j + g j" by auto
qed

end