TFL/examples/Subst/UTerm.ML

fixed pris of binder syntax;

(*  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 (uterm.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 (uterm.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(Comb M P) Un vars_of(Comb N Q)";
by (Simp_tac  1);
by (fast_tac set_cs 1);
val monotone_vars_of = result();

goal UTerm.thy "finite(vars_of M)";
by (uterm.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();