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 (rule iffI)
   apply (cases A)
    apply (rule disjI1)
    apply (erule impE)
     apply assumption
    apply assumption
   apply (rule disjI2)
   apply assumption
  apply (rule impI)
  apply (erule disjE)
   apply assumption
  apply (erule notE)
  apply assumption
  done
  
  
lemma "(A \<longrightarrow> B) = (B \<or> \<not>A)"
 proof (rule iffI)
   assume AimpB: "A\<longrightarrow>B"
   show "B \<or> \<not> A"
   proof (cases A)
     assume A: "A"
     from AimpB A have B:"B" by (rule impE) 
     from B show "B \<or> \<not>A" by (rule disjI1)
   next
     assume notA: "\<not> A"
     from notA show "B \<or> \<not>A" by (rule disjI2)
   qed
 next
   assume BA: "B \<or> \<not> A"
   show "A\<longrightarrow>B"
   proof (rule impI) 
     assume A: "A"
     from BA A show B
     proof (elim disjE) 
       assume B: "B"
       from B show B by assumption
       next
       assume notA: "\<not> A"
       from A notA show B by (elim notE)
     qed 
   qed
  qed
     
   
-- ----------------------------------------
 
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