src/HOL/Subst/UTerm.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 7499 23e090051cb8
permissions -rw-r--r--
import -> imports
clasohm@1465
     1
(*  Title:      HOL/Subst/UTerm.ML
clasohm@1266
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
clasohm@968
     6
Simple term structure for unifiation.
clasohm@968
     7
Binary trees with leaves that are constants or variables.
clasohm@968
     8
*)
clasohm@968
     9
clasohm@968
    10
open UTerm;
clasohm@968
    11
clasohm@968
    12
paulson@3192
    13
(**** vars_of lemmas  ****)
clasohm@968
    14
wenzelm@5069
    15
Goal "(v : vars_of(Var(w))) = (w=v)";
paulson@3192
    16
by (Simp_tac 1);
paulson@3192
    17
by (fast_tac HOL_cs 1);
paulson@3192
    18
qed "vars_var_iff";
clasohm@968
    19
wenzelm@5069
    20
Goal  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
paulson@3192
    21
by (induct_tac "t" 1);
paulson@3192
    22
by (ALLGOALS Simp_tac);
paulson@3192
    23
by (fast_tac HOL_cs 1);
paulson@3192
    24
qed "vars_iff_occseq";
clasohm@968
    25
clasohm@968
    26
paulson@3192
    27
(* Not used, but perhaps useful in other proofs *)
wenzelm@5069
    28
Goal "M<:N --> vars_of(M) <= vars_of(N)";
paulson@3192
    29
by (induct_tac "N" 1);
paulson@3192
    30
by (ALLGOALS Asm_simp_tac);
paulson@3192
    31
by (fast_tac set_cs 1);
paulson@3192
    32
val occs_vars_subset = result();
clasohm@968
    33
clasohm@968
    34
wenzelm@5069
    35
Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)";
paulson@3192
    36
by (Blast_tac 1);
paulson@3192
    37
val monotone_vars_of = result();
clasohm@968
    38
wenzelm@5069
    39
Goal "finite(vars_of M)";
paulson@3192
    40
by (induct_tac"M" 1);
paulson@3192
    41
by (ALLGOALS Simp_tac);
wenzelm@7499
    42
by (ftac finite_UnI 1);
paulson@3192
    43
by (assume_tac 1);
paulson@3192
    44
by (Asm_simp_tac 1);
paulson@3192
    45
val finite_vars_of = result();