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 {*

  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

  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

  "\<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]}

  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"}

  @{text [display] "\<forall>preds. orules \<longrightarrow> pred zs"} 

  @{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 

  Assuming we want to prove the introduction rule 

  @{text [display] "\<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}

  \begin{isabelle}

  (i)~~@{text "As"}\\

  (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}

  \end{isabelle}

  @{text [display] "pred ts"}

  \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}

  @{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.

  @{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