TFL/examples/Subst/UTerm.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/examples/Subst/UTerm.ML	Fri Oct 18 12:54:19 1996 +0200
@@ -0,0 +1,47 @@
+(*  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();