(* CSMR WS10/11 - Sheet 7 *)
(* *)
(* Exercise 1 -------------------- *)
(* *)
use_thy "RED";
(*Essentially the solution by Konrad Anton*)
(*A proper beta-reduction step consists of several applications of the
congruences appr, appl and epsi, followed by exactly one application
of beta. We will add those rules to the safe introduction rules*)
val RED_cs = empty_cs addSIs [beta,appr,appl,epsi];
(*We now write a tactic which does one proper beta-reduction step*)
fun proper_beta_step i =
(fast_tac RED_cs i);
(*We can use this to automate part of the beta-reduction process, as
seen in the example below:*)
Goal "S^K^K --> ?x";
by (rewrite_goals_tac [S_def,K_def]);
br trans 1;
by (proper_beta_step 1);
br trans 1;
by (proper_beta_step 1);
br trans 1;
by (proper_beta_step 1);
br trans 1;
by (proper_beta_step 1);
by (fold_goals_tac [I_def]);
br refl 1;
(*We can now automate further by including one application of
transitivity*)
fun trans_then_beta i = (rtac trans i) THEN (proper_beta_step i);
(*Same example but with further automation*)
Goal "S^K^K --> ?x";
by (rewrite_goals_tac [S_def,K_def]);
by (trans_then_beta 1);
by (trans_then_beta 1);
by (trans_then_beta 1);
by (trans_then_beta 1);
by (fold_goals_tac [I_def]);
br refl 1;
(*in case further expansion of the current subgoal by transitivity
followed by a proper beta step does not work, since the subgoal
already represents a beta-normal form, we want to apply reflexivity to
the goal. Moreover, it would be nice if just before concluding,
fold_goals_tac was applied*)
fun beta_star_fold_refl i = (REPEAT (trans_then_beta i))
THEN (fold_goals_tac [S_def, K_def, I_def])
THEN (rtac refl i);
(*Same example*)
Goal "S^K^K --> ?x";
by (rewrite_goals_tac [S_def,K_def]);
by (beta_star_fold_refl 1);
(*Do the unfolding at the beginning automatically*)
fun reduce_to_normal i = (rewrite_goals_tac [S_def, K_def, I_def])
THEN (beta_star_fold_refl i);
(*Same example, now fully automatic*)
Goal "S^K^K --> ?x";
by (reduce_to_normal 1);
(*now the actual exercise 1*)
Goal "S^K^K^S^K^S^I^K -->?t";
by (reduce_to_normal 1);
qed "ex1_1";
Goal "S^I^K^S^K^I^S^S -->?t";
by (reduce_to_normal 1);
qed "ex1_2";