CookBook/FirstSteps.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 06 Mar 2009 21:52:17 +0000
changeset 162 3fb9f820a294
parent 161 83f36a1c62f2
child 163 2319cff107f0
permissions -rw-r--r--
some additions to the simplifier section and general tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory FirstSteps
25
e2f9f94b26d4 Antiquotation setup is now contained in theory Base.
berghofe
parents: 21
diff changeset
     2
imports Base
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
chapter {* First Steps *}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
     7
text {*
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
     8
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
     9
  Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
    10
  in Isabelle is part of a theory. If you want to follow the code given in
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
    11
  this chapter, we assume you are working inside the theory starting with
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
6
007e09485351 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
    13
  \begin{center}
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    14
  \begin{tabular}{@ {}l}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
    15
  \isacommand{theory} FirstSteps\\
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    16
  \isacommand{imports} Main\\
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    17
  \isacommand{begin}\\
6
007e09485351 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
    18
  \ldots
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    19
  \end{tabular}
6
007e09485351 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
    20
  \end{center}
157
76cdc8f562fc added more to the simplifier section
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
    21
76cdc8f562fc added more to the simplifier section
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
    22
  We also generally assume you are working with HOL. The given examples might
76cdc8f562fc added more to the simplifier section
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
    23
  need to be adapted slightly if you work in a different logic.
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    24
*}
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    25
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 19
diff changeset
    26
section {* Including ML-Code *}
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    27
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    28
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    29
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    30
text {*
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    31
  The easiest and quickest way to include code in a theory is
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
    32
  by using the \isacommand{ML}-command. For example:
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
    34
\begin{isabelle}
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
    35
\begin{graybox}
85
b02904872d6b better handling of {* and *}
Christian Urban <urbanc@in.tum.de>
parents: 84
diff changeset
    36
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
    37
\hspace{5mm}@{ML "3 + 4"}\isanewline
85
b02904872d6b better handling of {* and *}
Christian Urban <urbanc@in.tum.de>
parents: 84
diff changeset
    38
@{text "\<verbclose>"}\isanewline
b02904872d6b better handling of {* and *}
Christian Urban <urbanc@in.tum.de>
parents: 84
diff changeset
    39
@{text "> 7"}\smallskip
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
    40
\end{graybox}
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
    41
\end{isabelle}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    43
  Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    44
  evaluated by using the advance and undo buttons of your Isabelle
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    45
  environment. The code inside the \isacommand{ML}-command can also contain
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    46
  value and function bindings, and even those can be undone when the proof
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
    47
  script is retracted. As mentioned in the Introduction, we will drop the
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    48
  \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
107
258ce361ba1b polished and more material in the tactic chapter
Christian Urban <urbanc@in.tum.de>
parents: 104
diff changeset
    49
  show code. The lines prefixed with @{text [quotes] ">"} are not part of the
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    50
  code, rather they indicate what the response is when the code is evaluated.
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    51
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    52
  Once a portion of code is relatively stable, you usually want to export it
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    53
  to a separate ML-file. Such files can then be included in a theory by using
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
    54
  the \isacommand{uses}-command in the header of the theory, like:
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    55
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    56
  \begin{center}
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    57
  \begin{tabular}{@ {}l}
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
    58
  \isacommand{theory} FirstSteps\\
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    59
  \isacommand{imports} Main\\
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
    60
  \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    61
  \isacommand{begin}\\
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    62
  \ldots
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    63
  \end{tabular}
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    64
  \end{center}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
    65
  
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    66
*}
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    67
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
    68
section {* Debugging and Printing\label{sec:printing} *}
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    69
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    70
text {*
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
    71
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    72
  During development you might find it necessary to inspect some data
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    73
  in your code. This can be done in a ``quick-and-dirty'' fashion using 
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
    74
  the function @{ML "warning"}. For example 
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    75
161
83f36a1c62f2 rolled back the changes on the function warning and tracing
Christian Urban <urbanc@in.tum.de>
parents: 160
diff changeset
    76
  @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    77
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
    78
  will print out @{text [quotes] "any string"} inside the response buffer
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
    79
  of Isabelle.  This function expects a string as argument. If you develop under PolyML,
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    80
  then there is a convenient, though again ``quick-and-dirty'', method for
107
258ce361ba1b polished and more material in the tactic chapter
Christian Urban <urbanc@in.tum.de>
parents: 104
diff changeset
    81
  converting values into strings, namely the function @{ML makestring}:
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    82
161
83f36a1c62f2 rolled back the changes on the function warning and tracing
Christian Urban <urbanc@in.tum.de>
parents: 160
diff changeset
    83
  @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
    84
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
    85
  However @{ML makestring} only works if the type of what is converted is monomorphic 
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
    86
  and not a function.
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
    87
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
    88
  The function @{ML "warning"} should only be used for testing purposes, because any
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
    89
  output this function generates will be overwritten as soon as an error is
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    90
  raised. For printing anything more serious and elaborate, the
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
    91
  function @{ML tracing} is more appropriate. This function writes all output into
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
    92
  a separate tracing buffer. For example:
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    93
161
83f36a1c62f2 rolled back the changes on the function warning and tracing
Christian Urban <urbanc@in.tum.de>
parents: 160
diff changeset
    94
  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
    95
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
    96
  It is also possible to redirect the ``channel'' where the string @{text "foo"} is 
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
    97
  printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 
107
258ce361ba1b polished and more material in the tactic chapter
Christian Urban <urbanc@in.tum.de>
parents: 104
diff changeset
    98
  amounts of trace output. This redirection can be achieved with the code:
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
    99
*}
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
   100
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   101
ML{*val strip_specials =
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   102
let
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   103
  fun strip ("\^A" :: _ :: cs) = strip cs
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   104
    | strip (c :: cs) = c :: strip cs
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   105
    | strip [] = [];
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   106
in implode o strip o explode end;
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   107
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   108
fun redirect_tracing stream =
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   109
 Output.tracing_fn := (fn s =>
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
   110
    (TextIO.output (stream, (strip_specials s));
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   111
     TextIO.output (stream, "\n");
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   112
     TextIO.flushOut stream)) *}
14
1c17e99f6f66 added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
parents: 13
diff changeset
   113
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   114
text {*
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   115
  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   116
  will cause that all tracing information is printed into the file @{text "foo.bar"}.
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   117
107
258ce361ba1b polished and more material in the tactic chapter
Christian Urban <urbanc@in.tum.de>
parents: 104
diff changeset
   118
  You can print out error messages with the function @{ML error}; for example:
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   119
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   120
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   121
"Exception- ERROR \"foo\" raised
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   122
At command \"ML\"."}
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   123
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   124
  Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   125
  or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   126
  but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   127
  a term into a string is to use the function @{ML Syntax.string_of_term}.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   128
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   129
  @{ML_response_fake [display,gray]
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   130
  "Syntax.string_of_term @{context} @{term \"1::nat\"}"
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   131
  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   132
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   133
  This produces a string with some additional information encoded in it. The string
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   134
  can be properly printed by using the function @{ML warning}.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   135
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   136
  @{ML_response_fake [display,gray]
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   137
  "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   138
  "\"1\""}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   139
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   140
  A @{ML_type cterm} can be transformed into a string by the following function.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   141
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   142
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   143
ML{*fun str_of_cterm ctxt t =  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   144
   Syntax.string_of_term ctxt (term_of t)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   145
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   146
text {*
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   147
  In this example the function @{ML term_of} extracts the @{ML_type term} from
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   148
  a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   149
  printed, you can use the function @{ML commas} to separate them.
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   150
*} 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   151
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   152
ML{*fun str_of_cterms ctxt ts =  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   153
   commas (map (str_of_cterm ctxt) ts)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   154
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   155
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   156
  The easiest way to get the string of a theorem is to transform it
158
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   157
  into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   158
  also include schematic variables, such as @{text "?P"}, @{text "?Q"}
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   159
  and so on. In order to improve the readability of theorems we convert
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   160
  these schematic variables into free variables using the 
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   161
  function @{ML Variable.import_thms}.
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   162
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   163
158
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   164
ML{*fun no_vars ctxt thm =
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   165
let 
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   166
  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   167
in
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   168
  thm'
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   169
end
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   170
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   171
fun str_of_thm ctxt thm =
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   172
let
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   173
  val {prop, ...} = crep_thm (no_vars ctxt thm)
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   174
in 
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   175
  str_of_cterm ctxt prop
d7944bdf7b3f removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
parents: 157
diff changeset
   176
end*}
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   177
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   178
text {* 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   179
  Again the function @{ML commas} helps with printing more than one theorem. 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   180
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   181
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   182
ML{*fun str_of_thms ctxt thms =  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   183
  commas (map (str_of_thm ctxt) thms)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   184
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   185
section {* Combinators\label{sec:combinators} *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   186
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   187
text {*
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   188
  For beginners perhaps the most puzzling parts in the existing code of Isabelle are
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   189
  the combinators. At first they seem to greatly obstruct the
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   190
  comprehension of the code, but after getting familiar with them, they
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   191
  actually ease the understanding and also the programming.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   192
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   193
  The simplest combinator is @{ML I}, which is just the identity function defined as
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   194
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   195
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   196
ML{*fun I x = x*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   197
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   198
text {* Another simple combinator is @{ML K}, defined as *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   199
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   200
ML{*fun K x = fn _ => x*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   201
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   202
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   203
  @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   204
  function ignores its argument. As a result, @{ML K} defines a constant function 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   205
  always returning @{text x}.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   206
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   207
  The next combinator is reverse application, @{ML "|>"}, defined as: 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   208
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   209
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   210
ML{*fun x |> f = f x*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   211
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   212
text {* While just syntactic sugar for the usual function application,
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   213
  the purpose of this combinator is to implement functions in a  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   214
  ``waterfall fashion''. Consider for example the function *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   215
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   216
ML %linenosgray{*fun inc_by_five x =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   217
  x |> (fn x => x + 1)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   218
    |> (fn x => (x, x))
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   219
    |> fst
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   220
    |> (fn x => x + 4)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   221
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   222
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   223
  which increments its argument @{text x} by 5. It does this by first incrementing 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   224
  the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   225
  the first component of the pair (Line 4) and finally incrementing the first 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   226
  component by 4 (Line 5). This kind of cascading manipulations of values is quite
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   227
  common when dealing with theories (for example by adding a definition, followed by
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   228
  lemmas and so on). The reverse application allows you to read what happens in 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   229
  a top-down manner. This kind of coding should also be familiar, 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   230
  if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using 
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   231
  the reverse application is much clearer than writing
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   232
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   233
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   234
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   235
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   236
text {* or *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   237
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   238
ML{*fun inc_by_five x = 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   239
       ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   240
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   241
text {* and typographically more economical than *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   242
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   243
ML{*fun inc_by_five x =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   244
   let val y1 = x + 1
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   245
       val y2 = (y1, y1)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   246
       val y3 = fst y2
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   247
       val y4 = y3 + 4
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   248
   in y4 end*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   249
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   250
text {* 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   251
  Another reason why the let-bindings in the code above are better to be
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   252
  avoided: it is more than easy to get the intermediate values wrong, not to 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   253
  mention the nightmares the maintenance of this code causes!
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   254
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   255
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   256
  (FIXME: give a real world example involving theories)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   257
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   258
  Similarly, the combinator @{ML "#>"} is the reverse function 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   259
  composition. It can be used to define the following function
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   260
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   261
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   262
ML{*val inc_by_six = 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   263
      (fn x => x + 1)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   264
   #> (fn x => x + 2)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   265
   #> (fn x => x + 3)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   266
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   267
text {* 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   268
  which is the function composed of first the increment-by-one function and then
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   269
  increment-by-two, followed by increment-by-three. Again, the reverse function 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   270
  composition allows you to read the code top-down.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   271
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   272
  The remaining combinators described in this section add convenience for the
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   273
  ``waterfall method'' of writing functions. The combinator @{ML tap} allows
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   274
  you to get hold of an intermediate result (to do some side-calculations for
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   275
  instance). The function
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   276
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   277
 *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   278
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   279
ML %linenosgray{*fun inc_by_three x =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   280
     x |> (fn x => x + 1)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   281
       |> tap (fn x => tracing (makestring x))
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   282
       |> (fn x => x + 2)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   283
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   284
text {* 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   285
  increments the argument first by @{text "1"} and then by @{text "2"}. In the
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   286
  middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   287
  intermediate result inside the tracing buffer. The function @{ML tap} can
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   288
  only be used for side-calculations, because any value that is computed
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   289
  cannot be merged back into the ``main waterfall''. To do this, you can use
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   290
  the next combinator.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   291
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   292
  The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   293
  and returns the result together with the value (as a pair). For example
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   294
  the function 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   295
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   296
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   297
ML{*fun inc_as_pair x =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   298
     x |> `(fn x => x + 1)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   299
       |> (fn (x, y) => (x, y + 1))*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   300
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   301
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   302
  takes @{text x} as argument, and then increments @{text x}, but also keeps
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   303
  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   304
  for x}. After that, the function increments the right-hand component of the
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   305
  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   306
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   307
  The combinators @{ML "|>>"} and @{ML "||>"} are defined for 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   308
  functions manipulating pairs. The first applies the function to
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   309
  the first component of the pair, defined as
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   310
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   311
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   312
ML{*fun (x, y) |>> f = (f x, y)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   313
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   314
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   315
  and the second combinator to the second component, defined as
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   316
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   317
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   318
ML{*fun (x, y) ||> f = (x, f y)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   319
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   320
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   321
  With the combinator @{ML "|->"} you can re-combine the elements from a pair.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   322
  This combinator is defined as
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   323
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   324
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   325
ML{*fun (x, y) |-> f = f x y*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   326
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   327
text {* and can be used to write the following roundabout version 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   328
  of the @{text double} function: 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   329
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   330
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   331
ML{*fun double x =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   332
      x |>  (fn x => (x, x))
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   333
        |-> (fn x => fn y => x + y)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   334
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   335
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   336
  Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   337
  reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   338
  @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   339
  composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   340
  for example, the function @{text double} can also be written as:
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   341
*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   342
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   343
ML{*val double =
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   344
            (fn x => (x, x))
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   345
        #-> (fn x => fn y => x + y)*}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   346
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   347
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   348
  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   349
  (FIXME: find a good exercise for combinators)
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   350
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   351
  \begin{readmore}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   352
  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   353
  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   354
  contains further information about combinators.
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   355
  \end{readmore}
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   356
 
15
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
   357
*}
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
   358
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   359
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   360
section {* Antiquotations *}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   361
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   362
text {*
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   363
  The main advantage of embedding all code in a theory is that the code can
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   364
  contain references to entities defined on the logical level of Isabelle. By
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   365
  this we mean definitions, theorems, terms and so on. This kind of reference is
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   366
  realised with antiquotations.  For example, one can print out the name of the current
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   367
  theory by typing
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   368
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   369
  
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   370
  @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   371
 
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   372
  where @{text "@{theory}"} is an antiquotation that is substituted with the
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   373
  current theory (remember that we assumed we are inside the theory 
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   374
  @{text FirstSteps}). The name of this theory can be extracted using
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   375
  the function @{ML "Context.theory_name"}. 
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   376
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   377
  Note, however, that antiquotations are statically linked, that is their value is
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   378
  determined at ``compile-time'', not ``run-time''. For example the function
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   379
*}
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   380
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   381
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   382
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   383
text {*
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   384
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   385
  does \emph{not} return the name of the current theory, if it is run in a 
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   386
  different theory. Instead, the code above defines the constant function 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   387
  that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   388
  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   389
  \emph{not} replaced with code that will look up the current theory in 
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   390
  some data structure and return it. Instead, it is literally
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
   391
  replaced with the value representing the theory name.
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   392
132
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   393
  In a similar way you can use antiquotations to refer to proved theorems: 
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   394
  @{text "@{thm \<dots>}"} for a single theorem
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   395
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   396
  @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   397
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   398
  and @{text "@{thms \<dots>}"} for more than one
132
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   399
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   400
@{ML_response_fake [display,gray] "@{thms conj_ac}" 
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   401
"(?P \<and> ?Q) = (?Q \<and> ?P)
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   402
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   403
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   404
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   405
  You can also refer to the current simpset. To illustrate this we implement the
132
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   406
  function that extracts the theorem names stored in a simpset.
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   407
*}
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   408
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   409
ML{*fun get_thm_names_from_ss simpset =
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   410
let
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   411
  val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
70
bbb2d5f1d58d deleted the fixme about simpsets
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   412
in
bbb2d5f1d58d deleted the fixme about simpsets
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   413
  map #name (Net.entries rules)
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   414
end*}
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   415
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   416
text {*
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   417
  The function @{ML rep_ss in MetaSimplifier} returns a record containing all
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   418
  information about the simpset. The rules of a simpset are stored in a
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   419
  \emph{discrimination net} (a data structure for fast indexing). From this
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   420
  net you can extract the entries using the function @{ML Net.entries}.
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   421
  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   422
  in the current simpset. This simpset can be referred to using the antiquotation
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   423
  @{text "@{simpset}"}.
81
8fda6b452f28 polished
Christian Urban <urbanc@in.tum.de>
parents: 78
diff changeset
   424
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   425
  @{ML_response_fake [display,gray] 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   426
  "get_thm_names_from_ss @{simpset}" 
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   427
  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   428
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   429
  Again, this way or referencing simpsets makes you independent from additions
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   430
  of lemmas to the simpset by the user that potentially cause loops.
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   431
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   432
  While antiquotations have many applications, they were originally introduced in order 
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   433
  to avoid explicit bindings for theorems such as:
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   434
*}
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   435
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   436
ML{*val allI = thm "allI" *}
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   437
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   438
text {*
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   439
  These bindings are difficult to maintain and also can be accidentally
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   440
  overwritten by the user. This often broke Isabelle
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   441
  packages. Antiquotations solve this problem, since they are ``linked''
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   442
  statically at compile-time.  However, this static linkage also limits their
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   443
  usefulness in cases where data needs to be build up dynamically. In the
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   444
  course of this chapter you will learn more about these antiquotations:
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   445
  they can simplify Isabelle programming since one can directly access all
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   446
  kinds of logical elements from th ML-level.
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   447
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   448
*}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   449
15
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
   450
section {* Terms and Types *}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   451
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   452
text {*
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   453
  One way to construct terms of Isabelle is by using the antiquotation 
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   454
  \mbox{@{text "@{term \<dots>}"}}. For example:
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   455
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   456
  @{ML_response [display,gray] 
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   457
"@{term \"(a::nat) + b = c\"}" 
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   458
"Const (\"op =\", \<dots>) $ 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   459
  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   460
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   461
  This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   462
  representation of this term. This internal representation corresponds to the 
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   463
  datatype @{ML_type "term"}.
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   464
  
34
527fc0af45e3 Corrected typos.
berghofe
parents: 25
diff changeset
   465
  The internal representation of terms uses the usual de Bruijn index mechanism where bound 
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   466
  variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   467
  the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   468
  binds the corresponding variable. However, in Isabelle the names of bound variables are 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   469
  kept at abstractions for printing purposes, and so should be treated only as ``comments''. 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   470
  Application in Isabelle is realised with the term-constructor @{ML $}.
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   471
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   472
  \begin{readmore}
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   473
  Terms are described in detail in \isccite{sec:terms}. Their
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   474
  definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   475
  \end{readmore}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   476
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   477
  Sometimes the internal representation of terms can be surprisingly different
157
76cdc8f562fc added more to the simplifier section
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
   478
  from what you see at the user-level, because the layers of
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   479
  parsing/type-checking/pretty printing can be quite elaborate. 
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   480
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   481
  \begin{exercise}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   482
  Look at the internal term representation of the following terms, and
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   483
  find out why they are represented like this:
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   484
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   485
  \begin{itemize}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   486
  \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   487
  \item @{term "\<lambda>(x,y). P y x"}  
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   488
  \item @{term "{ [x::int] | x. x \<le> -2 }"}  
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   489
  \end{itemize}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   490
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   491
  Hint: The third term is already quite big, and the pretty printer
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   492
  may omit parts of it by default. If you want to see all of it, you
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   493
  can use the following ML-function to set the printing depth to a higher 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   494
  value:
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   495
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   496
  @{ML [display,gray] "print_depth 50"}
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   497
  \end{exercise}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   498
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   499
  The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   500
  inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   501
  Consider for example the pairs
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   502
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   503
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   504
"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   505
 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   506
 
108
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
parents: 107
diff changeset
   507
  where a coercion is inserted in the second component and 
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   508
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   509
  @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   510
  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   511
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   512
  where it is not (since it is already constructed by a meta-implication). 
19
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   513
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   514
  Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   515
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   516
  @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 34
diff changeset
   517
19
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   518
  \begin{readmore}
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   519
  Types are described in detail in \isccite{sec:types}. Their
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   520
  definition and many useful operations are implemented 
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   521
  in @{ML_file "Pure/type.ML"}.
19
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   522
  \end{readmore}
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   523
*}
19
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   524
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   525
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   526
section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   527
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   528
text {*
81
8fda6b452f28 polished
Christian Urban <urbanc@in.tum.de>
parents: 78
diff changeset
   529
  While antiquotations are very convenient for constructing terms, they can
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   530
  only construct fixed terms (remember they are ``linked'' at compile-time).
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   531
  However, you often need to construct terms dynamically. For example, a
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   532
  function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   533
  @{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   534
  written as:
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   535
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   536
*}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   537
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   538
ML{*fun make_imp P Q tau =
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   539
let
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   540
  val x = Free ("x",tau)
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   541
in 
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   542
  Logic.all x (Logic.mk_implies (P $ x, Q $ x))
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   543
end *}
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   544
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   545
text {*
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   546
  The reason is that you cannot pass the arguments @{term P}, @{term Q} and 
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   547
  @{term "tau"} into an antiquotation. For example the following does \emph{not} work.
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   548
*}
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   549
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   550
ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   551
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   552
text {*
19
34b93dbf8c3c some tuning in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   553
  To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   554
  to both functions. With @{ML make_imp} we obtain the intended term involving 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   555
  the given arguments
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   556
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   557
  @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" 
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   558
"Const \<dots> $ 
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   559
  Abs (\"x\", Type (\"nat\",[]),
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   560
    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   561
81
8fda6b452f28 polished
Christian Urban <urbanc@in.tum.de>
parents: 78
diff changeset
   562
  whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} 
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   563
  and @{text "Q"} from the antiquotation.
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 66
diff changeset
   564
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   565
  @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   566
"Const \<dots> $ 
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   567
  Abs (\"x\", \<dots>,
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   568
    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   569
               (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   570
108
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
parents: 107
diff changeset
   571
  Although types of terms can often be inferred, there are many
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   572
  situations where you need to construct types manually, especially  
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   573
  when defining constants. For example the function returning a function 
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   574
  type is as follows:
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   575
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   576
*} 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   577
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   578
ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   579
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   580
text {* This can be equally written with the combinator @{ML "-->"} as: *}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   581
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   582
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   583
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   584
text {*
134
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   585
  A handy function for manipulating terms is @{ML map_types}: it takes a 
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   586
  function and applies it to every type in a term. You can, for example,
134
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   587
  change every @{typ nat} in a term into an @{typ int} using the function:
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   588
*}
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   589
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   590
ML{*fun nat_to_int t =
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   591
  (case t of
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   592
     @{typ nat} => @{typ int}
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   593
   | Type (s, ts) => Type (s, map nat_to_int ts)
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   594
   | _ => t)*}
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   595
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   596
text {*
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   597
  An example as follows:
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   598
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   599
@{ML_response_fake [display,gray] 
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   600
"map_types nat_to_int @{term \"a = (1::nat)\"}" 
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   601
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   602
           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
328370b75c33 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   603
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   604
  \begin{readmore}
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
   605
  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   606
  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   607
  and types easier.\end{readmore}
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   608
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   609
  Have a look at these files and try to solve the following two exercises:
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   610
*}
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   611
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   612
text {*
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   613
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   614
  \begin{exercise}\label{fun:revsum}
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   615
  Write a function @{text "rev_sum : term -> term"} that takes a
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   616
  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   617
  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   618
  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   619
  associates to the left. Try your function on some examples. 
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   620
  \end{exercise}
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   621
15
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
   622
  \begin{exercise}\label{fun:makesum}
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   623
  Write a function which takes two terms representing natural numbers
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   624
  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   625
  number representing their sum.
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   626
  \end{exercise}
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 10
diff changeset
   627
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   628
  There are a few subtle issues with constants. They usually crop up when
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   629
  pattern matching terms or types, or when constructing them. While it is perfectly ok
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   630
  to write the function @{text is_true} as follows
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   631
*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   632
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   633
ML{*fun is_true @{term True} = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   634
  | is_true _ = false*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   635
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   636
text {*
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   637
  this does not work for picking out @{text "\<forall>"}-quantified terms. Because
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   638
  the function 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   639
*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   640
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   641
ML{*fun is_all (@{term All} $ _) = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   642
  | is_all _ = false*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   643
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   644
text {* 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   645
  will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   646
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   647
  @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   648
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   649
  The problem is that the @{text "@term"}-antiquotation in the pattern 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   650
  fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   651
  an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   652
  for this function is
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   653
*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   654
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   655
ML{*fun is_all (Const ("All", _) $ _) = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   656
  | is_all _ = false*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   657
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   658
text {* 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   659
  because now
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   660
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   661
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   662
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   663
  matches correctly (the first wildcard in the pattern matches any type and the
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   664
  second any term).
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   665
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   666
  However there is still a problem: consider the similar function that
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   667
  attempts to pick out @{text "Nil"}-terms:
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   668
*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   669
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   670
ML{*fun is_nil (Const ("Nil", _)) = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   671
  | is_nil _ = false *}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   672
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   673
text {* 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   674
  Unfortunately, also this function does \emph{not} work as expected, since
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   675
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   676
  @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   677
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   678
  The problem is that on the ML-level the name of a constant is more
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   679
  subtle than you might expect. The function @{ML is_all} worked correctly,
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   680
  because @{term "All"} is such a fundamental constant, which can be referenced
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   681
  by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   682
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   683
  @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   684
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   685
  the name of the constant @{text "Nil"} depends on the theory in which the
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   686
  term constructor is defined (@{text "List"}) and also in which datatype
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   687
  (@{text "list"}). Even worse, some constants have a name involving
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   688
  type-classes. Consider for example the constants for @{term "zero"} and
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   689
  \mbox{@{text "(op *)"}}:
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   690
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   691
  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   692
 "(Const (\"HOL.zero_class.zero\", \<dots>), 
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   693
 Const (\"HOL.times_class.times\", \<dots>))"}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   694
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   695
  While you could use the complete name, for example 
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   696
  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   697
  matching against @{text "Nil"}, this would make the code rather brittle. 
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   698
  The reason is that the theory and the name of the datatype can easily change. 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   699
  To make the code more robust, it is better to use the antiquotation 
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   700
  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   701
  variable parts of the constant's name. Therefore a functions for 
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   702
  matching against constants that have a polymorphic type should 
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   703
  be written as follows.
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   704
*}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   705
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   706
ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   707
  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   708
  | is_nil_or_all _ = false *}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   709
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   710
text {*
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   711
  Occasional you have to calculate what the ``base'' name of a given
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   712
  constant is. For this you can use the function @{ML Sign.extern_const} or
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   713
  @{ML NameSpace.base_name}. For example:
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   714
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   715
  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   716
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   717
  The difference between both functions is that @{ML extern_const in Sign} returns
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   718
  the smallest name that is still unique, whereas @{ML base_name in NameSpace} always
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   719
  strips off all qualifiers.
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   720
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   721
  \begin{readmore}
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   722
  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   723
  functions about signatures in @{ML_file "Pure/sign.ML"}.
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   724
  
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   725
  \end{readmore}
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   726
*}
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   727
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   728
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   729
section {* Type-Checking *}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   730
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   731
text {* 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   732
  
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   733
  You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   734
  typ}es, since they are just arbitrary unchecked trees. However, you
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   735
  eventually want to see if a term is well-formed, or type-checks, relative to
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   736
  a theory.  Type-checking is done via the function @{ML cterm_of}, which
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   737
  converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   738
  term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   739
  abstract objects that are guaranteed to be type-correct, and they can only
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   740
  be constructed via ``official interfaces''.
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   741
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   742
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   743
  Type-checking is always relative to a theory context. For now we use
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   744
  the @{ML "@{theory}"} antiquotation to get hold of the current theory.
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   745
  For example you can write:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   746
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   747
  @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   748
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   749
  This can also be written with an antiquotation:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   750
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   751
  @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   752
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   753
  Attempting to obtain the certified term for
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   754
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   755
  @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   756
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   757
  yields an error (since the term is not typable). A slightly more elaborate
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   758
  example that type-checks is:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   759
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   760
@{ML_response_fake [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   761
"let
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   762
  val natT = @{typ \"nat\"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   763
  val zero = @{term \"0::nat\"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   764
in
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   765
  cterm_of @{theory} 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   766
      (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   767
end" "0 + 0"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   768
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   769
  In Isabelle also types need can be certified. For example, you obtain
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   770
  the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on the ML-level
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   771
  as follows:
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   772
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   773
  @{ML_response_fake [display,gray]
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   774
  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   775
  "nat \<Rightarrow> bool"}
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   776
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   777
  \begin{readmore}
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   778
  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   779
  the file @{ML_file "Pure/thm.ML"}.
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   780
  \end{readmore}
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   781
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   782
  \begin{exercise}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   783
  Check that the function defined in Exercise~\ref{fun:revsum} returns a
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   784
  result that type-checks.
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   785
  \end{exercise}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   786
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   787
  Remember that in Isabelle a term contains enough typing information
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   788
  (constants, free variables and abstractions all have typing 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   789
  information) so that it is always clear what the type of a term is. 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   790
  Given a well-typed term, the function @{ML type_of} returns the 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   791
  type of a term. Consider for example:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   792
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   793
  @{ML_response [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   794
  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   795
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   796
  To calculate the type, this function traverses the whole term and will
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   797
  detect any typing inconsistency. For examle changing the type of the variable 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   798
  @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   799
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   800
  @{ML_response_fake [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   801
  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   802
  "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   803
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   804
  Since the complete traversal might sometimes be too costly and
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   805
  not necessary, there is the function @{ML fastype_of}, which 
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   806
  also returns the type of a term.
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   807
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   808
  @{ML_response [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   809
  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   810
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   811
  However, efficiency is gained on the expense of skiping some tests. You 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   812
  can see this in the following example
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   813
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   814
   @{ML_response [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   815
  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   816
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   817
  where no error is detected.
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   818
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   819
  Sometimes it is a bit inconvenient to construct a term with 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   820
  complete typing annotations, especially in cases where the typing 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   821
  information is redundant. A short-cut is to use the ``place-holder'' 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   822
  type @{ML "dummyT"} and then let type-inference figure out the 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   823
  complete type. An example is as follows:
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   824
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   825
  @{ML_response_fake [display,gray] 
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   826
"let
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   827
  val c = Const (@{const_name \"plus\"}, dummyT) 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   828
  val o = @{term \"1::nat\"} 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   829
  val v = Free (\"x\", dummyT)
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   830
in   
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   831
  Syntax.check_term @{context} (c $ o $ v)
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   832
end"
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   833
"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   834
  Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   835
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   836
  Instead of giving explicitly the type for the constant @{text "plus"} and the free 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   837
  variable @{text "x"}, the type-inference filles in the missing information.
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   838
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   839
  \begin{readmore}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   840
  See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   841
  checking and pretty-printing of terms are defined. Fuctions related to the
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   842
  type inference are implemented in @{ML_file "Pure/type.ML"} and 
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
   843
  @{ML_file "Pure/type_infer.ML"}. 
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   844
  \end{readmore}
162
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   845
3fb9f820a294 some additions to the simplifier section and general tuning
Christian Urban <urbanc@in.tum.de>
parents: 161
diff changeset
   846
  (FIXME: say something about sorts)
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   847
*}
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   848
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   849
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   850
section {* Theorems *}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   851
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   852
text {*
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   853
  Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
122
79696161ae16 polished
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   854
  that can only be build by going through interfaces. As a consequence, every proof 
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   855
  in Isabelle is correct by construction. This follows the tradition of the LCF approach
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 123
diff changeset
   856
  \cite{GordonMilnerWadsworth79}.
107
258ce361ba1b polished and more material in the tactic chapter
Christian Urban <urbanc@in.tum.de>
parents: 104
diff changeset
   857
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   858
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   859
  To see theorems in ``action'', let us give a proof on the ML-level for the following 
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   860
  statement:
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   861
*}
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   862
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   863
  lemma 
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   864
   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   865
   and     assm\<^isub>2: "P t"
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   866
   shows "Q t" (*<*)oops(*>*) 
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   867
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   868
text {*
78
ef778679d3e0 added a section about combinators
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   869
  The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
   870
  application. See Section~\ref{sec:combinators}.}
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   871
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 71
diff changeset
   872
@{ML_response_fake [display,gray]
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   873
"let
138
e4d8dfb7e34a included comment from Sascha
Christian Urban <urbanc@in.tum.de>
parents: 136
diff changeset
   874
  val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
e4d8dfb7e34a included comment from Sascha
Christian Urban <urbanc@in.tum.de>
parents: 136
diff changeset
   875
  val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   876
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   877
  val Pt_implies_Qt = 
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   878
        assume assm1
138
e4d8dfb7e34a included comment from Sascha
Christian Urban <urbanc@in.tum.de>
parents: 136
diff changeset
   879
        |> forall_elim @{cterm \"t::nat\"};
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   880
  
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   881
  val Qt = implies_elim Pt_implies_Qt (assume assm2);
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   882
in
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   883
  Qt 
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   884
  |> implies_intr assm2
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   885
  |> implies_intr assm1
48
609f9ef73494 fixed FIXME's in fake responses
Christian Urban <urbanc@in.tum.de>
parents: 47
diff changeset
   886
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   887
21
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   888
  This code-snippet constructs the following proof:
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   889
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   890
  \[
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   891
  \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   892
    {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   893
       {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   894
          {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   895
                 {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   896
                 &
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   897
           \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   898
          }
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   899
       }
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   900
    }
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   901
  \]
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   902
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   903
  However, while we obtained a theorem as result, this theorem is not
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   904
  yet stored in Isabelle's theorem database. So it cannot be referenced later
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   905
  on. How to store theorems will be explained in Section~\ref{sec:storing}.
21
2356e5c70d98 added a proof and tuned the rest
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   906
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   907
  \begin{readmore}
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   908
  For the functions @{text "assume"}, @{text "forall_elim"} etc 
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   909
  see \isccite{sec:thms}. The basic functions for theorems are defined in
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   910
  @{ML_file "Pure/thm.ML"}. 
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
   911
  \end{readmore}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   912
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   913
  (FIXME: how to add case-names to goal states - maybe in the next section)
10
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   914
*}
df09e49b19bf many changes in the FirstSteps section
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
   915
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   916
section {* Theorem Attributes *}
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   917
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   918
text {*
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   919
  Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   920
  "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   921
  annotated to theorems, but functions that do further processing once a
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   922
  theorem is proven. In particular, it is not possible to find out
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   923
  what are all theorems that have a given attribute in common, unless of course
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   924
  the function behind the attribute stores the theorems in a retrivable 
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   925
  datastructure. 
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   926
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   927
  If you want to print out all currently known attributes a theorem 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   928
  can have, you can use the function:
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   929
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   930
  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   931
"COMP:  direct composition with rules (no lifting)
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   932
HOL.dest:  declaration of Classical destruction rule
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   933
HOL.elim:  declaration of Classical elimination rule 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   934
\<dots>"}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   935
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   936
  To explain how to write your own attribute, let us start with an extremely simple 
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   937
  version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   938
  to produce the ``symmetric'' version of an equation. The main function behind 
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   939
  this attribute is
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   940
*}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   941
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   942
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   943
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   944
text {* 
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   945
  where the function @{ML "Thm.rule_attribute"} expects a function taking a 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   946
  context (which we ignore in the code above) and a theorem (@{text thm}), and 
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   947
  returns another theorem (namely @{text thm} resolved with the lemma 
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   948
  @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
   949
  an attribute.
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   950
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   951
  Before we can use the attribute, we need to set it up. This can be done
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   952
  using the function @{ML Attrib.add_attributes} as follows.
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   953
*}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   954
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   955
setup {*
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   956
  Attrib.add_attributes 
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   957
    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   958
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   959
text {*
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   960
  The attribute does not expect any further arguments (unlike @{text "[OF
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   961
  \<dots>]"}, for example, which can take a list of theorems as argument). Therefore
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   962
  we use the function @{ML Attrib.no_args}. Later on we will also consider
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   963
  attributes taking further arguments. An example for the attribute @{text
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 138
diff changeset
   964
  "[my_sym]"} is the proof
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   965
*} 
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   966
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   967
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   968
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   969
text {*
136
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   970
  which stores the theorem @{thm test} under the name @{thm [source] test}. We 
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   971
  can also use the attribute when referring to this theorem.
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   972
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   973
  \begin{isabelle}
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   974
  \isacommand{thm}~@{text "test[my_sym]"}\\
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   975
  @{text "> "}~@{thm test[my_sym]}
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   976
  \end{isabelle}
58277de8493c to be in sync with Sascha
Christian Urban <urbanc@in.tum.de>
parents: 134
diff changeset
   977
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   978
  The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   979
  Another usage of attributes is to add and delete theorems from stored data.
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   980
  For example the attribute @{text "[simp]"} adds or deletes a theorem from the
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   981
  current simpset. For these applications, you can use @{ML Thm.declaration_attribute}. 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   982
  To illustrate this function, let us introduce a reference containing a list
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   983
  of theorems.
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   984
*}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   985
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   986
ML{*val my_thms = ref ([]:thm list)*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   987
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   988
text {* 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   989
  A word of warning: such references must not be used in any code that
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   990
  is meant to be more than just for testing purposes! Here it is only used 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   991
  to illustrate matters. We will show later how to store data properly without 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   992
  using references. The function @{ML Thm.declaration_attribute} expects us to 
153
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
   993
  provide two functions that add and delete theorems from this list. 
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
   994
  For this we use the two functions:
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   995
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   996
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   997
ML{*fun my_thms_add thm ctxt =
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   998
  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   999
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1000
fun my_thms_del thm ctxt =
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1001
  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1002
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1003
text {*
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1004
  These functions take a theorem and a context and, for what we are explaining
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1005
  here it is sufficient that they just return the context unchanged. They change
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1006
  however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1007
  adds a theorem if it is not already included in the list, and @{ML
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1008
  Thm.del_thm} deletes one. Both functions use the predicate @{ML
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1009
  Thm.eq_thm_prop} which compares theorems according to their proved
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1010
  propositions (modulo alpha-equivalence).
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1011
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1012
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1013
  You can turn both functions into attributes using
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1014
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1015
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1016
ML{*val my_add = Thm.declaration_attribute my_thms_add
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1017
val my_del = Thm.declaration_attribute my_thms_del *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1018
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1019
text {* 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1020
  and set up the attributes as follows
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1021
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1022
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1023
setup {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1024
  Attrib.add_attributes 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1025
    [("my_thms", Attrib.add_del_args my_add my_del, 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1026
        "maintaining a list of my_thms")] *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1027
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1028
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1029
  Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1030
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1031
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1032
lemma trueI_2[my_thms]: "True" by simp
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1033
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1034
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1035
  then you can see the lemma is added to the initially empty list.
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1036
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1037
  @{ML_response_fake [display,gray]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1038
  "!my_thms" "[\"True\"]"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1039
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 158
diff changeset
  1040
  You can also add theorems using the command \isacommand{declare}.
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1041
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1042
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1043
declare test[my_thms] trueI_2[my_thms add]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1044
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1045
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1046
  The @{text "add"} is the default operation and does not need
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1047
  to be given. This declaration will cause the theorem list to be 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1048
  updated as follows.
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1049
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1050
  @{ML_response_fake [display,gray]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1051
  "!my_thms"
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1052
  "[\"True\", \"Suc (Suc 0) = 2\"]"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1053
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1054
  The theorem @{thm [source] trueI_2} only appears once, since the 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1055
  function @{ML Thm.add_thm} tests for duplicates, before extending
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1056
  the list. Deletion from the list works as follows:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1057
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1058
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1059
declare test[my_thms del]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1060
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1061
text {* After this, the theorem list is again: 
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1062
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1063
  @{ML_response_fake [display,gray]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1064
  "!my_thms"
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1065
  "[\"True\"]"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1066
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1067
  We used in this example two functions declared as @{ML Thm.declaration_attribute}, 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1068
  but there can be any number of them. We just have to change the parser for reading
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1069
  the arguments accordingly. 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1070
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1071
  However, as said at the beginning of this example, using references for storing theorems is
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1072
  \emph{not} the received way of doing such things. The received way is to 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1073
  start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1074
*}
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1075
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1076
ML {*structure Data = GenericDataFun
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1077
 (type T = thm list
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1078
  val empty = []
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1079
  val extend = I
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1080
  fun merge _ = Thm.merge_thms) *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1081
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1082
text {*
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1083
  To use this data slot, you only have to change @{ML my_thms_add} and
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1084
  @{ML my_thms_del} to:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1085
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1086
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1087
ML{*val thm_add = Data.map o Thm.add_thm
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1088
val thm_del = Data.map o Thm.del_thm*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1089
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1090
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1091
  where @{ML Data.map} updates the data appropriately in the context. Since storing
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1092
  theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1093
  which does most of the work for you. To obtain such a named theorem lists, you just
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1094
  declare 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1095
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1096
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1097
ML{*structure FooRules = NamedThmsFun 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1098
 (val name = "foo" 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1099
  val description = "Rules for foo"); *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1100
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1101
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1102
  and set up the @{ML_struct FooRules} with the command
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1103
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1104
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1105
setup {* FooRules.setup *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1106
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1107
text {*
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1108
  This code declares a data slot where the theorems are stored,
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1109
  an attribute @{text foo} (with the @{text add} and @{text del} options
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1110
  for adding and deleting theorems) and an internal ML interface to retrieve and 
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1111
  modify the theorems.
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1112
157
76cdc8f562fc added more to the simplifier section
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
  1113
  Furthermore, the facts are made available on the user-level under the dynamic 
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1114
  fact name @{text foo}. For example you can declare three lemmas to be of the kind
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1115
  @{text foo} by:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1116
*}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1117
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1118
lemma rule1[foo]: "A" sorry
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1119
lemma rule2[foo]: "B" sorry
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1120
lemma rule3[foo]: "C" sorry
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1121
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1122
text {* and undeclare the first one by: *}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1123
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1124
declare rule1[foo del]
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1125
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1126
text {* and query the remaining ones with:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1127
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1128
  \begin{isabelle}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1129
  \isacommand{thm}~@{text "foo"}\\
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1130
  @{text "> ?C"}\\
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1131
  @{text "> ?B"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1132
  \end{isabelle}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1133
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1134
  On the ML-level the rules marked with @{text "foo"} can be retrieved
151
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1135
  using the function @{ML FooRules.get}:
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1136
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1137
  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1138
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1139
  \begin{readmore}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1140
  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1141
  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1142
  data.
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1143
  \end{readmore}
7e0bf13bf743 added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
  1144
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 153
diff changeset
  1145
  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1146
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1147
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1148
  \begin{readmore}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1149
  FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1150
  \end{readmore}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1151
*}
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1152
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
  1153
153
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1154
section {* Theories, Contexts and Local Theories (TBD) *}
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
  1155
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1156
text {*
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1157
  (FIXME: expand)
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1158
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1159
  (FIXME: explain \isacommand{setup})
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
  1160
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1161
  There are theories, proof contexts and local theories (in this order, if you
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1162
  want to order them). 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1163
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1164
  In contrast to an ordinary theory, which simply consists of a type
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1165
  signature, as well as tables for constants, axioms and theorems, a local
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1166
  theory also contains additional context information, such as locally fixed
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1167
  variables and local assumptions that may be used by the package. The type
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1168
  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1169
  @{ML_type "Proof.context"}, although not every proof context constitutes a
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1170
  valid local theory.
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1171
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1172
 *}
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1173
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1174
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1175
153
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1176
section {* Storing Theorems\label{sec:storing} (TBD) *}
123
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
  1177
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
  1178
text {* @{ML PureThy.add_thms_dynamic} *}
460bc2ee14e9 some polishing in the first-steps chapter
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
  1179
100
dd8eebae11ec polished
Christian Urban <urbanc@in.tum.de>
parents: 92
diff changeset
  1180
75
Christian Urban <urbanc@in.tum.de>
parents: 73
diff changeset
  1181
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
  1182
(* FIXME: some code below *)
89
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1183
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1184
(*<*)
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1185
setup {*
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1186
 Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] 
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1187
*}
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1188
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1189
lemma "bar = (1::nat)"
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1190
  oops
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1191
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1192
setup {*   
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1193
  Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1194
 #> PureThy.add_defs false [((Binding.name "foo_def", 
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1195
       Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1196
 #> snd
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1197
*}
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1198
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1199
lemma "foo = (1::nat)"
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1200
  apply(simp add: foo_def)
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1201
  done
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1202
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1203
thm foo_def
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1204
(*>*)
fee4942c4770 polishing
Christian Urban <urbanc@in.tum.de>
parents: 87
diff changeset
  1205
153
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1206
section {* Pretty-Printing (TBD) *}
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1207
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1208
text {*
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1209
  @{ML Pretty.big_list}
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1210
*}
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1211
c22b507e1407 general polishing; added versioning to the document
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
  1212
section {* Misc (TBD) *}
92
Christian Urban <urbanc@in.tum.de>
parents: 89
diff changeset
  1213
Christian Urban <urbanc@in.tum.de>
parents: 89
diff changeset
  1214
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
Christian Urban <urbanc@in.tum.de>
parents: 89
diff changeset
  1215
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1216
end