(* 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); ------------------------------------------------------------------------------- *)