CookBook/Recipes/NamedThms.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 06 Oct 2008 10:11:08 -0400
changeset 20 5ae6a1bb91c9
parent 15 9da9ba2b095b
child 25 e2f9f94b26d4
permissions -rw-r--r--
some slight polishing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
theory NamedThms
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
imports Main
15
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
     4
uses "antiquote_setup.ML"
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
     5
     "antiquote_setup_plus.ML"
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
begin
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
13
2b07da8b310d polished and added a subdirectory for the recipes
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
     8
section {* Accumulate a List of Theorems under a Name *} 
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents: 0
diff changeset
     9
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
text {*
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    12
  {\bf Problem:} 
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    13
  Your tool @{text foo} works with special rules, called @{text foo}-rules.
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  Users should be able to declare @{text foo}-rules in the theory,
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    15
  which are then used by some method.\smallskip
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    17
  {\bf Solution:} This can be achieved using 
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
  *}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
ML {*
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
  structure FooRules = NamedThmsFun(
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
    val name = "foo" 
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
    val description = "Rules for foo"
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  );
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
*}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
setup FooRules.setup
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
text {*
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    30
  This code declares a context data slot where the theorems are stored,
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    32
  to adding and deleting theorems) and an internal ML interface to retrieve and 
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    33
  modify the theorems.
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    35
  Furthermore, the facts are made available on the user level under the dynamic 
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    36
  fact name @{text foo}. For example:
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
*}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
lemma rule1[foo]: "A" sorry
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
lemma rule2[foo]: "B" sorry
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
declare rule1[foo del]
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
thm foo
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    46
text {* 
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    47
  In an ML-context the rules marked with @{text "foo"} an be retrieved
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    48
  using
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
*}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
20
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    51
ML {* FooRules.get @{context} *}
5ae6a1bb91c9 some slight polishing
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    52
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
text {* 
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  \begin{readmore}
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    56
  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
  \end{readmore}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
 *}
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
15
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    60
text {*
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    61
  (FIXME: maybe add a comment about the case when the theorems 
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    62
  to be added need to satisfy certain properties)
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    63
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    64
*}
9da9ba2b095b added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents: 14
diff changeset
    65
0
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
end
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
  
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
02503850a8cf initial commit of Alexander's files
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71