src/HOL/TLA/Stfun.ML

update by Stephan Merz;

(* 
    File:	 Stfun.ML
    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);

------------------------------------------------------------------------------- *)