--- a/ProgTutorial/Tactical.thy Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Tactical.thy Sat Aug 31 08:07:45 2013 +0100
@@ -243,9 +243,9 @@
this consider the proof in Figure~\ref{fig:goalstates}: as can be seen,
internally every goal state is an implication of the form
- @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #C"}
-
- where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
+ @{text[display] "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}
+
+ where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are
the subgoals. So after setting up the lemma, the goal state is always of the
form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
"#C"}. Since the goal @{term C} can potentially be an implication, there is a
@@ -253,7 +253,7 @@
@{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
as a @{text #}). This wrapper prevents that premises of @{text C} are
misinterpreted as open subgoals. While tactics can operate on the subgoals
- (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
+ (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
@{term C} intact, with the exception of possibly instantiating schematic
variables. This instantiations of schematic variables can be observed
on the user level. Have a look at the following definition and proof.
@@ -866,8 +866,8 @@
sorry
text {*
- and you want to apply it to the goal @{term "(t\<^isub>1 t\<^isub>2) \<le>
- (s\<^isub>1 s\<^isub>2)"}. Since in the theorem all variables are
+ and you want to apply it to the goal @{term "(t\<^sub>1 t\<^sub>2) \<le>
+ (s\<^sub>1 s\<^sub>2)"}. Since in the theorem all variables are
schematic, we have a nasty higher-order unification problem and @{text rtac}
will not be able to apply this rule in the way we want. For the goal at hand
we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
@@ -899,7 +899,7 @@
*}
lemma
- 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)"
+ 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)"
apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
@@ -1377,8 +1377,8 @@
\begin{isabelle}
\begin{center}
- \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
- {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
+ \mbox{\inferrule{@{text "t\<^sub>1 \<equiv> s\<^sub>1 \<dots> t\<^sub>n \<equiv> s\<^sub>n"}}
+ {@{text "constr t\<^sub>1\<dots>t\<^sub>n \<equiv> constr s\<^sub>1\<dots>s\<^sub>n"}}}
\end{center}
\end{isabelle}
@@ -1621,9 +1621,9 @@
end
lemma perm_append[simp]:
- fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
- shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
-by (induct pi\<^isub>1) (auto)
+ fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+ shows "((pi\<^sub>1@pi\<^sub>2)\<bullet>c) = (pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c))"
+by (induct pi\<^sub>1) (auto)
lemma perm_bij[simp]:
fixes c d::"nat" and pi::"prm"
@@ -1636,9 +1636,9 @@
by (induct pi arbitrary: c) (auto)
lemma perm_compose:
-fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
-shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
-by (induct pi\<^isub>2) (auto)
+fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>(pi\<^sub>1\<bullet>c)"
+by (induct pi\<^sub>2) (auto)
text_raw {*
\end{isabelle}
\end{boxedminipage}
@@ -1666,8 +1666,8 @@
*}
lemma
-fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
- 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)"
+fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+ 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)"
apply(simp)
apply(rule trans)
apply(rule perm_compose)
@@ -1689,13 +1689,13 @@
text {* Now the two lemmas *}
lemma perm_aux_expand:
- fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
- shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)"
+ fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+ shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = pi\<^sub>1 \<bullet>aux (pi\<^sub>2\<bullet>c)"
unfolding perm_aux_def by (rule refl)
lemma perm_compose_aux:
- fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
- 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)"
+ fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+ 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)"
unfolding perm_aux_def by (rule perm_compose)
text {*
@@ -1734,8 +1734,8 @@
*}
lemma
- fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
- 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)"
+ fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
+ 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)"
apply(tactic {* perm_simp_tac @{context} 1 *})
done
@@ -2049,7 +2049,7 @@
into a number. To solve this problem have a look at the next exercise.
\begin{exercise}\label{ex:addsimproc}
- Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their
+ Write a simproc that replaces terms of the form @{term "t\<^sub>1 + t\<^sub>2"} by their
result. You can assume the terms are ``proper'' numbers, that is of the form
@{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
\end{exercise}