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

section "More Isar"

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

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

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> B \<and> A" 
proof -  
  assume A: "A" and B: "B"
  from B A
  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 "B" "A"
    from this
    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)"
    from this
    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


text {* moreover *}

lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB have "B" by (rule conjunct2)
  moreover from AB have "A" by (rule conjunct1)
  ultimately show "B \<and> A" by (rule conjI)
qed

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 simp
qed

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

end