author | wenzelm |
Tue, 07 Sep 1999 10:40:58 +0200 | |
changeset 7499 | 23e090051cb8 |
parent 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Subst/UTerm.ML |
1266 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 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 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
13 |
(**** vars_of lemmas ****) |
968 | 14 |
|
5069 | 15 |
Goal "(v : vars_of(Var(w))) = (w=v)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
16 |
by (Simp_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
17 |
by (fast_tac HOL_cs 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
18 |
qed "vars_var_iff"; |
968 | 19 |
|
5069 | 20 |
Goal "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
21 |
by (induct_tac "t" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
22 |
by (ALLGOALS Simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
23 |
by (fast_tac HOL_cs 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
24 |
qed "vars_iff_occseq"; |
968 | 25 |
|
26 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
27 |
(* Not used, but perhaps useful in other proofs *) |
5069 | 28 |
Goal "M<:N --> vars_of(M) <= vars_of(N)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
29 |
by (induct_tac "N" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
30 |
by (ALLGOALS Asm_simp_tac); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
31 |
by (fast_tac set_cs 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
32 |
val occs_vars_subset = result(); |
968 | 33 |
|
34 |
||
5069 | 35 |
Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
36 |
by (Blast_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
37 |
val monotone_vars_of = result(); |
968 | 38 |
|
5069 | 39 |
Goal "finite(vars_of M)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
40 |
by (induct_tac"M" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
41 |
by (ALLGOALS Simp_tac); |
7499 | 42 |
by (ftac finite_UnI 1); |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
43 |
by (assume_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
44 |
by (Asm_simp_tac 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
2903
diff
changeset
|
45 |
val finite_vars_of = result(); |