|
3807
|
1 |
(*
|
|
|
2 |
File: Stfun.ML
|
|
|
3 |
Author: Stephan Merz
|
|
6255
|
4 |
Copyright: 1998 University of Munich
|
|
3807
|
5 |
|
|
|
6 |
Lemmas and tactics for states and state functions.
|
|
|
7 |
*)
|
|
|
8 |
|
|
6255
|
9 |
(* [| basevars v; !!x. v x = c ==> Q |] ==> Q *)
|
|
|
10 |
bind_thm("baseE", (standard (basevars RS exE)));
|
|
3807
|
11 |
|
|
6255
|
12 |
(* -------------------------------------------------------------------------------
|
|
|
13 |
The following shows that there should not be duplicates in a "stvars" tuple:
|
|
3807
|
14 |
|
|
6255
|
15 |
Goal "!!v. basevars (v::bool stfun, v) ==> False";
|
|
|
16 |
by (etac baseE 1);
|
|
|
17 |
by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
|
|
|
18 |
by (atac 2);
|
|
|
19 |
by (Asm_full_simp_tac 1);
|
|
3807
|
20 |
|
|
6255
|
21 |
------------------------------------------------------------------------------- *)
|