(* CSMR WS10/11 - Sheet 10 *)
(* Set isabelle logic to: HOL *)
(* *)
(* Exercise 2 -------------------- *)
(* *)
Goal "x=y \\ x==y";
be eq_reflection 1;
qed "ex2_1";
(*the eq_reflection rule effectively enforces an identification of the
meta and object equalities.*)
val [pr] = goal thy "x==y \\ x=y";
bw pr;
br refl 1;
qed "ex2_2";
(*This one would have also worked in FOL. In general, meta-level
equalities are stronger than object-level equalities.*)
(*Alternative solutions to ex2_2, together with a discussion of some
Isabelle subtleties.*)
(*The following is a proof which uses rewrite_goals_tac, but it is
completely irrelevant which rewrite rule is used, because
apparently, the non-hidden assumption is always added to the rewrite
rules.*)
Goal "x==y \\ x=y";
by (rewrite_goals_tac [excluded_middle,mp]);
br refl 1;
(*Alex Schimpf wrote: actually the manual says that "Goal" 'tries to be smart
in handling meta-hypotheses'. Maybe this is part of this 'smart' mechanism.
It is obvious that premises of the form "e == e'" are automatically added
to the 'defs' list of rewrite_goals_tac, since it only handles meta level
equations\\ therefore the following attempt, where the premise is an
object-level identity, does not work: *)
Goal "x=y \\ x=y";
by (rewrite_goals_tac [excluded_middle,mp]);
(*same as previous level.*)
(*Strangely, the list must not be empty though.*)
Goal "x==y \\ x=y";
by (rewrite_goals_tac []);
(*same as previous level.*)
(*Alex wrote: probably before rewrite_goals_tac is applied there is an
optimisation like 'if defs *is empty* then *do nothing*'.
Since the *magic* of Goal is not really documented, it is not obvious
why this is implemented in this way.*)
(*If the asusmption is hidden, it does not work*)
val [pr] = goal thy "x==y \\ x=y";
by (rewrite_goals_tac [excluded_middle,mp]);
(*same as previous level.*)
(*Alex wrote: On the other hand if one does not want to have this
*smart* mechanism, he just have to use the normal 'goal', because it
does not have any *smart* optimasations like 'Goal'.
Therefore using rewrite_goals_tac with 'goal' does not apply any
*magic* steps to the prove state.
But of course it works when you make the hidden assumption explicit:*)
val [pr] = goal thy "x==y \\ x=y";
by (rewrite_goals_tac [excluded_middle,pr]);
br refl 1;
(*End of Exercise 2*)
(*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 following line can cause trouble if there is an exercise using
<=. In order to understand "<" and "<=", the context has to be
sufficiently big and contain the theory "Orderings".
The following line makes the context smaller and removes theory "Orderings".*)
(*context (theory "HOL");*)
the_context();
(*Note: context just contains {ProtoPure, Pure, CPure, HOL}.*)
(* *)
(* Exercise 3 -------------------- *)
(* *)
(* 3.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 "ex3_1";
(*If we keep the tracer on it will slow down and jam Isabelle*)
trace_simp := false;
(* 3.2 *)
(*does not hold in general*)
Goal "(if False then A else B) \\ A";
(* 3.3 *)
val [pr] = Goal "\\~E \\ B = B'\\ \\ (if E then A else B) = (if E then A else B')";
by (Simp_tac 1);
br impI 1;
be pr 1;
qed "ex3_3";
(* 3.4 *)
(*impossible:
val [p1] = Goal "\\(~E) \\ B ~= B'\\ \\ (if E then A else B) ~= (if E then A else B')";
so ex3_4 does not hold in general*)
(* 3.5 *)
Goal "\\ A ~= A';B ~= B'\\ \\ (if E then A else B) \\ (if E then A' else B')";
by (Auto_tac);
qed "ex3_5";
(* 3.6 *)
Goal "(if E then A else B) = (if (~E) then B else A)";
by (Simp_tac 1);
qed "ex3_6";
(* 3.7 *)
Goal "f (if E then x else y) = (if E then (f x) else (f y))";
by (Simp_tac 1);
qed "ex3_7";
(* 3.8 *)
(*impossible*)
(*Goal "\\(P\\Q)\\ \\ ((if P then A else B) = (if Q then B else A))";*)
(*ex3_8 does not hold in general*)
(* 3.9 *)
Goal "\\P\\Q; P=(~Q)\\ \\ (if P then A else B) = (if Q then B else A)";
by (Asm_simp_tac 1);
qed "ex3_9";
(* 3.10 *)
val [p1,p2] = Goal "\\(~E) \\ B \\ B'; ~E\\ \\ (if E then A else B) \\ (if E then A else B')";
by (Simp_tac 1);
br conjI 1;
br p2 1;
br impI 1;
be p1 1;
qed "ex3_10";
(* 3.11 *)
Goal "(if R then A else B) \\ A\\B";
by (res_inst_tac [("Q","R")] (excluded_middle RS disjE) 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "ex3_11";
(* 3.12 *)
(*impossible*)
(*Goal "A\\B \\ (if P then A else B)";*)
(*ex3_12 does not hold in general*)
(* *)
(* Exercise 5 -------------------- *)
(* *)
(*Context has to contain theory "Orderings" so that "<" and "<=" will
be recognised.*)
(*context (theory "Orderings");*)
(* 5.1 *)
Goal "(x::'a::order) x<=y";
by (asm_simp_tac (HOL_ss addsimps [order_le_less]) 1);
qed "ex5_1";
(*the following helped in finding the solution. It works in this "context",
which includes orders, but it may not work in all "context"s. It
may happen that the constants "<" etc. are not recognised.*)
thms_containing ["op <=","op |","op <"];
thms_containing ["mono"];
order_less_le;
order_le_less;
(* 5.2 *)
Goal "\\(x::'a::order) <= y; y <= z; z <= x\\ \\ x = z \\ x = y";
by (Auto_tac);
qed "ex5_2";
qed "triple_antisym";
(* 5.3 *)
Goal "\\(x::'a::order) < y; y < z; z < x\\ \\ False";
by (Auto_tac);
qed "ex5_3";
qed "triple_order_less_not_sym";
(* 5.4 *)
Goalw [min_def] "min (x::'a::linorder) y = y \\ y <= x";
by (case_tac "x <= y" 1);
by (Auto_tac);
qed "ex5_4";
(* 5.5 *)
Goalw [min_def] "min (x::'a::linorder) y = min y x";
by (asm_simp_tac (HOL_ss addsimps [order_antisym,linorder_not_le]
addsplits [split_if]) 1);
br impI 1;
bd order_less_not_sym 1;
by (Asm_simp_tac 1);
qed "ex5_5";
(* 5.6 *)
Goalw [min_def] "min (x::'a::linorder) (min y z)= min (min x y) z";
by (Asm_simp_tac 1);
by (Auto_tac);
qed "ex5_6";
(* 5.7 *)
Goalw [mono_def] "mono (%x::'a::ord. y::'b::order)";
by (Blast_tac 1);
qed "ex5_7";
(* 5.8 *)
Goalw [mono_def] "mono (%x::'a::ord. x)";
by (Blast_tac 1);
qed "ex5_8";