more work on simple inductive and marked all sections that are still seriously incomplete with TBD
theory Ind_General_Scheme + −
imports Simple_Inductive_Package Ind_Prelims+ −
begin+ −
+ −
(*<*)+ −
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\label{sec: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.+ −
*}+ −
+ −
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 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 + −
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 assumed to be 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}+ −
+ −
For the purposes here, we will assume the @{text rules} 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.\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, like @{text "pred\<^isub>1 ss"} and + −
@{text "pred\<^isub>2 ts"}; @{text ss} and @{text ts} are the+ −
arguments of the predicates. Every formula left of @{text [quotes]+ −
"\<Longrightarrow> pred ts"} is a premise of the rule. The outermost quantified + −
variables @{text "xs"} are usually omitted in the user's input. The + −
quantification for the variables @{text "ys"} is local with respect to + −
one recursive premise and 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+ −
+ −
@{thm [display] evenS[no_vars]}+ −
+ −
has a single recursive premise; the rule+ −
+ −
@{thm [display] accpartI[no_vars]}+ −
+ −
has a recursive premise that has a precondition. As usual all + −
rules are stated without the leading meta-quantification @{text "\<And>xs"}.+ −
+ −
The code of the inductive package falls roughly in tree parts: the first+ −
deals with the definitions, the second with the induction principles and + −
the third with the introduction rules. + −
+ −
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 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"}+ −
+ −
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 every 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 fresh+ −
meta-variable @{text "?P"}.+ −
+ −
In order to derive an induction principle for the predicate @{text "pred"},+ −
we first transform @{text ind} 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"}-quantification + −
with the @{text "Ps"}. Then we are done since we are left with a simple + −
identity.+ −
+ −
Although the user declares introduction rules @{text rules}, they must + −
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"}+ −
+ −
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 @{text orule} that corresponds to introduction rule we are + −
proving. This introduction rule must necessarily 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}+ −
+ −
We can immediately discharge the goals @{text "As"} using the assumption in + −
@{text "(i)"}. The goals in @{text "(b)"} can be discharged as follows: we + −
assume the @{text "Bs"} and prove @{text "pred ss"}. For this we resolve the + −
@{text "Bs"} with the assumptions in @{text "(ii)"}. This gives us the + −
assumptions+ −
+ −
@{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.+ −
This completes the proof for introduction rules.+ −
+ −
What remains is to implement the reasoning outlined above. We do this in+ −
the next section. For building testcases, we use the shorthands for + −
@{text "even/odd"}, @{term "fresh"} and @{term "accpart"}+ −
given in Figure~\ref{fig:shorthands}.+ −
*}+ −
+ −
+ −
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 @{text "even"}-@{text "odd"}, + −
@{text "fresh"} and @{text "accpart"}. The names of these shorthands follow + −
the convention @{text "rules"}, @{text "orules"}, @{text "preds"} 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}+ −
*}+ −
+ −
+ −
+ −
end+ −