--- a/ProgTutorial/Package/Ind_General_Scheme.thy Wed Mar 25 15:09:04 2009 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy Thu Mar 26 19:00:51 2009 +0000
@@ -1,87 +1,235 @@
-theory Ind_General_Scheme
-imports Main
+theory Ind_General_Scheme
+imports Simple_Inductive_Package Ind_Prelims
begin
-section{* The General Construction Principle \label{sec:ind-general-method} *}
+(*<*)
+datatype trm =
+ Var "string"
+| App "trm" "trm"
+| Lam "string" "trm"
+
+simple_inductive
+ fresh :: "string \<Rightarrow> trm \<Rightarrow> bool"
+where
+ fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
+| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
+| 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 *}
text {*
-
+ (FIXME: perhaps move somewhere else)
+
The point of these examples is to get a feeling what the automatic proofs
should do in order to solve all inductive definitions we throw at them. For this
it is instructive to look at the general construction principle
of inductive definitions, which we shall do in the next section.
-
- Before we start with the implementation, it is useful to describe the general
- form of inductive definitions that our package should accept.
- Suppose $R_1,\ldots,R_n$ be mutually inductive predicates and $\vec{p}$ be
- some fixed parameters. Then the introduction rules for $R_1,\ldots,R_n$ may have
- the form
-
- \[
- \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
- R_{k_{ij}}~\vec{p}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow R_{l_i}~\vec{p}~\vec{t}_i
- \qquad \mbox{for\ } i=1,\ldots,r
- \]
-
- where $\vec{A}_i$ and $\vec{B}_{ij}$ are formulae not containing $R_1,\ldots,R_n$.
- Note that by disallowing the inductive predicates to occur in $\vec{B}_{ij}$ we make sure
- that all occurrences of the predicates in the premises of the introduction rules are
- \emph{strictly positive}. This condition guarantees the existence of predicates
- that are closed under the introduction rules shown above. Then the definitions of the
- inductive predicates $R_1,\ldots,R_n$ is:
-
- \[
- \begin{array}{l@ {\qquad}l}
- R_i \equiv \lambda\vec{p}~\vec{z}_i.~\forall P_1 \ldots P_n.~K_1 \longrightarrow \cdots \longrightarrow K_r \longrightarrow P_i~\vec{z}_i &
- \mbox{for\ } i=1,\ldots,n \\[1.5ex]
- \mbox{where} \\
- K_i \equiv \forall\vec{x}_i.~\vec{A}_i \longrightarrow \left(\forall\vec{y}_{ij}.~\vec{B}_{ij} \longrightarrow
- P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i &
- \mbox{for\ } i=1,\ldots,r
- \end{array}
- \]
-
- The induction principles for the inductive predicates $R_1,\ldots,R_n$ are
-
- \[
- \begin{array}{l@ {\qquad}l}
- R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i &
- \mbox{for\ } i=1,\ldots,n \\[1.5ex]
- \mbox{where} \\
- I_i \equiv \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
- P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow P_{l_i}~\vec{t}_i &
- \mbox{for\ } i=1,\ldots,r
- \end{array}
- \]
-
- Since $K_i$ and $I_i$ are equivalent modulo conversion between meta-level and object-level
- connectives, it is clear that the proof of the induction theorem is straightforward. We will
- therefore focus on the proof of the introduction rules. When proving the introduction rule
- shown above, we start by unfolding the definition of $R_1,\ldots,R_n$, which yields
-
- \[
- \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
- \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i
- \]
-
- where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for
- $\forall$ and $\longrightarrow$ yields a goal state in which we have to prove $P_{l_i}~\vec{t}_i$
- from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to the meta-logic format)
- to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption,
- as well as subgoals of the form
-
- \[
- \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i
- \]
-
- that can be solved using the assumptions
-
- \[
- \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow
- \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{and} \qquad \vec{K}
- \]
-
- What remains is to implement these proofs generically.
*}
+text {*
+ The inductive package will generate the reasoning infrastructure
+ for mutually recursive predicates @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
+ follows we will have the convention that various, possibly empty collections of
+ ``things'' are indicated either by adding an @{text "s"} or by adding
+ a superscript @{text [quotes] "\<^isup>*"}. The shorthand for the predicates
+ will therefore be @{text "preds"} or @{text "pred\<^sup>*"}. In this case of the
+ predicates there must be at least a single one in order to obtain a meaningful
+ definition.
+
+ The input for the inductive predicate will be some @{text "preds"} 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
+ notation, one such @{text "rule"} is of the form
+
+ \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}}$>
+ \<Longrightarrow> pred ts"}
+ \end{isabelle}
+
+ We actually assume the user will always state rules of this form and we omit
+ any code that test this format. So things can go horribly wrong if the
+ @{text "rules"} are not of this form.\footnote{FIXME: Exercise to test this
+ format.} The @{text As} and @{text Bs} in a @{text "rule"} are formulae not
+ involving the inductive predicates @{text "preds"}; the instances @{text
+ "pred ss"} and @{text "pred ts"} can stand for different predicates.
+ Everything left of @{text [quotes] "\<Longrightarrow> pred ts"} are called the premises of
+ the rule. The variables @{text "xs"} are usually omitted in the user's
+ input. The variables @{text "ys"} are local with respect to on recursive
+ premise. Some examples of @{text "rule"}s the user might write are:
+
+
+ @{thm [display] fresh_var[no_vars]}
+
+ which has only a single non-recursive premise, whereas
+
+ @{thm [display] evenS[no_vars]}
+
+ has a single recursive premise; the rule
+
+ @{thm [display] accpartI[no_vars]}
+
+ has a recursive premise which has a precondition. In the examples, all
+ rules are stated without the leading meta-quantification @{text "\<And>xs"}.
+
+ The code of the inductive package falls roughly in tree parts involving
+ the definitions, the induction principles and the introduction rules,
+ respectively. For the definitions we need to have the @{text rules}
+ in a form where the meta-quantifiers and meta-implications are replaced
+ by their object logic equivalent. 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"}
+
+ A definition for the predicate @{text "pred"} has then the form
+
+ @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
+
+ The induction principles for the predicate @{text "pred"} are of the
+ form
+
+ @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
+
+ where in the @{text "rules"} every @{text pred} is replaced by a new
+ (meta)variable @{text "?P"}.
+
+ In order to derive an induction principle for the predicate @{text "pred"}
+ we first transform it into the object logic and fix the meta-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
+
+ @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"}
+
+ and must prove
+
+ @{text [display] "orules[preds := Ps] \<longrightarrow> P zs"}
+
+ This can be done by instantiating the @{text "\<forall>preds"} with the @{text "Ps"}.
+ Then we are done since we are left with a simple identity.
+
+ The proofs for the introduction rules are more 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"}
+
+ then we can assume
+
+ \begin{isabelle}
+ (i)~~@{text "As"}\\
+ (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+ \end{isabelle}
+
+ and must show
+
+ @{text [display] "pred ts"}
+
+ If we now unfold the definitions for the @{text preds}, we have
+
+ \begin{isabelle}
+ (i)~~~@{text "As"}\\
+ (ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}\\
+ (iii)~@{text "orules"}
+ \end{isabelle}
+
+ and need to show
+
+ @{text [display] "pred ts"}
+
+ In the last step we removed some quantifiers and moved the precondition @{text "orules"}
+ into the assumtion. The @{text "orules"} stand for all introduction rules that are given
+ by the user. We apply the one which corresponds to introduction rule we are proving.
+ This introduction rule must be of the form
+
+ @{text [display] "As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+
+ When we apply this rule we end up in the goal state where we have to prove
+
+ \begin{isabelle}
+ (a)~@{text "As"}\\
+ (b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
+ \end{isabelle}
+
+ The goals @{text "As"} we can immediately discharge with the assumption in @{text "(i)"}.
+ The goals in @{text "(b)"} we discharge as follows: we assume the @{text "(iv)"}
+ @{text "Bs"} and prove @{text "(c)"} @{text "pred ss"}. We then resolve the
+ @{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us
+
+ @{text [display] "(\<forall>preds. orules \<longrightarrow> pred ss)\<^isup>*"}
+
+ 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.
+
+
+ What remains is to implement the reasoning outlined above.
+ For building testcases, we use some shorthands for the definitions
+ of @{text "even/odd"}, @{term "fresh"} and @{term "accpart"}.
+*}
+
+
+text_raw{*
+\begin{figure}[p]
+\begin{minipage}{\textwidth}
+\begin{isabelle}*}
+ML{*(* 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)"},
+ @{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
+
+val eo_orules =
+ [@{prop "even 0"},
+ @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
+ @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
+
+val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+val eo_prednames = [@{binding "even"}, @{binding "odd"}]
+val eo_syns = [NoSyn, NoSyn]
+val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
+val e_pred = @{term "even::nat\<Rightarrow>bool"}
+val e_arg_tys = [@{typ "nat"}]
+
+
+
+(* freshness example *)
+val fresh_rules =
+ [@{prop "\<And>a b. a \<noteq> b \<Longrightarrow> fresh a (Var b)"},
+ @{prop "\<And>a s t. fresh a t \<Longrightarrow> fresh a s \<Longrightarrow> fresh a (App t s)"},
+ @{prop "\<And>a t. fresh a (Lam a t)"},
+ @{prop "\<And>a b t. a \<noteq> b \<Longrightarrow> fresh a t \<Longrightarrow> fresh a (Lam b t)"}]
+
+val fresh_orules =
+ [@{prop "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"},
+ @{prop "\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"},
+ @{prop "\<forall>a t. fresh a (Lam a t)"},
+ @{prop "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}]
+
+val fresh_pred = @{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"}
+val fresh_arg_tys = [@{typ "string"}, @{typ "trm"}]
+
+
+
+(* 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"}*}
+text_raw{*
+\end{isabelle}
+\end{minipage}
+\caption{Shorthands for the inductive predicates of @{text "even"}-@{text "odd"},
+ @{text "fresh"} and @{text "accpart"}. The follow the convention @{text "rules"},
+ @{text "orules"}, @{text "preds"} and so on as used in Section ???. The purpose
+ of these shorthands is to simplify the construction of testcases.}
+\end{figure}
+*}
+
+
+
end