theory Demo05
imports Main
begin

section {* 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: "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 {* . = 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 and 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 A: "A" and B: "B"
    from B A show "B \<and> A" ..
  qed
qed

-- "Backtick: refer to facts without naming them"

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

-- "then = from this"

lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  then show "B \<and> A"
  proof
    assume "B" "A"
    then 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)"
    then 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)" ..
  then show "\<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" ..
  then have "P x y" ..
  then show "\<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
  then show ?thesis by blast
qed

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


text {* Isar: moreover/ultimately *}

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


text {* Isar: also/finally *}

lemma right_inverse:
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
  fixes inv :: "'a \<Rightarrow> 'a"    ("(_\<^sup>-)" [1000] 999)
  fixes one :: 'a    ("\<one>")

  assumes assoc: "\<And>x y z. (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
  assumes left_inv: "\<And>x. x\<^sup>- \<cdot> x = \<one>"
  assumes left_one: "\<And>x. \<one> \<cdot> x = x"

  shows "x \<cdot> x\<^sup>- = \<one>"
proof -
  have "x \<cdot> x\<^sup>- = \<one> \<cdot> (x \<cdot> x\<^sup>-)" by (simp only: left_one)
  also have "\<dots> = \<one> \<cdot> x \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>- \<cdot> x \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (x\<^sup>- \<cdot> x) \<cdot> x\<^sup>-" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> \<one> \<cdot> x\<^sup>-" by (simp only: left_inv)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> (\<one> \<cdot> x\<^sup>-)" by (simp only: assoc)
  also have "\<dots> = (x\<^sup>-)\<^sup>- \<cdot> x\<^sup>-" by (simp only: left_one)
  also have "\<dots> = \<one>" by (simp only: left_inv)
  finally show ?thesis .
qed

-- "mixed operators"
lemma "1 < (5::nat)"
proof -
  have "1 < Suc 1" by simp
  also have "Suc 1 = 2" by simp
  also have "2 \<le> (5::nat)" by simp
  finally show ?thesis .
qed
  
-- "substitution"
lemma blah
proof -
  have "x + 2*y = (0::nat)" sorry
  also have "2*y = x" sorry
  also have "(0::nat) \<le> 2*c" sorry
  also have "c = d div 2" sorry
  also have "d = 2 * x" sorry  
  finally have "x + x \<le> 2 * x " by simp
oops
    
-- "antisymmetry"
lemma blub
proof -
  have "a < (b::nat)" sorry
  also have "b < a" sorry
  finally show blub .
qed


-- "notE as trans"

thm notE
declare notE [trans]

lemma blub
proof -
  have "\<not>P" sorry
  also have "P" sorry
  finally show blub .
qed


-- "monotonicity"

lemma "a+b \<le> 2*a + 2*(b::nat)" 
proof -
  have "a + b \<le> 2*a + b" by simp
  also have "b \<le> 2*b" by simp
  finally show "a+b \<le> 2*a + 2*b" by simp
qed

lemma "a+b \<le> 2*a + 2*(b::nat)" 
proof -
  have "a + b \<le> 2*a + b" by simp
  also have "b \<le> 2*b" by simp
  also have "\<And>x y. x \<le> y \<Longrightarrow> 2 * a + x \<le> 2 * a + y" by simp
  ultimately show "a+b \<le> 2*a + 2*(b::nat)" .
qed
  

declare ring_simps [simp]

lemma "(a+b::int)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
proof -
       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>" by simp
  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b" by (simp add: numeral_2_eq_2)
  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b" by (simp add: numeral_2_eq_2)
  finally show ?thesis by simp
qed

end