(* Pearls of CSMR Aquila II Semestre A.A.2009/2010 *)

(*Some first steps in Isabelle*)
conjI;

goal thy "A \\<longrightarrow> B \\<longrightarrow> A";
by (rtac impI 1);
by (rtac impI 1);
by (atac 1);
qed "aba";

(*Meta-variables*)
goal thy "A \\<and> B \\<longrightarrow> A";
br impI 1;
br conjunct1 1;
ba 1;
qed "conjunct1thm";


(*                                  *)
(* Exercise 1 --------------------  *)
(*                                  *)

(* 1.1 *)
goal thy "A\\<and> B \\<longrightarrow> B\\<and> A";
br impI 1;
br conjI 1;
br conjunct1 2;
br conjunct2 1;
ba 2;
ba 1;
qed "ex1_1";

(* 1.2 *)
goal thy "A\\<and> B \\<longrightarrow> B \\<or> A";
br impI 1;
br disjI1 1;
br conjunct2 1;
ba 1;
qed "ex1_2";

(* 1.3 *)
goal thy "A \\<or> B \\<longrightarrow> B \\<or> A";
br impI 1;
br disjE 1;
ba 1;
(* 2 different cases for "or" *)
br disjI2 1;
ba 1;
br disjI1 1;
ba 1;
qed "ex1_3";

(* 1.4 *)
goal thy "(A\\<and> B)\\<and> C \\<longrightarrow> A\\<and> (B\\<and> C)";
br impI 1;
br conjI 1;
br conjunct1 1;
br conjunct1 1;
ba 1;
br conjI 1;
br conjunct2 1;
br conjunct1 1;
ba 1;
br conjunct2 1;
ba 1;
qed "ex1_4";

(* 1.5 *)
goal thy "(A \\<longrightarrow> B \\<longrightarrow> C) \\<longrightarrow> (A \\<longrightarrow> B)\\<longrightarrow> (A \\<longrightarrow> C)";
br impI 1;
br impI 1;
br impI 1;
br mp 1;
br mp 1;
ba 1;
ba 1;
br mp 1;
ba 1;
ba 1;
qed "ex1_5";

(* 1.6 *)
goal thy "(A \\<or> B)\\<and> (B \\<or> C) \\<longrightarrow> B \\<or> (A\\<and> C)";
br impI 1;
br disjE 1;
br conjunct1 1;
ba 1;
br disjE 1;
br conjunct2 1;
ba 1;
br disjI1 1;
ba 1;
br disjI2 1;
br conjI 1;
ba 1;
ba 1;
br disjI1 1;
ba 1;
qed "ex1_6";

(*Derived Rules*)
(*let's see what the type of goal is*)
goal;

(*The following is not very useful:*)
goal thy "P&Q \\<Longrightarrow> Q&P";
(*Note that the problem could be avoided here by using Goal, but in
  other situations that would not work.*)

(*Exception due to non-matching binding attempt
val [prem1,prem2] = goal thy "P&Q \\<Longrightarrow> Q&P";
*)

(*deriving commutativity of &*)
val [prem] = goal thy "P&Q \\<Longrightarrow> Q&P";
prem;
br conjI 1;
br conjunct2 1;
br prem 1;
br conjunct1 1;
br prem 1;
qed "conjComm";


(*Elimination tactic*)
Goal "A & B \\<longrightarrow> A";
br impI 1;
by (etac conjunct1 1);
qed;


(*                                  *)
(* Exercise 2 --------------------  *)
(*                                  *)

(* 2.1 *)
Goal "A \\<and> (B \\<and> C) \\<longrightarrow> (A \\<and> B) \\<and> C";
br impI 1;
be conjE 1;
be conjE 1;
br conjI 1;
br conjI 1;
ba 1;
ba 1;
ba 1;
qed "ex2_1";

(*For comparison, ex2_1 without using etac*)
(*without conjE*)
Goal "A \\<and> (B \\<and> C) \\<longrightarrow> (A \\<and> B) \\<and> C";
br impI 1;
br conjI 1;
br conjI 1;
br conjunct1 1;
ba 1;
br conjunct1 1;
br conjunct2 1;
ba 1;
br conjunct2 1;
br conjunct2 1;
ba 1;
qed;

(*with conjE but without etac*)
Goal "A \\<and> (B \\<and> C) \\<longrightarrow> (A \\<and> B) \\<and> C";
br impI 1;
br conjE 1;
ba 1;
by (rotate_tac 1 1);
br conjE 1;
ba 1;
br conjI 1;
br conjI 1;
ba 1;
ba 1;
ba 1;
qed;

(* 2.2 *)
Goal "(A \\<or> C) \\<and> (B \\<or> C) \\<longrightarrow> (A \\<and> B) \\<or> C";
br impI 1;
be conjE 1;
be disjE 1;
be disjE 1;
br disjI1 1;
br conjI 1;
ba 1;
ba 1;
br disjI2 1;
ba 1;
br disjI2 1;
ba 1;
qed "ex2_2";

allI;
spec;
exI;
exE;
(*                                  *)
(* Exercise 5 --------------------  *)
(*                                  *)

(* 5.1 *)
Goal "(ALL y. q(f(y))) \\<longrightarrow> (EX x. q(x))";
br impI 1;
br exI 1;
be spec 1;
qed "ex5_1";

(* 5.2 *)
Goal "(ALL x. p(x)) \\<or> (ALL x. q(x)) \\<longrightarrow> (ALL x. p(x) \\<or> q(x))";
br impI 1;
br allI 1;
be disjE 1;
br disjI1 1;
br spec 1;
ba 1;
br disjI2 1;
br spec 1;
ba 1;
qed "ex5_2";

(* 5.3
An invalid statement
Goal "(ALL x. p(x) \\<or> q(x)) \\<longrightarrow> (ALL x. q(x)) \\<or> (ALL x. p(x))";
*)

(* 5.4 *)
Goal "(ALL x. p(x)) \\<and> (ALL x. q(x)) \\<longrightarrow> (ALL x. p(x) \\<and> q(x))";
br impI 1;
br allI 1;
be conjE 1;
br conjI 1;
be spec 1;
be spec 1;
qed "ex5_4";

(* 5.5
An invalid statement
Goal "(ALL x. EX y. p(x,y)) \\<longrightarrow> (EX y. ALL x. p(x,y))";
*)

(* 5.6 *)
Goal "(EX x. ALL y. p(x,y)) \\<longrightarrow> (ALL y. EX x. p(x,y))";
br impI 1;
be exE 1;
br allI 1;
br exI 1;
br spec 1;
ba 1;
qed "ex5_6";

(* A similar solution: *)
Goal "(EX x. ALL y. p(x,y)) \\<longrightarrow> (ALL y. EX x. p(x,y))";
br impI 1;
br allI 1;
be exE 1;
br exI 1;
br spec 1;
ba 1;
qed "ex5_6_old";

(* 5.7 *)
Goal "(ALL x. p(x)) \\<longrightarrow> (ALL x. p(g(x)))";
br impI 1;
br allI 1;
be spec 1;
qed "ex5_7";


(*Forward resolution*)
[conjunct2,conjunct1] MRS conjI;


(*                                  *)
(* Exercise 6 --------------------  *)
(*                                  *)

Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; 
br impI 1;
br ([conjunct2,conjunct1] MRS conjI) 1;
ba 1;
ba 1;
qed "ex6";

(*example where rule list is "too" short*)
[conjunct2] MRS conjI;

(*Another combination*)
([conjunct2,conjunct1] MRS conjI) RS impI;


(*                                  *)
(* Exercise 7 --------------------  *)
(*                                  *)

Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
br (([conjunct2,conjunct1] MRS conjI) RS impI) 1;
ba 1;
ba 1;
qed "ex7";

(*                                  *)
(* Exercise 8 --------------------  *)
(*                                  *)

(* 8_sym *)
(*using Goal so that the premise is available and combine this with
  etac makes Isabelle find the right unifier straightaway*) 
Goal "x=y \\<Longrightarrow> y=x";
be subst 1;
br refl 1;
qed "ex8_sym";
(*there are several alternative ways of doing this, but this will be
    done in a later exercise.*)


(* 8_trans *)
Goal "\\<lbrakk>x=y;y=z\\<rbrakk> \\<Longrightarrow> x=z";
br subst 1;
ba 1;
ba 1;
(*happens to be very easy. No reason to try more sophisticated things*)
qed "ex8_trans";

(*Alternative: using a trick to get hold of the assumption. But thanks
  to Goal, this is not really needed.*)
val [p1,p2] = goal thy "\\<lbrakk>x=y;y=z\\<rbrakk> \\<Longrightarrow> x=z";
br mp 1;
br mp 1;
br impI 1;
br impI 1;
br p1 2;
br p2 2;
br subst 1;
ba 1;
ba 1;
qed;

(*Another alternative*)
val [p1,p2] = goal thy "\\<lbrakk>x=y;y=z\\<rbrakk> \\<Longrightarrow> x=z";
br (p2 RS subst) 1;
br p1 1;
qed;


(*                                  *)
(* Exercise 9 -------------------  *)
(*                                  *)

Goal "s(s(s(s(s(zero))))) = five \\<and> p(zero) \\<and> (ALL x. p(x) \\<longrightarrow> p(s(x))) \\<longrightarrow> p(five)";
br impI 1;
be conjE 1;
be conjE 1;
be subst 1;
br mp 1;
by (res_inst_tac [("x","s(s(s(s(zero))))")] spec 1);
ba 1;
br mp 1;
by (res_inst_tac [("x","s(s(s(zero)))")] spec 1);
ba 1;
br mp 1;
by (res_inst_tac [("x","s(s(zero))")] spec 1);
ba 1;
br mp 1;
by (res_inst_tac [("x","s(zero)")] spec 1);
ba 1;
br mp 1;
by (res_inst_tac [("x","zero")] spec 1);
ba 1;
ba 1;
qed "ex9";

(*alternative solution without using res_inst_tac*)
Goal "s(s(s(s(s(zero))))) = five \\<and> p(zero) \\<and> (ALL x. p(x) \\<longrightarrow> p(s(x))) \\<longrightarrow> p(five)";
br impI 1;
be conjE 1;
be conjE 1;
be subst 1;
br mp 1;
br mp 2;
br mp 3;
br mp 4;
br mp 5;
ba 6;
be spec 5;
be spec 4;
be spec 3;
be spec 2;
be spec 1;
qed "ex9_alternative";

(*                                  *)
(* Exercise 15 --------------------  *)
(*                                  *)

(* using res_inst_tac *)
Goal "x=y \\<Longrightarrow> y=x";
subst;
by (res_inst_tac [("P","%u. u=x")] subst 1);
ba 1;
br refl 1;
qed "ex15_1";

(* using MRS, even shorter *)
val [prem] = goal thy "x=y \\<Longrightarrow> y=x";
by (rtac ([prem,refl] MRS subst) 1);
qed "ex15_2";

(* using THEN *)
Goal "x=y \\<Longrightarrow> y=x";
by ((rtac subst 1) THEN (atac 1) THEN (rtac refl 1));
qed "ex15_3";