theory Ind_General_Scheme + −
imports Ind_Intro Simple_Inductive_Package+ −
begin+ −
+ −
(*<*)+ −
simple_inductive+ −
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
base: "trcl R x x"+ −
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"+ −
+ −
simple_inductive+ −
even and odd+ −
where+ −
even0: "even 0"+ −
| evenS: "odd n \<Longrightarrow> even (Suc n)"+ −
| oddS: "even n \<Longrightarrow> odd (Suc n)"+ −
+ −
simple_inductive+ −
accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"+ −
+ −
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 {*+ −
The inductive package will generate the reasoning infrastructure for+ −
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]+ −
"\<^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.+ −
+ −
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)\<^sup>*\<^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. The @{text As} and+ −
@{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\<^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+ −
"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 single recursive premise that has a precondition. As is custom all + −
rules are stated without the leading meta-quantification @{text "\<And>xs"}.+ −
+ −
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+ −
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)\<^sup>* \<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"}-part every @{text pred} is replaced by a fresh+ −
schematic 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 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+ −
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 + −
with the @{text "Ps"}. Then we are done since we are left with a simple + −
identity.+ −
+ −
Although the user declares the introduction rules @{text rules}, they must + −
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)\<^sup>* \<Longrightarrow> pred ts"}+ −
+ −
then we have assumptions of the form+ −
+ −
\begin{isabelle}+ −
(i)~~@{text "As"}\\+ −
(ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}+ −
\end{isabelle}+ −
+ −
and must show the goal+ −
+ −
@{text [display] "pred ts"}+ −
+ −
If we now unfold the definitions for the @{text preds}, we have assumptions+ −
+ −
\begin{isabelle}+ −
(i)~~~@{text "As"}\\+ −
(ii)~~@{text "(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*"}\\+ −
(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 assumption. 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. 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"}\\+ −
(b)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*"}+ −
\end{isabelle}+ −
+ −
We can immediately discharge the goals @{text "As"} using the assumptions 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)\<^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.+ −
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"}+ −
defined in Figure~\ref{fig:shorthands}.+ −
*}+ −
+ −
+ −
text_raw{*+ −
\begin{figure}[p]+ −
\begin{minipage}{\textwidth}+ −
\begin{isabelle}*} + −
ML %grayML{*(* 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_mxs = [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+ −