src/HOL/TLA/Stfun.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 6255 db63752140c7
child 12607 16b63730cfbb
permissions -rw-r--r--
improved theory reference in comment
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 Stfun.ML
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@6255
     4
    Copyright:   1998 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
Lemmas and tactics for states and state functions.
wenzelm@3807
     7
*)
wenzelm@3807
     8
wenzelm@6255
     9
(*  [| basevars v; !!x. v x = c ==> Q |] ==> Q  *)
wenzelm@6255
    10
bind_thm("baseE", (standard (basevars RS exE)));
wenzelm@3807
    11
wenzelm@6255
    12
(* -------------------------------------------------------------------------------
wenzelm@6255
    13
   The following shows that there should not be duplicates in a "stvars" tuple:
wenzelm@3807
    14
wenzelm@6255
    15
Goal "!!v. basevars (v::bool stfun, v) ==> False";
wenzelm@6255
    16
by (etac baseE 1);
wenzelm@6255
    17
by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); 
wenzelm@6255
    18
by (atac 2);
wenzelm@6255
    19
by (Asm_full_simp_tac 1);
wenzelm@3807
    20
wenzelm@6255
    21
------------------------------------------------------------------------------- *)