# File Stfun.ML

    (*
        File:        Stfun.ML
        ID:          $Id: Stfun.ML,v 1.6 2005/09/07 18:22:40 wenzelm Exp $
        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);

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