equal
deleted
inserted
replaced
1 (* Title: HOL/Subst/UTerm.ML |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Simple term structure for unifiation. |
|
7 Binary trees with leaves that are constants or variables. |
|
8 *) |
|
9 |
|
10 open UTerm; |
|
11 |
|
12 |
|
13 (**** vars_of lemmas ****) |
|
14 |
|
15 Goal "(v : vars_of(Var(w))) = (w=v)"; |
|
16 by (Simp_tac 1); |
|
17 by (fast_tac HOL_cs 1); |
|
18 qed "vars_var_iff"; |
|
19 |
|
20 Goal "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; |
|
21 by (induct_tac "t" 1); |
|
22 by (ALLGOALS Simp_tac); |
|
23 by (fast_tac HOL_cs 1); |
|
24 qed "vars_iff_occseq"; |
|
25 |
|
26 |
|
27 (* Not used, but perhaps useful in other proofs *) |
|
28 Goal "M<:N --> vars_of(M) <= vars_of(N)"; |
|
29 by (induct_tac "N" 1); |
|
30 by (ALLGOALS Asm_simp_tac); |
|
31 by (fast_tac set_cs 1); |
|
32 val occs_vars_subset = result(); |
|
33 |
|
34 |
|
35 Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; |
|
36 by (Blast_tac 1); |
|
37 val monotone_vars_of = result(); |
|
38 |
|
39 Goal "finite(vars_of M)"; |
|
40 by (induct_tac"M" 1); |
|
41 by (ALLGOALS Simp_tac); |
|
42 by (ftac finite_UnI 1); |
|
43 by (assume_tac 1); |
|
44 by (Asm_simp_tac 1); |
|
45 val finite_vars_of = result(); |
|