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 \<open>The Code in a Nutshell\label{sec:nutshell}\<close>+
−
+
−
+
−
text \<open>+
−
  The inductive package will generate the reasoning infrastructure for+
−
  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 \<open>preds\<close> or \<open>pred\<^sup>*\<close>. 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 \<open>preds\<close> with possible +
−
  typing and syntax annotations, and also some introduction rules. We call below the +
−
  introduction rules short as \<open>rules\<close>. Borrowing some idealised Isabelle +
−
  notation, one such \<open>rule\<close> is assumed to be of the form+
−
+
−
  \begin{isabelle}+
−
  \<open>rule ::= +
−
  \<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> +
−
  \<Longrightarrow> pred ts\<close>+
−
  \end{isabelle}+
−
  +
−
  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 \<open>rules\<close> are not of this form.  The \<open>As\<close> and+
−
  \<open>Bs\<close> in a \<open>rule\<close> stand for formulae not involving the+
−
  inductive predicates \<open>preds\<close>; the instances \<open>pred ss\<close> and+
−
  \<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+
−
  predicates are defined; the terms \<open>ss\<close> and \<open>ts\<close> 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 \<open>xs\<close> 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+
−
  must be given. Some examples of \<open>rule\<close>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 \<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+
−
  \<open>rules\<close> in a form where the meta-quantifiers and meta-implications are+
−
  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 \<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 \<open>pred\<close> are of the+
−
  form+
−
+
−
  @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}+
−
+
−
  where in the \<open>rules\<close>-part every \<open>pred\<close> is replaced by a fresh+
−
  schematic variable \<open>?P\<close>.+
−
+
−
  In order to derive an induction principle for the predicate \<open>pred\<close>,+
−
  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 \<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 \<open>\<forall>preds\<close>-quantification +
−
  with the \<open>Ps\<close>. Then we are done since we are left with a simple +
−
  identity.+
−
  +
−
  Although the user declares the introduction rules \<open>rules\<close>, they must +
−
  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)~~\<open>As\<close>\\+
−
  (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 \<open>preds\<close>, we have assumptions+
−
+
−
  \begin{isabelle}+
−
  (i)~~~\<open>As\<close>\\+
−
  (ii)~~\<open>(\<And>ys. Bs \<Longrightarrow> \<forall>preds. orules \<longrightarrow> pred ss)\<^sup>*\<close>\\+
−
  (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 \<open>orules\<close>  +
−
  into the assumption. The \<open>orules\<close> stand for all introduction rules that are given +
−
  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)~\<open>As\<close>\\+
−
  (b)~\<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<close>+
−
  \end{isabelle}+
−
+
−
  We can immediately discharge the goals \<open>As\<close> using the assumptions in +
−
  \<open>(i)\<close>. The goals in \<open>(b)\<close> can be discharged as follows: we +
−
  assume the \<open>Bs\<close> and prove \<open>pred ss\<close>. For this we resolve 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 \<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 +
−
  \<open>even/odd\<close>, @{term "fresh"} and @{term "accpart"}+
−
  defined in Figure~\ref{fig:shorthands}.+
−
\<close>+
−
+
−
+
−
text_raw\<open>+
−
\begin{figure}[p]+
−
\begin{minipage}{\textwidth}+
−
\begin{isabelle}\<close>  +
−
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)"},+
−
   @{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"}\<close>+
−
text_raw\<open>+
−
\end{isabelle}+
−
\end{minipage}+
−
\caption{Shorthands for the inductive predicates \<open>even\<close>/\<open>odd\<close>, +
−
  \<open>fresh\<close> and \<open>accpart\<close>. The names of these shorthands follow +
−
  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+
−