isabelle-cookbook: comparison ProgTutorial/Package/Ind_General

equal deleted inserted replaced

-:6e2479089226
+:cecd7a941885
 | fresh_lam1: "fresh a (Lam a t)"
 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*>*)
-section {* The Code in a Nutshell\label{sec:nutshell} *}
+section \<open>The Code in a Nutshell\label{sec:nutshell}\<close>
-text {*
+text \<open>
 The inductive package will generate the reasoning infrastructure for
-mutually recursive predicates, say @{text "pred\<^sub>1\<dots>pred\<^sub>n"}. In what
+mutually recursive predicates, say \<open>pred\<^sub>1\<dots>pred\<^sub>n\<close>. 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]
-"\<^sup>*"}. The shorthand for the predicates will therefore be @{text
+"\<^sup>*"}. The shorthand for the predicates will therefore be \<open>preds\<close> or \<open>pred\<^sup>*\<close>. In the case of the predicates there must
-"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.
-The input for the inductive package will be some @{text "preds"} with possible
+The input for the inductive package will be some \<open>preds\<close> with possible
 typing and syntax annotations, and also some introduction rules. We call below the
-introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle
+introduction rules short as \<open>rules\<close>. Borrowing some idealised Isabelle
-notation, one such @{text "rule"} is assumed to be of the form
+notation, one such \<open>rule\<close> is assumed to be of the form
 \begin{isabelle}
-@{text "rule ::=
+\<open>rule ::=
-\<And>xs. \<^latex>\<open>$\\underbrace{\\mbox{\<close>As\<^latex>\<open>}}_{\\text{\\makebox[0mm]{\\rm non-recursive premises}}}$\<close> \<Longrightarrow>
+\<And>xs. \<^latex>\<open>$\underbrace{\mbox{\<close>As\<^latex>\<open>}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$\<close> \<Longrightarrow>
-\<^latex>\<open>$\\underbrace{\\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\\text{\\rm recursive premises}}$>\<close>
+\<^latex>\<open>$\underbrace{\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\text{\rm recursive premises}}$>\<close>
-\<Longrightarrow> pred ts"}
+\<Longrightarrow> pred ts\<close>
 \end{isabelle}
-For the purposes here, we will assume the @{text rules} have this format and
+For the purposes here, we will assume the \<open>rules\<close> have this format and
 omit any code that actually tests this. Therefore ``things'' can go horribly
-wrong, if the @{text "rules"} are not of this form.  The @{text As} and
+wrong, if the \<open>rules\<close> are not of this form.  The \<open>As\<close> and
-@{text Bs} in a @{text "rule"} stand for formulae not involving the
+\<open>Bs\<close> in a \<open>rule\<close> stand for formulae not involving the
-inductive predicates @{text "preds"}; the instances @{text "pred ss"} and
+inductive predicates \<open>preds\<close>; the instances \<open>pred ss\<close> and
-@{text "pred ts"} can stand for different predicates, like @{text
+\<open>pred ts\<close> can stand for different predicates, like \<open>pred\<^sub>1 ss\<close> and \<open>pred\<^sub>2 ts\<close>, in case mutual recursive
-"pred\<^sub>1 ss"} and @{text "pred\<^sub>2 ts"}, in case mutual recursive
+predicates are defined; the terms \<open>ss\<close> and \<open>ts\<close> are the
-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
+ts"} is a premise of the rule. The outermost quantified variables \<open>xs\<close> are usually omitted in the user's input. The quantification for the
-"xs"} are usually omitted in the user's input. The quantification for the
+variables \<open>ys\<close> is local with respect to one recursive premise and
-variables @{text "ys"} is local with respect to one recursive premise and
+must be given. Some examples of \<open>rule\<close>s are
-must be given. Some examples of @{text "rule"}s are
 @{thm [display] fresh_var[no_vars]}
 which has only a single non-recursive premise, whereas
 has a single recursive premise; the rule
 @{thm [display] accpartI[no_vars]}
 has a single recursive premise that has a precondition. As is custom all
-rules are stated without the leading meta-quantification @{text "\<And>xs"}.
+rules are stated without the leading meta-quantification \<open>\<And>xs\<close>.
 The output of the inductive package will be definitions for the predicates,
 induction principles and introduction rules.  For the definitions we need to have the
-@{text rules} in a form where the meta-quantifiers and meta-implications are
+\<open>rules\<close> in a form where the meta-quantifiers and meta-implications are
-replaced by their object logic equivalents. Therefore an @{text "orule"} is
+replaced by their object logic equivalents. Therefore an \<open>orule\<close> is
 of the form
 @{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
+A definition for the predicate \<open>pred\<close> has then the form
 @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-The induction principles for every predicate @{text "pred"} are of the
+The induction principles for every predicate \<open>pred\<close> are of the
 form
 @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
-where in the @{text "rules"}-part every @{text pred} is replaced by a fresh
+where in the \<open>rules\<close>-part every \<open>pred\<close> is replaced by a fresh
-schematic variable @{text "?P"}.
+schematic variable \<open>?P\<close>.
-In order to derive an induction principle for the predicate @{text "pred"},
+In order to derive an induction principle for the predicate \<open>pred\<close>,
-we first transform @{text ind} into the object logic and fix the schematic variables.
+we first transform \<open>ind\<close> into the object logic and fix the schematic variables.
 Hence we have to prove a formula of the form
 @{text [display] "pred zs \<longrightarrow> orules[preds := Ps] \<longrightarrow> P zs"}
-If we assume @{text "pred zs"} and unfold its definition, then we have an
+If we assume \<open>pred zs\<close> and unfold its definition, then we have an
 assumption
 @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"}
 and must prove the goal
 @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
-This can be done by instantiating the @{text "\<forall>preds"}-quantification
+This can be done by instantiating the \<open>\<forall>preds\<close>-quantification
-with the @{text "Ps"}. Then we are done since we are left with a simple
+with the \<open>Ps\<close>. Then we are done since we are left with a simple
 identity.
-Although the user declares the introduction rules @{text rules}, they must
+Although the user declares the introduction rules \<open>rules\<close>, they must
-also be derived from the @{text defs}. These derivations are a bit involved.
+also be derived from the \<open>defs\<close>. 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)\<^sup>* \<Longrightarrow> pred ts"}
 then we have assumptions of the form
 \begin{isabelle}
-(i)~~@{text "As"}\\
+(i)~~\<open>As\<close>\\
-(ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
+(ii)~\<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<close>
 \end{isabelle}
 and must show the goal
 @{text [display] "pred ts"}
-If we now unfold the definitions for the @{text preds}, we have assumptions
+If we now unfold the definitions for the \<open>preds\<close>, we have assumptions
 \begin{isabelle}
-(i)~~~@{text "As"}\\
+(i)~~~\<open>As\<close>\\
-(ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}\\
+(ii)~~\<open>(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*\<close>\\
-(iii)~@{text "orules"}
+(iii)~\<open>orules\<close>
 \end{isabelle}
 and need to show
 @{text [display] "pred ts"}
-In the last step we removed some quantifiers and moved the precondition @{text "orules"}
+In the last step we removed some quantifiers and moved the precondition \<open>orules\<close>
-into the assumption. The @{text "orules"} stand for all introduction rules that are given
+into the assumption. The \<open>orules\<close> stand for all introduction rules that are given
-by the user. We apply the @{text orule} that corresponds to introduction rule we are
+by the user. We apply the \<open>orule\<close> that corresponds to introduction rule we are
 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)\<^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"}\\
+(a)~\<open>As\<close>\\
-(b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}
+(b)~\<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<close>
 \end{isabelle}
-We can immediately discharge the goals @{text "As"} using the assumptions in
+We can immediately discharge the goals \<open>As\<close> using the assumptions in
-@{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we
+\<open>(i)\<close>. The goals in \<open>(b)\<close> can be discharged as follows: we
-assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the
+assume the \<open>Bs\<close> and prove \<open>pred ss\<close>. For this we resolve the
-@{text "Bs"}  with the assumptions in @{text "(ii)"}. This gives us the
+\<open>Bs\<close>  with the assumptions in \<open>(ii)\<close>. This gives us the
 assumptions
 @{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.
+in \<open>(iii)\<close> gives us \<open>pred ss\<close>, which is the goal we are after.
 This completes the proof for introduction rules.
 What remains is to implement in Isabelle the reasoning outlined in this section.
 We will describe the code in the next section. For building testcases, we use the shorthands for
-@{text "even/odd"}, @{term "fresh"} and @{term "accpart"}
+\<open>even/odd\<close>, @{term "fresh"} and @{term "accpart"}
 defined in Figure~\ref{fig:shorthands}.
-*}
+\<close>
-text_raw{*
+text_raw\<open>
 \begin{figure}[p]
 \begin{minipage}{\textwidth}
-\begin{isabelle}*}
+\begin{isabelle}\<close>
-ML %grayML{*(* even-odd example *)
+ML %grayML\<open>(* even-odd example *)
 val eo_defs = [@{thm even_def}, @{thm odd_def}]
 val eo_rules =
 [@{prop "even 0"},
 @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
 (* accessible-part example *)
 val acc_rules =
 [@{prop "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}]
-val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}*}
+val acc_pred = @{term "accpart::('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a \<Rightarrow> bool"}\<close>
-text_raw{*
+text_raw\<open>
 \end{isabelle}
 \end{minipage}
-\caption{Shorthands for the inductive predicates @{text "even"}/@{text "odd"},
+\caption{Shorthands for the inductive predicates \<open>even\<close>/\<open>odd\<close>,
-@{text "fresh"} and @{text "accpart"}. The names of these shorthands follow
+\<open>fresh\<close> and \<open>accpart\<close>. The names of these shorthands follow
-the convention @{text "rules"}, @{text "orules"}, @{text "preds"} and so on.
+the convention \<open>rules\<close>, \<open>orules\<close>, \<open>preds\<close> and so on.
 The purpose of these shorthands is to simplify the construction of testcases
 in Section~\ref{sec:code}.\label{fig:shorthands}}
 \end{figure}
-*}
+\<close>
 end

changeset 565	cecd7a941885
parent 562	daf404920ab9