theory Ind_General_Scheme 
imports  "../Base" 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 @{text "pred\<^isub>1\<dots>pred\<^isub>n"}. In what
  follows we will have the convention that various, possibly empty collections
  of ``things'' (lists, nested implications and so on) are indicated either by
  adding an @{text [quotes] "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"}
  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\<^isub>1 ss"} and @{text
  "pred\<^isub>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 usual 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)\<^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 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)\<^isup>* \<Longrightarrow> pred ts"}

  then we have assumptions of the form

  \begin{isabelle}
  (i)~~@{text "As"}\\
  (ii)~@{text "(\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>*"}
  \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)\<^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 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)\<^isup>* \<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)\<^isup>*"}
  \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)\<^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 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{*(* 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