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 |