doc-src/TutorialI/Misc/cond_rewr.thy

*** empty log message ***

(*<*)
theory cond_rewr = Main:;
(*>*)

text{*
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example
*}

lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
by(case_tac xs, simp, simp);

text{*\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
sequence of methods. Assuming that the simplification rule
@{term"(rev xs = []) = (xs = [])"}
is present as well,
*}

lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
(*<*)
by(simp);
(*>*)
text{*\noindent
is proved by plain simplification:
the conditional equation @{thm[source]hd_Cons_tl} above
can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
because the corresponding precondition @{term"rev xs ~= []"}
simplifies to @{term"xs ~= []"}, which is exactly the local
assumption of the subgoal.
*}
(*<*)
end
(*>*)