ProgTutorial/Package/Ind_Interface.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 01 Apr 2009 12:26:56 +0100
changeset 219 98d43270024f
parent 218 7ff7325e3b4e
child 224 647cab4a72c2
permissions -rw-r--r--
more work on the simple inductive chapter
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     1
theory Ind_Interface
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
     2
imports "../Base" "../Parsing" Simple_Inductive_Package
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     3
begin
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
     4
215
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
     5
section {* Parsing and Typing the Specification\label{sec:interface} *}
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
     6
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
     7
text_raw {*
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
     8
\begin{figure}[p]
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
     9
\begin{boxedminipage}{\textwidth}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    10
\begin{isabelle}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    11
*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    12
simple_inductive
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    13
  trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    14
where
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    15
  base: "trcl R x x"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    16
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    17
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    18
simple_inductive
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    19
  even and odd
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    20
where
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    21
  even0: "even 0"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    22
| evenS: "odd n \<Longrightarrow> even (Suc n)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    23
| oddS: "even n \<Longrightarrow> odd (Suc n)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    24
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    25
simple_inductive
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    26
  accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    27
where
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    28
  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    29
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    30
(*<*)
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    31
datatype trm =
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    32
  Var "string"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    33
| App "trm" "trm"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    34
| Lam "string" "trm"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    35
(*>*)
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    36
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    37
simple_inductive 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    38
  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    39
where
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    40
  fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    41
| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    42
| fresh_lam1: "fresh a (Lam a t)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    43
| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    44
text_raw {*
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    45
\end{isabelle}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    46
\end{boxedminipage}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    47
\caption{Specification given by the user for the inductive predicates
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    48
@{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    49
@{text "fresh"}.\label{fig:specs}}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    50
\end{figure}  
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    51
*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    52
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    53
text {*
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    54
  \begin{figure}[p]
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    55
  \begin{boxedminipage}{\textwidth}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    56
  \begin{isabelle}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    57
  \railnontermfont{\rmfamily\itshape}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    58
  \railterm{simpleinductive,where,for}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    59
  \railalias{simpleinductive}{\simpleinductive{}}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    60
  \railalias{where}{\isacommand{where}}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    61
  \railalias{for}{\isacommand{for}}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    62
  \begin{rail}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    63
  simpleinductive target?\\ fixes
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    64
  (where (thmdecl? prop + '|'))?
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    65
  ;
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    66
  \end{rail}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    67
  \end{isabelle}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    68
  \end{boxedminipage}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    69
  \caption{A railroad diagram describing the syntax of \simpleinductive{}. 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    70
  The \emph{target} indicates an optional locale; the \emph{fixes} are an 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    71
  \isacommand{and}-separated list of names for the inductive predicates (they
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    72
  can also contain typing- and syntax anotations); \emph{prop} stands for a 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    73
  introduction rule with an optional theorem declaration (\emph{thmdecl}).
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    74
  \label{fig:railroad}}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    75
  \end{figure}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    76
*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    77
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
    78
text {* 
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
    79
  To be able to write down the specification in Isabelle, we have to introduce
129
e0d368a45537 started a section about simprocs
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
    80
  a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    81
  new command we chose \simpleinductive{}. Examples of specifications we expect
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    82
  the user gives for the inductive predicates from the previous section are
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    83
  shown in Figure~ref{fig:specs}. The general syntax we will parse is specified
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    84
  in the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    85
  \simpleinductive{}. This diagram more or less translates directly into 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    86
  the parser:
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    87
*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    88
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    89
ML{*val spec_parser = 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    90
   OuterParse.fixes -- 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    91
   Scan.optional 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    92
     (OuterParse.$$$ "where" |--
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    93
        OuterParse.!!! 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    94
          (OuterParse.enum1 "|" 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    95
             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    96
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    97
text {*
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    98
  which we explaind in Section~\ref{sec:parsingspecs}.
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
    99
  If you look closely, there is no code for parsing the optional
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   100
  target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   101
  which we will inherit for ``free'' from the infrastructure on which
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   102
  we build the package. The target stands for a locale and allows us 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   103
  to specify
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   104
*}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   105
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   106
locale rel =
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   107
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   108
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   109
text {*
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 215
diff changeset
   110
  and then define the transitive closure and the accessible part of this 
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 215
diff changeset
   111
  locale as follows:
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   112
*}
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   113
129
e0d368a45537 started a section about simprocs
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   114
simple_inductive (in rel) 
e0d368a45537 started a section about simprocs
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   115
  trcl' 
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   116
where
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   117
  base: "trcl' x x"
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   118
| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   119
129
e0d368a45537 started a section about simprocs
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   120
simple_inductive (in rel) 
e0d368a45537 started a section about simprocs
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   121
  accpart'
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   122
where
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   123
  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   124
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   125
text {*
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   126
  Note that in these definitions the parameter @{text R} for the
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   127
  relation is left implicit.  If we feed into the 
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   128
  parser the string (which corresponds to our definition of @{term even} and 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   129
  @{term odd}):
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   130
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   131
  @{ML_response [display,gray]
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   132
"let
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   133
  val input = filtered_input
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   134
     (\"even and odd \" ^  
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   135
      \"where \" ^
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   136
      \"  even0[intro]: \\\"even 0\\\" \" ^ 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   137
      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   138
      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   139
in
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   140
  parse spec_parser input
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   141
end"
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   142
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   143
     [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   144
      ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   145
      ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   146
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   147
  then we get back the predicates (with type
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   148
  and syntax annotations), and the specifications of the introduction 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   149
  rules. This is all the information we
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   150
  need for calling the package and setting up the keyword. The latter is
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   151
  done in Lines 6 and 7 in the code below.
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   152
*}
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   153
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   154
(*<*)
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   155
ML{* fun add_inductive pred_specs rule_specs lthy = lthy *}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   156
(*>*)
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   157
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   158
ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   159
let
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   160
  val ((pred_specs', rule_specs'), _) = 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   161
         Specification.read_spec pred_specs rule_specs lthy
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   162
in
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   163
  add_inductive pred_specs' rule_specs' lthy
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   164
end*} 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   165
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   166
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   167
ML{*val specification =
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   168
  spec_parser >>
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   169
    (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   170
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   171
ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   172
              "definition of simple inductive predicates"
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   173
                 OuterKeyword.thy_decl specification*}
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   174
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   175
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   176
text {*
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   177
  We call @{ML OuterSyntax.command} with the kind-indicator @{ML
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   178
  OuterKeyword.thy_decl} since the package does not need to open up any goal
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   179
  state (see Section~\ref{sec:newcommand}). Note that the predicates and
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   180
  parameters are at the moment only some ``naked'' variables: they have no
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   181
  type yet (even if we annotate them with types) and they are also no defined
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   182
  constants yet (which the predicates will eventually be).  In Lines 1 to 4 we
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   183
  gather the information from the parser to be processed further. The locale
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   184
  is passed as argument to the function @{ML
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   185
  Toplevel.local_theory}.\footnote{FIXME Is this already described?} The other
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   186
  arguments, i.e.~the predicates, parameters and intro rule specifications,
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   187
  are passed to the function @{ML add_inductive in SimpleInductivePackage}
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   188
  (Line 4).
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   189
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   190
  We now come to the second subtask of the package, namely transforming the 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   191
  parser output into some internal datastructures that can be processed further. 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   192
  Remember that at the moment the introduction rules are just strings, and even
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   193
  if the predicates and parameters can contain some typing annotations, they
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   194
  are not yet in any way reflected in the introduction rules. So the task of
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   195
  @{ML add_inductive in SimpleInductivePackage} is to transform the strings
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   196
  into properly typed terms. For this it can use the function 
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   197
  @{ML read_spec in Specification}. This function takes some constants
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   198
  with possible typing annotations and some rule specifications and attempts to
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   199
  find a type according to the given type constraints and the type constraints
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   200
  by the surrounding (local theory). However this function is a bit
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   201
  too general for our purposes: we want that each introduction rule has only 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   202
  name (for example @{text even0} or @{text evenS}), if a name is given at all.
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   203
  The function @{ML read_spec in Specification} however allows more
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   204
  than one rule. Since it is quite convenient to rely on this function (instead of
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   205
  building your own) we just quick ly write a wrapper function that translates
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   206
  between our specific format and the general format expected by 
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   207
  @{ML read_spec in Specification}. The code of this wrapper is as follows:
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   208
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   209
  @{ML_chunk [display,gray,linenos] read_specification}
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   210
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   211
  It takes a list of constants, a list of rule specifications and a local theory 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   212
  as input. Does the transformation of the rule specifications in Line 3; calls
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   213
  the function and transforms the now typed rule specifications back into our
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   214
  format and returns the type parameter and typed rule specifications. 
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   215
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   216
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   217
   @{ML_chunk [display,gray,linenos] add_inductive}
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   218
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   219
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   220
  In order to add a new inductive predicate to a theory with the help of our
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   221
  package, the user must \emph{invoke} it. For every package, there are
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   222
  essentially two different ways of invoking it, which we will refer to as
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   223
  \emph{external} and \emph{internal}. By external invocation we mean that the
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   224
  package is called from within a theory document. In this case, the
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   225
  specification of the inductive predicate, including type annotations and
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   226
  introduction rules, are given as strings by the user. Before the package can
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   227
  actually make the definition, the type and introduction rules have to be
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   228
  parsed. In contrast, internal invocation means that the package is called by
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   229
  some other package. For example, the function definition package
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 118
diff changeset
   230
  calls the inductive definition package to define the
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   231
  graph of the function. However, it is not a good idea for the function
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   232
  definition package to pass the introduction rules for the function graph to
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   233
  the inductive definition package as strings. In this case, it is better to
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   234
  directly pass the rules to the package as a list of terms, which is more
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   235
  robust than handling strings that are lacking the additional structure of
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   236
  terms. These two ways of invoking the package are reflected in its ML
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   237
  programming interface, which consists of two functions:
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   238
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   239
113
9b6c9d172378 slightly updated
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   240
  @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   241
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   242
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   243
text {*
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   244
  (FIXME: explain Binding.binding; Attrib.binding somewhere else)
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   245
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   246
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   247
  The function for external invocation of the package is called @{ML
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   248
  add_inductive in SimpleInductivePackage}, whereas the one for internal
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   249
  invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   250
  of these functions take as arguments the names and types of the inductive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   251
  predicates, the names and types of their parameters, the actual introduction
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   252
  rules and a \emph{local theory}.  They return a local theory containing the
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   253
  definition and the induction principle as well introduction rules. 
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   254
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   255
  Note that @{ML add_inductive_i in SimpleInductivePackage} expects
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   256
  the types of the predicates and parameters to be specified using the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   257
  datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   258
  add_inductive in SimpleInductivePackage} expects them to be given as
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   259
  optional strings. If no string is given for a particular predicate or
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   260
  parameter, this means that the type should be inferred by the
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   261
  package. 
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   262
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   263
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   264
  Additional \emph{mixfix syntax} may be associated with the
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   265
  predicates and parameters as well. Note that @{ML add_inductive_i in
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   266
  SimpleInductivePackage} does not allow mixfix syntax to be associated with
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   267
  parameters, since it can only be used for parsing.\footnote{FIXME: why ist it there then?} 
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   268
  The names of the
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   269
  predicates, parameters and rules are represented by the type @{ML_type
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   270
  Binding.binding}. Strings can be turned into elements of the type @{ML_type
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   271
  Binding.binding} using the function @{ML [display] "Binding.name : string ->
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   272
  Binding.binding"} Each introduction rule is given as a tuple containing its
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   273
  name, a list of \emph{attributes} and a logical formula. Note that the type
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   274
  @{ML_type Attrib.binding} used in the list of introduction rules is just a
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   275
  shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}.  The
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   276
  function @{ML add_inductive_i in SimpleInductivePackage} expects the formula
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   277
  to be specified using the datatype @{ML_type term}, whereas @{ML
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   278
  add_inductive in SimpleInductivePackage} expects it to be given as a string.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   279
  An attribute specifies additional actions and transformations that should be
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   280
  applied to a theorem, such as storing it in the rule databases used by
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   281
  automatic tactics like the simplifier. The code of the package, which will
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   282
  be described in the following section, will mostly treat attributes as a
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   283
  black box and just forward them to other functions for storing theorems in
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   284
  local theories.  The implementation of the function @{ML add_inductive in
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   285
  SimpleInductivePackage} for external invocation of the package is quite
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   286
  simple. Essentially, it just parses the introduction rules and then passes
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   287
  them on to @{ML add_inductive_i in SimpleInductivePackage}:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   288
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   289
  @{ML_chunk [display] add_inductive}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   290
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   291
  For parsing and type checking the introduction rules, we use the function
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   292
  
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   293
  @{ML [display] "Specification.read_specification:
76
b99fa5fa63fc adapted to changes in binding.ML
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   294
  (Binding.binding * string option * mixfix) list ->  (*{variables}*)
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 129
diff changeset
   295
  (Attrib.binding * string list) list ->  (*{rules}*)
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   296
  local_theory ->
76
b99fa5fa63fc adapted to changes in binding.ML
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   297
  (((Binding.binding * typ) * mixfix) list *
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   298
   (Attrib.binding * term list) list) *
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   299
  local_theory"}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   300
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   301
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   302
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   303
  During parsing, both predicates and parameters are treated as variables, so
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   304
  the lists \verb!preds_syn! and \verb!params_syn! are just appended
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   305
  before being passed to @{ML read_spec in Specification}. Note that the format
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   306
  for rules supported by @{ML read_spec in Specification} is more general than
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   307
  what is required for our package. It allows several rules to be associated
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   308
  with one name, and the list of rules can be partitioned into several
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   309
  sublists. In order for the list \verb!intro_srcs! of introduction rules
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   310
  to be acceptable as an input for @{ML read_spec in Specification}, we first
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   311
  have to turn it into a list of singleton lists. This transformation
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   312
  has to be reversed later on by applying the function
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   313
  @{ML [display] "the_single: 'a list -> 'a"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   314
  to the list \verb!specs! containing the parsed introduction rules.
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   315
  The function @{ML read_spec in Specification} also returns the list \verb!vars!
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   316
  of predicates and parameters that contains the inferred types as well.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   317
  This list has to be chopped into the two lists \verb!preds_syn'! and
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   318
  \verb!params_syn'! for predicates and parameters, respectively.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   319
  All variables occurring in a rule but not in the list of variables passed to
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
   320
  @{ML read_spec in Specification} will be bound by a meta-level universal
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   321
  quantifier.
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   322
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   323
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   324
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   325
  Finally, @{ML read_specification in Specification} also returns another local theory,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   326
  but we can safely discard it. As an example, let us look at how we can use this
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   327
  function to parse the introduction rules of the @{text trcl} predicate:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   328
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   329
  @{ML_response [display]
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   330
"Specification.read_specification
55
0b55402ae95e Adapted to changes in binding module.
berghofe
parents: 53
diff changeset
   331
  [(Binding.name \"trcl\", NONE, NoSyn),
0b55402ae95e Adapted to changes in binding module.
berghofe
parents: 53
diff changeset
   332
   (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]
176
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 129
diff changeset
   333
  [((Binding.name \"base\", []), [\"trcl r x x\"]),
3da5f3f07d8b updated to new read_specification
Christian Urban <urbanc@in.tum.de>
parents: 129
diff changeset
   334
   ((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   335
  @{context}"
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   336
"((\<dots>,
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   337
  [(\<dots>,
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   338
    [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   339
       Const (\"Trueprop\", \<dots>) $
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   340
         (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 0 $ Bound 0))]),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   341
   (\<dots>,
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   342
    [Const (\"all\", \<dots>) $ Abs (\"x\", TFree (\"'a\", \<dots>),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   343
       Const (\"all\", \<dots>) $ Abs (\"y\", TFree (\"'a\", \<dots>),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   344
         Const (\"all\", \<dots>) $ Abs (\"z\", TFree (\"'a\", \<dots>),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   345
           Const (\"==>\", \<dots>) $
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   346
             (Const (\"Trueprop\", \<dots>) $
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 35
diff changeset
   347
               (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   348
             (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   349
 \<dots>)
76
b99fa5fa63fc adapted to changes in binding.ML
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   350
: (((Binding.binding * typ) * mixfix) list *
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   351
   (Attrib.binding * term list) list) * local_theory"}
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   352
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   353
  In the list of variables passed to @{ML read_specification in Specification}, we have
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   354
  used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   355
  mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r},
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   356
  whereas the type of \texttt{trcl} is computed using type inference.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   357
  The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   358
  are turned into bound variables with the de Bruijn indices,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   359
  whereas \texttt{trcl} and \texttt{r} remain free variables.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   360
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   361
*}
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   362
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   363
text {*
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   364
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   365
  \paragraph{Parsers for theory syntax}
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   366
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   367
  Although the function @{ML add_inductive in SimpleInductivePackage} parses terms and types, it still
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   368
  cannot be used to invoke the package directly from within a theory document.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   369
  In order to do this, we have to write another parser. Before we describe
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   370
  the process of writing parsers for theory syntax in more detail, we first
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   371
  show some examples of how we would like to use the inductive definition
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   372
  package.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   373
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   374
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   375
  The definition of the transitive closure should look as follows:
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   376
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   377
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
   378
ML {* SpecParse.opt_thm_name *}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
   379
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   380
text {*
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   381
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   382
  A proposition can be parsed using the function @{ML prop in OuterParse}.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   383
  Essentially, a proposition is just a string or an identifier, but using the
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   384
  specific parser function @{ML prop in OuterParse} leads to more instructive
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   385
  error messages, since the parser will complain that a proposition was expected
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   386
  when something else than a string or identifier is found.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   387
  An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   388
  can be parsed using @{ML opt_target in OuterParse}.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   389
  The lists of names of the predicates and parameters, together with optional
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   390
  types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   391
  and @{ML for_fixes in OuterParse}, respectively.
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   392
  In addition, the following function from @{ML_struct SpecParse} for parsing
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   393
  an optional theorem name and attribute, followed by a delimiter, will be useful:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   394
  
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   395
  \begin{table}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   396
  @{ML "opt_thm_name:
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
   397
  string -> Attrib.binding parser" in SpecParse}
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   398
  \end{table}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   399
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   400
  We now have all the necessary tools to write the parser for our
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   401
  \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   402
  
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 113
diff changeset
   403
 
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   404
  Once all arguments of the command have been parsed, we apply the function
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   405
  @{ML add_inductive in SimpleInductivePackage}, which yields a local theory
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   406
  transformer of type @{ML_type "local_theory -> local_theory"}. Commands in
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   407
  Isabelle/Isar are realized by transition transformers of type
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   408
  @{ML_type [display] "Toplevel.transition -> Toplevel.transition"}
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   409
  We can turn a local theory transformer into a transition transformer by using
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   410
  the function
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   411
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   412
  @{ML [display] "Toplevel.local_theory : string option ->
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   413
  (local_theory -> local_theory) ->
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   414
  Toplevel.transition -> Toplevel.transition"}
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   415
 
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   416
  which, apart from the local theory transformer, takes an optional name of a locale
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   417
  to be used as a basis for the local theory. 
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 55
diff changeset
   418
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   419
  (FIXME : needs to be adjusted to new parser type)
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 55
diff changeset
   420
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   421
  {\it
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   422
  The whole parser for our command has type
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 88
diff changeset
   423
  @{text [display] "OuterLex.token list ->
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   424
  (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"}
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 88
diff changeset
   425
  which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   426
  to the system via the function
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 88
diff changeset
   427
  @{text [display] "OuterSyntax.command :
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   428
  string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"}
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   429
  which imperatively updates the parser table behind the scenes. }
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 55
diff changeset
   430
88
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   431
  In addition to the parser, this
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   432
  function takes two strings representing the name of the command and a short description,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   433
  as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   434
  command we intend to add. Since we want to add a command for declaring new concepts,
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   435
  we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   436
  @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword},
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   437
  but requires the user to prove a goal before making the declaration, or
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   438
  @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   439
  not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   440
  by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   441
  to prove that a given set of equations is non-overlapping and covers all cases. The kind
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   442
  of the command should be chosen with care, since selecting the wrong one can cause strange
ebbd0dd008c8 adaptation of the package chapter to fit the rest
Christian Urban <urbanc@in.tum.de>
parents: 76
diff changeset
   443
  behaviour of the user interface, such as failure of the undo mechanism.
32
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   444
*}
5bb2d29553c2 Added new chapter about writing packages.
berghofe
parents:
diff changeset
   445
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   446
text {*
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   447
  Note that the @{text trcl} predicate has two different kinds of parameters: the
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   448
  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   449
  the second and third parameter changes in the ``recursive call''. This will
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   450
  become important later on when we deal with fixed parameters and locales. 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   451
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   452
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   453
 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   454
  The purpose of the package we show next is that the user just specifies the
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   455
  inductive predicate by stating some introduction rules and then the packages
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   456
  makes the equivalent definition and derives from it the needed properties.
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   457
*}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   458
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   459
text {*
212
ac01ddb285f6 polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
   460
  (FIXME: perhaps move somewhere else)
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   461
212
ac01ddb285f6 polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
   462
  The point of these examples is to get a feeling what the automatic proofs 
ac01ddb285f6 polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
   463
  should do in order to solve all inductive definitions we throw at them. For this 
ac01ddb285f6 polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
   464
  it is instructive to look at the general construction principle 
ac01ddb285f6 polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
   465
  of inductive definitions, which we shall do in the next section.
215
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
   466
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
   467
  The code of the inductive package falls roughly in tree parts: the first
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
   468
  deals with the definitions, the second with the induction principles and 
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
   469
  the third with the introduction rules. 
8d1a344a621e more work on the inductive package
Christian Urban <urbanc@in.tum.de>
parents: 212
diff changeset
   470
  
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   471
*}
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   472
(*<*)end(*>*)