# HG changeset patch
# User wenzelm
# Date 1009628051 -3600
# Node ID 16b63730cfbb87c1c2e48b5d8b167f45c8bdeaa5
# Parent  cf1715a5f5ec73f4d62878f7fd6ab5d27a8760ed
update by Stephan Merz;

diff -r cf1715a5f5ec -r 16b63730cfbb src/HOL/TLA/Stfun.ML
--- a/src/HOL/TLA/Stfun.ML	Fri Dec 28 10:11:14 2001 +0100
+++ b/src/HOL/TLA/Stfun.ML	Sat Dec 29 13:14:11 2001 +0100
@@ -6,6 +6,43 @@
 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)));
 
diff -r cf1715a5f5ec -r 16b63730cfbb src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Fri Dec 28 10:11:14 2001 +0100
+++ b/src/HOL/TLA/Stfun.thy	Sat Dec 29 13:14:11 2001 +0100
@@ -34,8 +34,7 @@
      of flexible quantification later on. Nevertheless, we need to distinguish
      state variables, mainly to define the enabledness of actions. The user
      identifies (tuples of) "base" state variables in a specification via the
-     "meta predicate" stvars.
-     NOTE: There should not be duplicates in the tuple!
+     "meta predicate" basevars, which is defined here.
   *)
   stvars    :: "'a stfun => bool"
 
@@ -47,17 +46,13 @@
   "PRED P"   =>  "(P::state => _)"
   "_stvars"  ==  "stvars"
 
-rules
+defs
   (* Base variables may be assigned arbitrary (type-correct) values. 
-     Note that vs may be a tuple of variables. The rule would be unsound 
-     if vs contained duplicates.
+     Note that vs may be a tuple of variables. The correct identification
+     of base variables is up to the user who must take care not to
+     introduce an inconsistency. For example, "basevars (x,x)" would
+     definitely be inconsistent.
   *)
-  basevars  "basevars vs ==> EX u. vs u = c"
-  base_pair "basevars (x,y) ==> basevars x & basevars y"
-  (* 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.
-  *)
-  unit_base "basevars (v::unit stfun)"
+  basevars_def	"stvars vs == range vs = UNIV"
 
 end