update by Stephan Merz;
authorwenzelm
Sat Dec 29 13:14:11 2001 +0100 (2001-12-29)
changeset 1260716b63730cfbb
parent 12606 cf1715a5f5ec
child 12608 2df381faa787
update by Stephan Merz;
src/HOL/TLA/Stfun.ML
src/HOL/TLA/Stfun.thy
     1.1 --- a/src/HOL/TLA/Stfun.ML	Fri Dec 28 10:11:14 2001 +0100
     1.2 +++ b/src/HOL/TLA/Stfun.ML	Sat Dec 29 13:14:11 2001 +0100
     1.3 @@ -6,6 +6,43 @@
     1.4  Lemmas and tactics for states and state functions.
     1.5  *)
     1.6  
     1.7 +Goalw [basevars_def] "!!vs. basevars vs ==> EX u. vs u = c";
     1.8 +by (res_inst_tac [("b","c"),("f","vs")] rangeE 1);
     1.9 +by Auto_tac;
    1.10 +qed "basevars";
    1.11 +
    1.12 +Goal "!!x y. basevars (x,y) ==> basevars x";
    1.13 +by (simp_tac (simpset() addsimps [basevars_def]) 1);
    1.14 +by (rtac equalityI 1);
    1.15 + by (rtac subset_UNIV 1);
    1.16 +by (rtac subsetI 1);
    1.17 +by (dres_inst_tac [("c", "(xa, arbitrary)")] basevars 1);
    1.18 +by Auto_tac;
    1.19 +qed "base_pair1";
    1.20 +
    1.21 +Goal "!!x y. basevars (x,y) ==> basevars y";
    1.22 +by (simp_tac (simpset() addsimps [basevars_def]) 1);
    1.23 +by (rtac equalityI 1);
    1.24 + by (rtac subset_UNIV 1);
    1.25 +by (rtac subsetI 1);
    1.26 +by (dres_inst_tac [("c", "(arbitrary, xa)")] basevars 1);
    1.27 +by Auto_tac;
    1.28 +qed "base_pair2";
    1.29 +
    1.30 +Goal "!!x y. basevars (x,y) ==> basevars x & basevars y";
    1.31 +by (rtac conjI 1);
    1.32 +by (etac base_pair1 1);
    1.33 +by (etac base_pair2 1);
    1.34 +qed "base_pair";
    1.35 +
    1.36 +(* Since the unit type has just one value, any state function can be
    1.37 +   regarded as "base". The following axiom can sometimes be useful
    1.38 +   because it gives a trivial solution for "basevars" premises.
    1.39 +*)
    1.40 +Goalw [basevars_def] "basevars (v::unit stfun)";
    1.41 +by Auto_tac;
    1.42 +qed "unit_base";
    1.43 +
    1.44  (*  [| basevars v; !!x. v x = c ==> Q |] ==> Q  *)
    1.45  bind_thm("baseE", (standard (basevars RS exE)));
    1.46  
     2.1 --- a/src/HOL/TLA/Stfun.thy	Fri Dec 28 10:11:14 2001 +0100
     2.2 +++ b/src/HOL/TLA/Stfun.thy	Sat Dec 29 13:14:11 2001 +0100
     2.3 @@ -34,8 +34,7 @@
     2.4       of flexible quantification later on. Nevertheless, we need to distinguish
     2.5       state variables, mainly to define the enabledness of actions. The user
     2.6       identifies (tuples of) "base" state variables in a specification via the
     2.7 -     "meta predicate" stvars.
     2.8 -     NOTE: There should not be duplicates in the tuple!
     2.9 +     "meta predicate" basevars, which is defined here.
    2.10    *)
    2.11    stvars    :: "'a stfun => bool"
    2.12  
    2.13 @@ -47,17 +46,13 @@
    2.14    "PRED P"   =>  "(P::state => _)"
    2.15    "_stvars"  ==  "stvars"
    2.16  
    2.17 -rules
    2.18 +defs
    2.19    (* Base variables may be assigned arbitrary (type-correct) values. 
    2.20 -     Note that vs may be a tuple of variables. The rule would be unsound 
    2.21 -     if vs contained duplicates.
    2.22 +     Note that vs may be a tuple of variables. The correct identification
    2.23 +     of base variables is up to the user who must take care not to
    2.24 +     introduce an inconsistency. For example, "basevars (x,x)" would
    2.25 +     definitely be inconsistent.
    2.26    *)
    2.27 -  basevars  "basevars vs ==> EX u. vs u = c"
    2.28 -  base_pair "basevars (x,y) ==> basevars x & basevars y"
    2.29 -  (* Since the unit type has just one value, any state function can be
    2.30 -     regarded as "base". The following axiom can sometimes be useful
    2.31 -     because it gives a trivial solution for "basevars" premises.
    2.32 -  *)
    2.33 -  unit_base "basevars (v::unit stfun)"
    2.34 +  basevars_def	"stvars vs == range vs = UNIV"
    2.35  
    2.36  end