theory Demo85 imports Main begin

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

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


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

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

text{*A manual proof in set theory:*}

thm equalityI subsetI
thm UnI1 UnI2 UnE

lemma "A \<union> B = B \<union> A" 
apply(rule equalityI)
 apply(rule subsetI)
 apply(erule UnE)
  apply(rule UnI2)
  apply(assumption)
 apply(rule UnI1)
 apply(assumption)
 apply(rule subsetI)
apply(erule UnE)
 apply(rule UnI2)
 apply(assumption)
apply(rule UnI1)
apply(assumption)
done


text{* Most simple proofs in set theory are automatic: *}

lemma "-(A \<union> B) = (-A \<inter> -B)"
  by blast

lemma "{x. P x \<and> Q x} = {x. P x} \<inter> {x. Q x}"
  by blast


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


end