2 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package

     2 imports "../Base" "../Parsing" Simple_Inductive_Package

     5 section {* Parsing and Typing the Specification *}

     5 section {* Parsing and Typing the Specification\label{sec:interface} *}

     6 

     6 

     7 text {* 

     7 text_raw {*

     8   To be able to write down the specification in Isabelle, we have to introduce

     8 \begin{figure}[p]

     9   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the

     9 \begin{boxedminipage}{\textwidth}

    10   new command we chose \simpleinductive{}. In the package we want to support

    10 \begin{isabelle}

    11   some ``advanced'' features: First, we want that the package can cope with

    11 *}

    12   specifications inside locales. For example it should be possible to declare

    13 *}

    14 

    15 locale rel =

    16   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    17 

    18 text {*

    19   and then define the transitive closure and the accessible part as follows:

    20 *}

    21 

    22 

    23 simple_inductive (in rel) 

    24   trcl' 

    25 where

    26   base: "trcl' x x"

    27 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"

    28 

    29 simple_inductive (in rel) 

    30   accpart'

    31 where

    32   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"

    33 

    34 text {* 

    35   Second, we want that the user can specify fixed parameters.

    36   Remember in the previous section we stated that the user can give the 

    37   specification for the transitive closure of a relation @{text R} as 

    38 *}

    39 

    41   trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

    13   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

    42 where

    14 where

    43   base: "trcl\<iota>\<iota> R x x"

    15   base: "trcl R x x"

    44 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"

    16 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"

    45 

    46 text {*

    47   Note that there is no locale given in this specification---the parameter

    48   @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but

    49   stays fixed throughout the specification. The problem with this way of

    50   stating the specification for the transitive closure is that it derives the

    51   following induction principle.

    52 

    53   \begin{center}\small

    54   \mprset{flushleft}

    55   \mbox{\inferrule{

    56              @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

    57              @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

    58              @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}

    59             {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  

    60   \end{center}

    61 

    62   But this does not correspond to the induction principle we derived by hand, which

    63   was

    64   

    65   \begin{center}\small

    66   \mprset{flushleft}

    67   \mbox{\inferrule{

    68              @{thm_style prem1  trcl_induct[no_vars]}\\\\

    69              @{thm_style prem2  trcl_induct[no_vars]}\\\\

    70              @{thm_style prem3  trcl_induct[no_vars]}}

    71             {@{thm_style concl  trcl_induct[no_vars]}}}  

    72   \end{center}

    73 

    74   The difference is that in the one derived by hand the relation @{term R} is not

    75   a parameter of the proposition @{term P} to be proved and it is also not universally

    76   qunatified in the second and third premise. The point is that the parameter @{term R}

    77   stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''

    78   argument of the transitive closure, but one that can be freely instantiated. 

    79   In order to recognise such parameters, we have to extend the specification

    80   to include a mechanism to state fixed parameters. The user should be able

    81   to write 

    82 

    83 *}

    86   trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    19   even and odd

    87 where

    20 where

    88   base: "trcl'' R x x"

    21   even0: "even 0"

    89 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"

    22 | evenS: "odd n \<Longrightarrow> even (Suc n)"

    23 | oddS: "even n \<Longrightarrow> odd (Suc n)"

    92   accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    26   accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"

    93 where

    27 where

    94   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"

    28   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"

    95 

    29 

    96 text {*

    30 (*<*)

    97   \begin{figure}[t]

    31 datatype trm =

    32   Var "string"

    33 | App "trm" "trm"

    34 | Lam "string" "trm"

    35 (*>*)

    36 

    37 simple_inductive 

    38   fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" 

    39 where

    40   fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"

    41 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"

    42 | fresh_lam1: "fresh a (Lam a t)"

    43 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"

    44 text_raw {*

    45 \end{isabelle}

    46 \end{boxedminipage}

    47 \caption{Specification given by the user for the inductive predicates

    48 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and 

    49 @{text "fresh"}.\label{fig:specs}}

    50 \end{figure}  

    51 *}

    52 

    53 text {*

    54   \begin{figure}[p]

    55   \begin{boxedminipage}{\textwidth}

   105   simpleinductive target? fixes (for fixes)? \\

    63   simpleinductive target?\\ fixes

   113   can also contain typing- and syntax anotations); similarly the \emph{fixes} 

    72   can also contain typing- and syntax anotations); \emph{prop} stands for a 

   114   after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a 

   120 text {*

    78 text {* 

   121   This leads directly to the railroad diagram shown in

    79   To be able to write down the specification in Isabelle, we have to introduce

   122   Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram

    80   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the

   123   more or less translates directly into the parser:

    81   new command we chose \simpleinductive{}. Examples of specifications we expect

   124 

    82   the user gives for the inductive predicates from the previous section are

   125   @{ML_chunk [display,gray] parser}

    83   shown in Figure~ref{fig:specs}. The general syntax we will parse is specified

   126 

    84   in the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of 

   127   which we described in Section~\ref{sec:parsingspecs}. If we feed into the 

    85   \simpleinductive{}. This diagram more or less translates directly into 

    86   the parser:

    87 *}

    88 

    89 ML{*val spec_parser = 

    90    OuterParse.fixes -- 

    91    Scan.optional 

    92      (OuterParse.$$$ "where" |--

    93         OuterParse.!!! 

    94           (OuterParse.enum1 "|" 

    95              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}

    96 

    97 text {*

    98   which we explaind in Section~\ref{sec:parsingspecs}.

    99   If you look closely, there is no code for parsing the optional

   100   target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature

   101   which we will inherit for ``free'' from the infrastructure on which

   102   we build the package. The target stands for a locale and allows us 

   103   to specify

   104 *}

   105 

   106 locale rel =

   107   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

   108 

   109 text {*

   110   and then define the transitive closure and the accessible part of this 

   111   locale as follows:

   112 *}

   113 

   114 simple_inductive (in rel) 

   115   trcl' 

   116 where

   117   base: "trcl' x x"

   118 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"

   119 

   120 simple_inductive (in rel) 

   121   accpart'

   122 where

   123   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"

   124 

   125 text {*

   126   Note that in these definitions the parameter @{text R} for the

   127   relation is left implicit.  If we feed into the 

   146 *}

   146 

   147 

   147   then we get back the predicates (with type

   148 

   148   and syntax annotations), and the specifications of the introduction 

   149 text {*

   149   rules. This is all the information we

   150   then we get back a locale (in this case @{ML NONE}), the predicates (with type

   151   and syntax annotations), the parameters (similar as the predicates) and

   152   the specifications of the introduction rules. 

   153 

   154 

   155 

   156   This is all the information we

   159 

   152 *}

   160   @{ML_chunk [display,gray,linenos] syntax}

   153 

   161   

   154 (*<*)

   155 ML{* fun add_inductive pred_specs rule_specs lthy = lthy *}

   156 (*>*)

   157 

   158 ML{*fun add_inductive_cmd pred_specs rule_specs lthy =

   159 let

   160   val ((pred_specs', rule_specs'), _) = 

   161          Specification.read_spec pred_specs rule_specs lthy

   162 in

   163   add_inductive pred_specs' rule_specs' lthy

   164 end*} 

   165 

   166 

   167 ML{*val specification =

   168   spec_parser >>

   169     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*}

   170 

   171 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 

   172               "definition of simple inductive predicates"

   173                  OuterKeyword.thy_decl specification*}

   174 

   175 

   176 text {*

   451 *}

   466 

   452 

   467   The code of the inductive package falls roughly in tree parts: the first

   453 

   468   deals with the definitions, the second with the induction principles and 

   454 (*<*)

   469   the third with the introduction rules. 

   455 end

   470   

   456 (*>*)

   471 *}

   472 (*<*)end(*>*)