src/HOL/Subst/UTerm.ML

New version, modified by Konrad Slind and LCP for TFL

(*  Title:      HOL/Subst/UTerm.ML
    ID:         $Id$
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Simple term structure for unifiation.
Binary trees with leaves that are constants or variables.
*)

open UTerm;


(**** vars_of lemmas  ****)

goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)";
by (Simp_tac 1);
by (fast_tac HOL_cs 1);
qed "vars_var_iff";

goal UTerm.thy  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
by (induct_tac "t" 1);
by (ALLGOALS Simp_tac);
by (fast_tac HOL_cs 1);
qed "vars_iff_occseq";


(* Not used, but perhaps useful in other proofs *)
goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)";
by (induct_tac "N" 1);
by (ALLGOALS Asm_simp_tac);
by (fast_tac set_cs 1);
val occs_vars_subset = result();


goal UTerm.thy "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)";
by (Blast_tac 1);
val monotone_vars_of = result();

goal UTerm.thy "finite(vars_of M)";
by (induct_tac"M" 1);
by (ALLGOALS Simp_tac);
by (forward_tac [finite_UnI] 1);
by (assume_tac 1);
by (Asm_simp_tac 1);
val finite_vars_of = result();