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


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

(* congruences *)

(* 2.1: fun_cong *)
(*A paper-and pencil proof looks as follows:

       ________ refl
  f=g  f(x)=f(x)
       _________subst
       f(x) = g(x)

  Using backwards reasoning, this leads to a proof starting as follows:*)

Goal "f=g \\<Longrightarrow> f(x) = g(x)";
br subst 1;
back();
back();
back();
back();
back();
back();
(*Isabelle doesn't find the unifier*)
(*back();*)

(*There are several ways of circumventing the problem:*)

(*using etac:*)
Goal "f=g \\<Longrightarrow> f(x) = g(x)";
be subst 1;
br refl 1;
qed "my_fun_cong";

(*using res_inst_tac*)
Goal "f=g \\<Longrightarrow> f(x) = g(x)";
by(res_inst_tac [("t","g")] subst 1);
ba 1;
br refl 1;

Goal "f=g \\<Longrightarrow> f(x) = g(x)";
by (res_inst_tac [("P","%h. f x = h x")] subst 1);
ba 1;
br refl 1;

(*using RS*)
val [pr] = goal thy "f=g \\<Longrightarrow> f(x) = g(x)";
br (pr RS subst) 1;
br refl 1;

(* 2.2: arg_cong *)
Goal "x=y \\<Longrightarrow> f(x) = f(y)"; 
be subst 1;
br refl 1;
qed "my_arg_cong";


(*                                  *)
(* Exercise 3 --------------------  *)
(*                                  *)

(* Derive some rules form the lecture *)

(* 3.1 *)
Goal "s=t \\<Longrightarrow> t=s";
be subst 1;
br refl 1;
qed "my_sym";

(* 3.2 *)
Goalw [True_def] "True";
br refl 1;
qed "my_TrueI";

(* 3.3 *)
val [prem] = Goalw [All_def] "(!!x. P x) \\<Longrightarrow> ALL x. P x";
All_def;
br ext 1;
br eqTrueI 1;
br prem 1;
qed "my_allI";

(* 3.4*)
Goalw [False_def] "False \\<Longrightarrow> P";
be spec 1;
qed "my_FalseE";

(* 3.5 *)
(*Help by Alex Schimpf on 19.3.10: It is important to use Goal here,
    not "goal thy" because thy may deviate from the current context*)
Goal "\\<lbrakk> P; Q \\<rbrakk> \\<Longrightarrow> (P \\<and> Q) ";
by(rewtac and_def);
br my_allI 1;
br impI 1;
br mp 1;
br mp 1;
ba 1;
ba 1;
ba 1;
qed "my_conjI";

(*A bit of playing around to see the simpset etc.*)
simpset();
Simp_tac;
simp_tac;
the_context();
(*Note: Really big context!*)
thy;
(*Note: thy is just {ProtoPure, Pure, CPure, HOL}, not identical to the_context()*)
context;
theory;
the_context();
(*Note: context just contains {ProtoPure, Pure, CPure, HOL}.*)


(*                                  *)
(* Exercise 4 --------------------  *)
(*                                  *)

(* 4.1 *)
Goal "(if False then A else B) = B";
set trace_simp;
trace_simp := true;
by (Simp_tac 1);
(*you should look at the buffer *isabelle-trace*.*)
print_ss;
print_ss (simpset());
(*you should look at the buffer *isabelle-response*.*)
qed "ex4_1";

(*If we keep the tracer on it will slow down and jam Isabelle*)
trace_simp := false;

(* 4.2 *)
(*impossible:
val [p1] = Goal "\\<lbrakk>(~E) \\<Longrightarrow> B ~= B'\\<rbrakk> \\<Longrightarrow> (if E then A else B) ~= (if E then A else B')";
so ex4_2 does not hold in general*)

(* 4.3 *)
Goal "\\<lbrakk> A ~= A';B ~= B'\\<rbrakk> \\<Longrightarrow> (if E then A else B) \\<noteq> (if E then A' else B')";
by (Auto_tac);
qed "ex4_3";

(* 4.4 *)
Goal "f (if E then x else y) = (if E then (f x) else (f y))";
by (Simp_tac 1);
qed "ex4_4";

(* 4.5 *)
Goal "\\<lbrakk>P\\<or>Q; P=(~Q)\\<rbrakk>  \\<Longrightarrow> (if P then A else B) = (if Q then B else A)";
by (Asm_simp_tac 1);
qed "ex4_5";

(* 4.6 *)
val [p1,p2] = Goal "\\<lbrakk>(~E) \\<Longrightarrow> B \\<noteq> B';  ~E\\<rbrakk> \\<Longrightarrow> (if E then A else B) \\<noteq> (if E then A else B')";
by (Simp_tac 1);
br conjI 1;
br p2 1;
br impI 1;
be p1 1;
qed "ex4_6";

(* 4.7 *)
(*impossible*)
(*Goal "A\\<or>B \\<Longrightarrow> (if P then A else B)";*)
(*ex4_7 does not hold in general*)



(*                                  *)
(* Exercise 5 --------------------  *)
(*                                  *)
(*context (theory "Set");*)
(*Solution suggested by Muhammad Irfan Nazir*)
(* 6.1 *)
Goal "P a \\<Longrightarrow> a \\<in> Collect P";
by (rewrite_goals_tac [mem_Collect_eq RS eq_reflection]);
ba 1;
qed "ex5_1";

(* 5.2 *)
Goal "a \\<in> Collect P \\<Longrightarrow> P a ";
by (rewrite_goals_tac [mem_Collect_eq RS eq_reflection]);
ba 1;
qed "ex5_2";

(* 5.3 *)
Goal "(!x. (x \\<in> A) = (x \\<in> B)) \\<Longrightarrow> A = B";
br (Collect_mem_eq RS subst) 1;
br (Collect_mem_eq RS subst) 1;
back();
back();
by (res_inst_tac [("f","Collect")] arg_cong 1);
br ext 1;
be allE 1;
ba 1;
(*not nice because it uses back()*)

(*alternative using box_equals*)
Goal "(!x. (x \\<in> A) = (x \\<in> B)) \\<Longrightarrow> A = B";
br box_equals 1;
br Collect_mem_eq 2;
br Collect_mem_eq 2;
by (res_inst_tac [("f","Collect")] arg_cong 1);
br ext 1;
be allE 1;
ba 1;
qed "ex5_3";


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

(* 6.1 *)
Goalw [subset_def] "\\<lbrakk>\\<forall>x\\<in>A. x \\<in> B; \\<forall>x\\<in>B. x \\<in> C \\<rbrakk> \\<Longrightarrow> \\<forall>x\\<in>A. x \\<in> C";
by (Blast_tac 1);
qed "ex6_1";

(* 6.2 *)
Goal "A \\<inter> B \\<subseteq> A";
by (Fast_tac 1);
qed "ex6_2";

(* 6.3 *)
Goal "(A=B) = ((Pow A) = (Pow B))";
by (Fast_tac 1);
qed "ex6_3";

(* 6.4 *)
Goal "(A \\<subseteq> B) = (A \\<in> Pow B)";
by (Fast_tac 1);
qed "ex6_4";

(* 6.5 *)
Goalw [insert_def] "X \\<subseteq> insert x X";
by (Auto_tac);
qed "ex6_5";

(* 6.6 *)
Goal "\\<lbrakk>X \\<subseteq> Y;  X \\<noteq> {}\\<rbrakk> \\<Longrightarrow> (Y - X) \\<subset> Y";
by (Fast_tac 1);
qed "ex6_6";

(* 6.7 *)
Goal "x\\<noteq>y \\<Longrightarrow> {x} \\<noteq> {y,x}";
by (Fast_tac 1);
qed "ex6_7";

(* 6.8 *)
Goalw [Bex_def] "\\<lbrakk>S = {a,b}; a \\<noteq> b\\<rbrakk> \\<Longrightarrow> (\\<exists>A\\<in>Pow S. (\\<exists>B\\<in>Pow S. (\\<exists>C\\<in>Pow S. (\\<exists>D\\<in>Pow S.
                                       A \\<noteq> B \\<and> A \\<noteq> C \\<and> A \\<noteq> D \\<and> 
                                       B \\<noteq> C \\<and> B \\<noteq> D \\<and> C \\<noteq> D ))))";
by (res_inst_tac [("x","{}")] exI 1);
by (asm_simp_tac (HOL_ss addsimps []) 1);
br conjI 1;
br PowI 1;
by (Fast_tac 1);
by (res_inst_tac [("x","{a}")] exI 1);
br conjI 1;
br PowI 1;
by (Fast_tac 1);
by (res_inst_tac [("x","{b}")] exI 1);
by (Auto_tac);
qed "ex6_8";

(* 6.9 *)
Goal "range (%x. False) = {False}";
by (Fast_tac 1);
qed "ex6_9";

(* 6.10 *)
Goal "f`{} = {}";
by (Fast_tac 1);
qed "ex6_10";

(* 6.11 *)
Goal "A \\<noteq> {} \\<Longrightarrow> ((%x. True)`A) = {True}";
by (Fast_tac 1);
qed "ex6_11";

(* 6.12 *)
Goal "\\<Union>{} = {}";
by (Blast_tac 1);
qed "ex6_12";


(*a bit of playing around with opening structures*)
use_thy "FinSet";

open FinSet;
Fin.defs;
Fin.induct;
open Fin;
(*now Fin has been opened and we can simply do \\<dots>*)
defs;
induct;

lfp_unfold;


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

(*Following solution essentially due to Paul Hankes-Drielsma*)
Goalw Fin.defs "{0,1} : Fin {0,1,2}";
by (stac lfp_unfold 1);
by (stac lfp_unfold 2);
by (stac lfp_unfold 3);
by (Blast_tac 4);
br mono 1;
br mono 1;
br mono 1;
qed "ex8";

(*Shorter solution by Hauke Strasdat: *)
Goal  "{0,1}:Fin{0,1,2}";
br Fin.insertI 1;
auto();
br Fin.insertI 1;
auto();
br Fin.emptyI 1;
qed "ex8_hauke";


open Finites;
(*Careful: since FinSet and Fin were opened above, we use the full
  names for all components of Finites, to be sure that we address the
  correct entities*)
thm "Finites.defs";

(* just typing
Finites.defs;
will not do, since the ML binding mechanism has not been preset for
  that. *)

Finites.elims;
Finites.induct;

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

inj_on_def;

Goalw [inj_on_def] "EX (f::(ind=>ind)) x y. (ALL w. f w ~= x) \\<and> 
(ALL w. f w ~= y) \\<and> x ~= y \\<and> (inj f)";
by (res_inst_tac [("x","Suc_Rep o Suc_Rep")] exI 1);
by (res_inst_tac [("x","Zero_Rep")] exI 1);
by (res_inst_tac [("x","Suc_Rep Zero_Rep")] exI 1);
val inj_Suc_Rep = thm "inj_Suc_Rep";
val Suc_Rep_not_Zero_Rep = thm "Suc_Rep_not_Zero_Rep";
by (asm_simp_tac (HOL_ss addsimps [inj_Suc_Rep,Suc_Rep_not_Zero_Rep,o_apply,inj_eq]) 1);
by (asm_simp_tac (HOL_ss addsimps [Suc_Rep_not_Zero_Rep,not_sym]) 1);
by (Blast_tac 1);
qed "ex9";



nat_induct;
wf_pred_nat;
less_linear;
Suc_less_SucD;
add_0_right;
add_ac;
mult_ac;
zadd_ac;
zmult_ac;
inj_on_def;
(*Why do I need this and not for the others?*)
val acyclic_def = thm "acyclic_def";
acyclic_def;


(*                                  *)
(* Exercise 10 --------------------  *)
(*                                  *)
use_thy "Iterate";

Goal "iterate (Suc (Suc 0)) Suc (Suc 0) = ?x";
auto();
qed "ex10_1";

Goal "iterate (Suc (Suc (Suc 0))) (Suc o Suc) 0 = ?x";
auto();
qed "ex10_2";

(*Look at nat_rec_0 and nat_rec_Suc*) 
nat_rec_0;
nat_rec_Suc;
nat.recs;


(*                                  *)
(* Exercise 11 --------------------  *)
(*                                  *)

Goal "\\<lbrakk>c = (Suc 0); g = (%n s. ((Suc n) * s))\\<rbrakk> \\<Longrightarrow> 
nat_rec c g 0 = Suc 0"; 
auto();
qed "ex11_1";


Goal "\\<lbrakk>c = (Suc 0); g = (%n s. ((Suc n) * s))\\<rbrakk> \\<Longrightarrow> 
nat_rec c g (Suc (Suc (Suc (Suc 0)))) = 24";
auto();
qed "ex11_2";

(*or, if you prefer to write it out:*)
Goal "\\<lbrakk>c = (Suc 0); g = (%n s. ((Suc n) * s))\\<rbrakk> \\<Longrightarrow> 
nat_rec c g (Suc (Suc (Suc (Suc 0)))) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (0))))))))))))))))))))))))";
auto();

Goal "\\<lbrakk>c = (Suc 0); g = (%n s. ((Suc n) * s))\\<rbrakk> \\<Longrightarrow> 
nat_rec c g 13 = ?x";
auto();
qed "ex11_3";
(*result: 6227020800*)


(*                                  *)
(* Exercise 12 --------------------  *)
(*                                  *)

Goal "sumup = (%f. (nat_rec 0 (%n s. (f (n+1)) + s))) \\<Longrightarrow> 
      sumup (%i. i) 5 = 15";
auto();
qed "ex12_1";

Goal "sumup = (%f. (nat_rec 0 (%n s. (f (n+1)) + s))) \\<Longrightarrow> 
      sumup (%i. i+2) 6 = 33";
auto();
qed "ex12_2";

nat.recs;
Goal "sumup = (%f. (nat_rec 0 (%n s. (f (n+1)) + s))) \\<Longrightarrow> 
      (sumup (%i. 2*i)) m  = m * (m+1)";
by (res_inst_tac [("n","m")] nat_induct 1);
auto();
qed "ex12_3";