# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1377932865 -3600
# Node ID be361e980acf0bf62ed03bf59ab66052aced572c
# Parent  95d6853dec4a5ea9d0a8d4e2379ab8bd8dedcce1
updated subscripts

diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Essential.thy
--- 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 {*
diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Package/Ind_Extensions.thy
--- 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
diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Package/Ind_General_Scheme.thy
--- 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.
diff -r 95d6853dec4a -r be361e980acf ProgTutorial/Tactical.thy
--- 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}
diff -r 95d6853dec4a -r be361e980acf progtutorial.pdf
Binary file progtutorial.pdf has changed