--- a/ProgTutorial/Essential.thy Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Essential.thy Sat Aug 31 08:07:45 2013 +0100
@@ -699,9 +699,9 @@
\begin{exercise}\label{fun:revsum}
Write a function @{text "rev_sum : term -> term"} that takes a
- term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
- and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
- the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
+ term of the form @{text "t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n"} (whereby @{text "n"} might be one)
+ and returns the reversed sum @{text "t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1"}. Assume
+ the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"}
associates to the left. Try your function on some examples.
\end{exercise}
@@ -1514,8 +1514,8 @@
*}
lemma
- assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
- and assm\<^isub>2: "P t"
+ assumes assm\<^sub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
+ and assm\<^sub>2: "P t"
shows "Q t"(*<*)oops(*>*)
text {*
--- a/ProgTutorial/Package/Ind_Extensions.thy Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy Sat Aug 31 08:07:45 2013 +0100
@@ -135,7 +135,7 @@
form
\begin{isabelle}
- @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+ @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
\end{isabelle}
where the @{text "As"} and @{text "Bs"} can be any collection of formulae
--- a/ProgTutorial/Package/Ind_General_Scheme.thy Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy Sat Aug 31 08:07:45 2013 +0100
@@ -41,11 +41,11 @@
text {*
The inductive package will generate the reasoning infrastructure for
- mutually recursive predicates, say @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+ mutually recursive predicates, say @{text "pred\<^sub>1\<dots>pred\<^sub>n"}. In what
follows we will have the convention that various, possibly empty collections
of ``things'' (lists, terms, nested implications and so on) are indicated either by
adding an @{text [quotes] "s"} or by adding a superscript @{text [quotes]
- "\<^isup>*"}. The shorthand for the predicates will therefore be @{text
+ "\<^sup>*"}. The shorthand for the predicates will therefore be @{text
"preds"} or @{text "pred\<^sup>*"}. In the case of the predicates there must
be, of course, at least a single one in order to obtain a meaningful
definition.
@@ -58,7 +58,7 @@
\begin{isabelle}
@{text "rule ::=
\<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow>
- \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*\<^raw:}}_{\text{\rm recursive premises}}$>
+ \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$>
\<Longrightarrow> pred ts"}
\end{isabelle}
@@ -68,7 +68,7 @@
@{text Bs} in a @{text "rule"} stand for formulae not involving the
inductive predicates @{text "preds"}; the instances @{text "pred ss"} and
@{text "pred ts"} can stand for different predicates, like @{text
- "pred\<^isub>1 ss"} and @{text "pred\<^isub>2 ts"}, in case mutual recursive
+ "pred\<^sub>1 ss"} and @{text "pred\<^sub>2 ts"}, in case mutual recursive
predicates are defined; the terms @{text ss} and @{text ts} are the
arguments of these predicates. Every formula left of @{text [quotes] "\<Longrightarrow> pred
ts"} is a premise of the rule. The outermost quantified variables @{text
@@ -96,7 +96,7 @@
replaced by their object logic equivalents. Therefore an @{text "orule"} is
of the form
- @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
+ @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^sup>* \<longrightarrow> pred ts"}
A definition for the predicate @{text "pred"} has then the form
@@ -133,13 +133,13 @@
also be derived from the @{text defs}. These derivations are a bit involved.
Assuming we want to prove the introduction rule
- @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+ @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
then we have assumptions of the form
\begin{isabelle}
(i)~~@{text "As"}\\
- (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+ (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
\end{isabelle}
and must show the goal
@@ -150,7 +150,7 @@
\begin{isabelle}
(i)~~~@{text "As"}\\
- (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\
+ (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}\\
(iii)~@{text "orules"}
\end{isabelle}
@@ -164,14 +164,14 @@
proving. After transforming the object connectives into meta-connectives, this introduction
rule must necessarily be of the form
- @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+ @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
When we apply this rule we end up in the goal state where we have to prove
goals of the form
\begin{isabelle}
(a)~@{text "As"}\\
- (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+ (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
\end{isabelle}
We can immediately discharge the goals @{text "As"} using the assumptions in
@@ -180,7 +180,7 @@
@{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the
assumptions
- @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
+ @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}
Instantiating the universal quantifiers and then resolving with the assumptions
in @{text "(iii)"} gives us @{text "pred ss"}, which is the goal we are after.
--- 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}
Binary file progtutorial.pdf has changed