3807
|
1 |
(*
|
|
2 |
File: Stfun.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
|
6 |
Lemmas and tactics for states and state functions.
|
|
7 |
*)
|
|
8 |
|
|
9 |
(* A stronger version of existential elimination (goal needn't be boolean) *)
|
|
10 |
qed_goalw "exE_prop" HOL.thy [Ex_def]
|
|
11 |
"[| ? x::'a.P(x); !!x. P(x) ==> PROP R |] ==> PROP R"
|
|
12 |
(fn prems => [REPEAT(resolve_tac prems 1)]);
|
|
13 |
|
|
14 |
(* Might as well use that version in automated proofs *)
|
|
15 |
AddSEs [exE_prop];
|
|
16 |
|
|
17 |
(* [| base_var v; !!x. v x = c ==> PROP R |] ==> PROP R *)
|
|
18 |
bind_thm("baseE", (standard (base_var RS exE_prop)));
|
|
19 |
|
|
20 |
qed_goal "PairVarE" Stfun.thy
|
|
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 |
|