theory week11A_demo imports Main begin

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

text {* Motivation *}

lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
by blast  

value "True \<longrightarrow> False" 
value "False \<or> \<not> True"
  
lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
  (* apply style *)
  sorry
  
lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
  (* isar style *)
  sorry
  
-- ----------------------------------------
 
text {* Isar *}

lemma "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> A \<and> B"
  sorry

lemma 
  assumes A: "A"
  assumes B: "B"
  shows "A \<and> B"
  sorry


lemma "(x::nat) + 1 = 1 + x"
  sorry
  
  
  
-- ------------------------------------------------------------------

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


text{* fix *}

lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P (f x)"
  sorry

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"
  sorry  
  
text {* obtain *}

lemma assumes Pf: "\<exists>x. P (f x)" shows "\<exists>y. P y"
  sorry

lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
  sorry

lemma 
  assumes A: "\<forall>x y. P x y \<and> Q x y" 
  shows "\<exists>x y. P x y \<and> Q x y"
  sorry (* apply style *)

  
text {* moreover *}

lemma "A \<and> B \<longrightarrow> B \<and> A"
  sorry


thm mono_def 
thm 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)"
  sorry


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

 
lemma "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
  apply(rule conjI)
  proof - 
  assume A thus A .
  assume B thus B .
  qed

end