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

(*>*)

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 

  typing and syntax annotations, and also some introduction rules. We call below the 

  introduction rules short as @{text "rules"}. Borrowing some idealised Isabelle 

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

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

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

  form

  @{text [display] "ind ::= pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}

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

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

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

*}

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

text_raw{*

\end{isabelle}

\end{minipage}

\end{figure}

*}

end