Subst/ROOT.ML
author clasohm
Thu, 16 Sep 1993 12:21:07 +0200
changeset 0 7949f97df77a
child 8 8dd033c3ffbc
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/Subst
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    Author: 	Martin Coen, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
Substitution and Unification in Higher-Order Logic. 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
Implements Manna & Waldinger's formalization, with Paulson's simplifications:
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
SCP 1 (1981), 5-48
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    14
setplus      -  minor additions to HOL's set theory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
alist        -  association lists
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    16
uterm        -  inductive data type of terms
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    17
utermlemmas  -  definition of occurs and vars_of for terms
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    18
subst        -  substitutions
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    19
unifier      -  specification of unification and conditions for 
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    20
                correctness and termination
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    21
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    22
To load, go to the parent directory and type use"Substitutions/ROOT.ML";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    24
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    25
HOL_build_completed;    (*Cause examples to fail if HOL did*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    26
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    27
writeln"Root file for Substitutions and Unification";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
use_thy "Subst/setplus";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    29
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    30
use_thy "Subst/alist";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    31
use_thy "Subst/uterm";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    32
use_thy "Subst/utermlemmas";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    34
use_thy "Subst/subst";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    35
use_thy "Subst/unifier";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    36
writeln"END: Root file for Substitutions and Unification";