|
1476
|
1 |
(* Title: Substitutions/utermlemmas.thy
|
|
|
2 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
968
|
3 |
Copyright 1993 University of Cambridge
|
|
|
4 |
|
|
|
5 |
Additional definitions for uterms that are not part of the basic inductive definition.
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
UTLemmas = UTerm + Setplus +
|
|
|
9 |
|
|
|
10 |
consts
|
|
|
11 |
|
|
1381
|
12 |
vars_of :: 'a uterm=>'a set
|
|
|
13 |
"<:" :: ['a uterm,'a uterm]=>bool (infixl 54)
|
|
968
|
14 |
|
|
|
15 |
rules (*Definitions*)
|
|
|
16 |
|
|
|
17 |
vars_of_def "vars_of(t) == uterm_rec t (%x.{x}) (%x.{}) (%u v q r.q Un r)"
|
|
|
18 |
occs_def "s <: t == uterm_rec t (%x.False) (%x.False) (%u v q r.s=u | s=v | q | r)"
|
|
|
19 |
|
|
|
20 |
end
|