1 (* |
1 (* |
2 File: Stfun.ML |
2 File: Stfun.ML |
3 Author: Stephan Merz |
3 Author: Stephan Merz |
4 Copyright: 1997 University of Munich |
4 Copyright: 1998 University of Munich |
5 |
5 |
6 Lemmas and tactics for states and state functions. |
6 Lemmas and tactics for states and state functions. |
7 *) |
7 *) |
8 |
8 |
9 (* A stronger version of existential elimination (goal needn't be boolean) *) |
9 (* [| basevars v; !!x. v x = c ==> Q |] ==> Q *) |
10 qed_goalw "exE_prop" HOL.thy [Ex_def] |
10 bind_thm("baseE", (standard (basevars RS exE))); |
11 "[| ? x::'a. P(x); !!x. P(x) ==> PROP R |] ==> PROP R" |
|
12 (fn prems => [REPEAT(resolve_tac prems 1)]); |
|
13 |
11 |
14 (* Might as well use that version in automated proofs *) |
12 (* ------------------------------------------------------------------------------- |
15 AddSEs [exE_prop]; |
13 The following shows that there should not be duplicates in a "stvars" tuple: |
16 |
14 |
17 (* [| base_var v; !!x. v x = c ==> PROP R |] ==> PROP R *) |
15 Goal "!!v. basevars (v::bool stfun, v) ==> False"; |
18 bind_thm("baseE", (standard (base_var RS exE_prop))); |
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); |
19 |
20 |
20 qed_goal "PairVarE" Stfun.thy |
21 ------------------------------------------------------------------------------- *) |
21 "[| <v,w> u = (x,y); [| v u = x; w u = y |] ==> PROP R |] ==> PROP R" |
|
22 (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1, |
|
23 ALLGOALS (asm_full_simp_tac (simpset() addsimps [pairSF_def])) |
|
24 ]); |
|
25 |
|