theory tut2
imports Main

begin

(* Solutions using explicit instantiation and avoiding introduction
   of meta-variables
*)
   
lemma one: "(\<forall> x. P x \<longrightarrow> Q) \<longrightarrow> (\<exists> x. P x \<longrightarrow> Q)"  
apply (rule impI)
apply (rule_tac x="a" in exI)
apply (erule_tac x="a" in allE)
apply assumption
done

lemma two: "\<not>(\<exists> x. P x) \<Longrightarrow> \<forall> x. \<not>P x" 
apply (rule allI)
apply (rule notI)
apply (erule notE)
apply (rule_tac x="x" in exI)
by assumption

lemma three: "\<not>(\<forall> x. P x) \<Longrightarrow> \<exists> x. \<not>P x"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (rule_tac x="x" in exI)
by assumption


(* The next solutions exploit meta-variables that avoid the explicit
   instantiations of variables in the inference rules.  Unification calculates
   appropriate instantiations of the meta-variables automatically.  

   These solutions are presented for your interest.

*)
  
(* Observe here in lemma one_a:

   - After the erule allE, the meta-variable introduced has a function type
     and is applied to the variable x, bound by a meta-forall quantifier.

     Why?  Well isabelle instantiates meta-variables using capture-avoiding
     substitution.  Here the meta-variable introduced can be a function
     that then makes use of the variable x.  

  - In the 'apply assumption' step, Isabelle uses Higher-order unification to
    unify terms  ?f x  and x, yielding the substitution [(\<lambda>y.y) / ?f].
    Higher-order unification has the lambda calculus
    beta rule built in, so substituting '\<lambda>y.y' for ?f yields '(\<lambda>y.y) x' which
    is equal by the beta-rule to x.
*)

lemma one_a: "(\<forall> x. P x \<longrightarrow> Q) \<longrightarrow> (\<exists> x. P x \<longrightarrow> Q)"  
apply (rule impI)
apply (rule exI)
apply (erule allE)
apply assumption
done

lemma two_a: "\<not>(\<exists> x. P x) \<Longrightarrow> \<forall> x. \<not>P x" 
apply (rule allI)
apply (rule notI)
apply (erule notE)
apply (rule exI)
by assumption

lemma three_a: "\<not>(\<forall> x. P x) \<Longrightarrow> \<exists> x. \<not>P x"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (rule ccontr)
apply (erule notE)
apply (rule exI)
by assumption


end