ProgTutorial/Tactical.thy
changeset 551 be361e980acf
parent 544 501491d56798
child 552 82c482467d75
equal deleted inserted replaced
550:95d6853dec4a 551:be361e980acf
   241   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
   241   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
   242   tactic we are in the position to inspect every goal state in a proof. For
   242   tactic we are in the position to inspect every goal state in a proof. For
   243   this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
   243   this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
   244   internally every goal state is an implication of the form
   244   internally every goal state is an implication of the form
   245 
   245 
   246   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
   246   @{text[display] "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}
   247 
   247 
   248   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   248   where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are
   249   the subgoals. So after setting up the lemma, the goal state is always of the
   249   the subgoals. So after setting up the lemma, the goal state is always of the
   250   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
   250   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
   251   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
   251   "#C"}. Since the goal @{term C} can potentially be an implication, there is a
   252   ``protector'' wrapped around it (the wrapper is the outermost constant
   252   ``protector'' wrapped around it (the wrapper is the outermost constant
   253   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   253   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   254   as a @{text #}). This wrapper prevents that premises of @{text C} are
   254   as a @{text #}). This wrapper prevents that premises of @{text C} are
   255   misinterpreted as open subgoals. While tactics can operate on the subgoals
   255   misinterpreted as open subgoals. While tactics can operate on the subgoals
   256   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   256   (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
   257   @{term C} intact, with the exception of possibly instantiating schematic
   257   @{term C} intact, with the exception of possibly instantiating schematic
   258   variables. This instantiations of schematic variables can be observed 
   258   variables. This instantiations of schematic variables can be observed 
   259   on the user level. Have a look at the following definition and proof.
   259   on the user level. Have a look at the following definition and proof.
   260 *}
   260 *}
   261 
   261 
   864 lemma rule:
   864 lemma rule:
   865   shows "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> R (f x) (g y)"
   865   shows "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> R (f x) (g y)"
   866 sorry
   866 sorry
   867 
   867 
   868 text {* 
   868 text {* 
   869   and you want to apply it to the goal @{term "(t\<^isub>1 t\<^isub>2) \<le>
   869   and you want to apply it to the goal @{term "(t\<^sub>1 t\<^sub>2) \<le>
   870   (s\<^isub>1 s\<^isub>2)"}. Since in the theorem all variables are
   870   (s\<^sub>1 s\<^sub>2)"}. Since in the theorem all variables are
   871   schematic, we have a nasty higher-order unification problem and @{text rtac}
   871   schematic, we have a nasty higher-order unification problem and @{text rtac}
   872   will not be able to apply this rule in the way we want. For the goal at hand 
   872   will not be able to apply this rule in the way we want. For the goal at hand 
   873   we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
   873   we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
   874   similarly ``obvious'' instantiations for the other variables.  To achieve this 
   874   similarly ``obvious'' instantiations for the other variables.  To achieve this 
   875   we need to match the conclusion of 
   875   we need to match the conclusion of 
   897   for calculating the conclusion of a theorem (produced as @{ML_type cterm}).
   897   for calculating the conclusion of a theorem (produced as @{ML_type cterm}).
   898   An example of @{ML fo_rtac} is as follows.
   898   An example of @{ML fo_rtac} is as follows.
   899 *}
   899 *}
   900 
   900 
   901 lemma
   901 lemma
   902   shows "\<And>t\<^isub>1 s\<^isub>1 (t\<^isub>2::'a) (s\<^isub>2::'a). (t\<^isub>1 t\<^isub>2) \<le> (s\<^isub>1 s\<^isub>2)"
   902   shows "\<And>t\<^sub>1 s\<^sub>1 (t\<^sub>2::'a) (s\<^sub>2::'a). (t\<^sub>1 t\<^sub>2) \<le> (s\<^sub>1 s\<^sub>2)"
   903 apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
   903 apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
   904 txt{*\begin{minipage}{\textwidth}
   904 txt{*\begin{minipage}{\textwidth}
   905      @{subgoals [display]}
   905      @{subgoals [display]}
   906      \end{minipage}*}
   906      \end{minipage}*}
   907 (*<*)oops(*>*)
   907 (*<*)oops(*>*)
  1375   The rewriting inside terms requires congruence theorems, which
  1375   The rewriting inside terms requires congruence theorems, which
  1376   are typically meta-equalities of the form
  1376   are typically meta-equalities of the form
  1377 
  1377 
  1378   \begin{isabelle}
  1378   \begin{isabelle}
  1379   \begin{center}
  1379   \begin{center}
  1380   \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
  1380   \mbox{\inferrule{@{text "t\<^sub>1 \<equiv> s\<^sub>1 \<dots> t\<^sub>n \<equiv> s\<^sub>n"}}
  1381                   {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
  1381                   {@{text "constr t\<^sub>1\<dots>t\<^sub>n \<equiv> constr s\<^sub>1\<dots>s\<^sub>n"}}}
  1382   \end{center}
  1382   \end{center}
  1383   \end{isabelle}
  1383   \end{isabelle}
  1384 
  1384 
  1385   with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
  1385   with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
  1386   and so on. Every simpset contains only one congruence rule for each
  1386   and so on. Every simpset contains only one congruence rule for each
  1619 | "perm_list pi (x#xs) = (pi\<bullet>x)#(perm_list pi xs)"
  1619 | "perm_list pi (x#xs) = (pi\<bullet>x)#(perm_list pi xs)"
  1620 
  1620 
  1621 end
  1621 end
  1622 
  1622 
  1623 lemma perm_append[simp]:
  1623 lemma perm_append[simp]:
  1624   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1624   fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1625   shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
  1625   shows "((pi\<^sub>1@pi\<^sub>2)\<bullet>c) = (pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c))"
  1626 by (induct pi\<^isub>1) (auto) 
  1626 by (induct pi\<^sub>1) (auto) 
  1627 
  1627 
  1628 lemma perm_bij[simp]:
  1628 lemma perm_bij[simp]:
  1629   fixes c d::"nat" and pi::"prm"
  1629   fixes c d::"nat" and pi::"prm"
  1630   shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
  1630   shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
  1631 by (induct pi) (auto)
  1631 by (induct pi) (auto)
  1634   fixes c::"nat" and pi::"prm"
  1634   fixes c::"nat" and pi::"prm"
  1635   shows "pi\<bullet>((rev pi)\<bullet>c) = c"
  1635   shows "pi\<bullet>((rev pi)\<bullet>c) = c"
  1636 by (induct pi arbitrary: c) (auto)
  1636 by (induct pi arbitrary: c) (auto)
  1637 
  1637 
  1638 lemma perm_compose:
  1638 lemma perm_compose:
  1639 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1639 fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1640 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
  1640 shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>(pi\<^sub>1\<bullet>c)" 
  1641 by (induct pi\<^isub>2) (auto)
  1641 by (induct pi\<^sub>2) (auto)
  1642 text_raw {*
  1642 text_raw {*
  1643 \end{isabelle}
  1643 \end{isabelle}
  1644 \end{boxedminipage}
  1644 \end{boxedminipage}
  1645 \caption{A simple theory about permutations over @{typ nat}s. The point is that the
  1645 \caption{A simple theory about permutations over @{typ nat}s. The point is that the
  1646   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
  1646   lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
  1664   and so causes an infinite loop. There seems to be no easy way to reformulate 
  1664   and so causes an infinite loop. There seems to be no easy way to reformulate 
  1665   this rule and so one ends up with clunky proofs like:
  1665   this rule and so one ends up with clunky proofs like:
  1666 *}
  1666 *}
  1667 
  1667 
  1668 lemma 
  1668 lemma 
  1669 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1669 fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1670   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
  1670   shows "pi\<^sub>1\<bullet>(c, pi\<^sub>2\<bullet>((rev pi\<^sub>1)\<bullet>d)) = (pi\<^sub>1\<bullet>c, (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>d)"
  1671 apply(simp)
  1671 apply(simp)
  1672 apply(rule trans)
  1672 apply(rule trans)
  1673 apply(rule perm_compose)
  1673 apply(rule perm_compose)
  1674 apply(simp)
  1674 apply(simp)
  1675 done 
  1675 done 
  1687   "pi \<bullet>aux c \<equiv> pi \<bullet> c"
  1687   "pi \<bullet>aux c \<equiv> pi \<bullet> c"
  1688 
  1688 
  1689 text {* Now the two lemmas *}
  1689 text {* Now the two lemmas *}
  1690 
  1690 
  1691 lemma perm_aux_expand:
  1691 lemma perm_aux_expand:
  1692   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1692   fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1693   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
  1693   shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = pi\<^sub>1 \<bullet>aux (pi\<^sub>2\<bullet>c)" 
  1694 unfolding perm_aux_def by (rule refl)
  1694 unfolding perm_aux_def by (rule refl)
  1695 
  1695 
  1696 lemma perm_compose_aux:
  1696 lemma perm_compose_aux:
  1697   fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1697   fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1698   shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
  1698   shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>aux c) = (pi\<^sub>1\<bullet>pi\<^sub>2) \<bullet>aux (pi\<^sub>1\<bullet>c)" 
  1699 unfolding perm_aux_def by (rule perm_compose)
  1699 unfolding perm_aux_def by (rule perm_compose)
  1700 
  1700 
  1701 text {* 
  1701 text {* 
  1702   are simple consequence of the definition and @{thm [source] perm_compose}. 
  1702   are simple consequence of the definition and @{thm [source] perm_compose}. 
  1703   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
  1703   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
  1732   for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
  1732   for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
  1733   the desired results. Now we can solve the following lemma
  1733   the desired results. Now we can solve the following lemma
  1734 *}
  1734 *}
  1735 
  1735 
  1736 lemma 
  1736 lemma 
  1737   fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
  1737   fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
  1738   shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
  1738   shows "pi\<^sub>1\<bullet>(c, pi\<^sub>2\<bullet>((rev pi\<^sub>1)\<bullet>d)) = (pi\<^sub>1\<bullet>c, (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>d)"
  1739 apply(tactic {* perm_simp_tac @{context} 1 *})
  1739 apply(tactic {* perm_simp_tac @{context} 1 *})
  1740 done
  1740 done
  1741 
  1741 
  1742 
  1742 
  1743 text {*
  1743 text {*
  2047   where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot 
  2047   where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot 
  2048   rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
  2048   rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
  2049   into a number. To solve this problem have a look at the next exercise. 
  2049   into a number. To solve this problem have a look at the next exercise. 
  2050 
  2050 
  2051   \begin{exercise}\label{ex:addsimproc}
  2051   \begin{exercise}\label{ex:addsimproc}
  2052   Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their 
  2052   Write a simproc that replaces terms of the form @{term "t\<^sub>1 + t\<^sub>2"} by their 
  2053   result. You can assume the terms are ``proper'' numbers, that is of the form
  2053   result. You can assume the terms are ``proper'' numbers, that is of the form
  2054   @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
  2054   @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
  2055   \end{exercise}
  2055   \end{exercise}
  2056 
  2056 
  2057   (FIXME: We did not do anything with morphisms. Anything interesting
  2057   (FIXME: We did not do anything with morphisms. Anything interesting