src/HOL/Subst/UTLemmas.thy
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1476 608483c2122a
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
clasohm@1476
     1
(*  Title:      Substitutions/utermlemmas.thy
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
Additional definitions for uterms that are not part of the basic inductive definition.
clasohm@968
     6
*)
clasohm@968
     7
clasohm@968
     8
UTLemmas = UTerm + Setplus +
clasohm@968
     9
clasohm@968
    10
consts
clasohm@968
    11
clasohm@1381
    12
  vars_of       ::   'a uterm=>'a set
clasohm@1381
    13
  "<:"          ::   ['a uterm,'a uterm]=>bool   (infixl 54) 
clasohm@968
    14
clasohm@968
    15
rules  (*Definitions*)
clasohm@968
    16
clasohm@968
    17
  vars_of_def   "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)"
clasohm@968
    18
  occs_def      "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)"
clasohm@968
    19
clasohm@968
    20
end