--- a/src/HOL/TLA/Stfun.ML Fri Dec 01 17:22:33 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*
- File: Stfun.ML
- ID: $Id$
- Author: Stephan Merz
- Copyright: 1998 University of Munich
-
-Lemmas and tactics for states and state functions.
-*)
-
-Goalw [basevars_def] "!!vs. basevars vs ==> EX u. vs u = c";
-by (res_inst_tac [("b","c"),("f","vs")] rangeE 1);
-by Auto_tac;
-qed "basevars";
-
-Goal "!!x y. basevars (x,y) ==> basevars x";
-by (simp_tac (simpset() addsimps [basevars_def]) 1);
-by (rtac equalityI 1);
- by (rtac subset_UNIV 1);
-by (rtac subsetI 1);
-by (dres_inst_tac [("c", "(xa, arbitrary)")] basevars 1);
-by Auto_tac;
-qed "base_pair1";
-
-Goal "!!x y. basevars (x,y) ==> basevars y";
-by (simp_tac (simpset() addsimps [basevars_def]) 1);
-by (rtac equalityI 1);
- by (rtac subset_UNIV 1);
-by (rtac subsetI 1);
-by (dres_inst_tac [("c", "(arbitrary, xa)")] basevars 1);
-by Auto_tac;
-qed "base_pair2";
-
-Goal "!!x y. basevars (x,y) ==> basevars x & basevars y";
-by (rtac conjI 1);
-by (etac base_pair1 1);
-by (etac base_pair2 1);
-qed "base_pair";
-
-(* Since the unit type has just one value, any state function can be
- regarded as "base". The following axiom can sometimes be useful
- because it gives a trivial solution for "basevars" premises.
-*)
-Goalw [basevars_def] "basevars (v::unit stfun)";
-by Auto_tac;
-qed "unit_base";
-
-(* [| basevars v; !!x. v x = c ==> Q |] ==> Q *)
-bind_thm("baseE", (standard (basevars RS exE)));
-
-(* -------------------------------------------------------------------------------
- The following shows that there should not be duplicates in a "stvars" tuple:
-
-Goal "!!v. basevars (v::bool stfun, v) ==> False";
-by (etac baseE 1);
-by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
-by (atac 2);
-by (Asm_full_simp_tac 1);
-
-------------------------------------------------------------------------------- *)