3 Author: Stephan Merz |
3 Author: Stephan Merz |
4 Copyright: 1998 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 |
|
9 Goalw [basevars_def] "!!vs. basevars vs ==> EX u. vs u = c"; |
|
10 by (res_inst_tac [("b","c"),("f","vs")] rangeE 1); |
|
11 by Auto_tac; |
|
12 qed "basevars"; |
|
13 |
|
14 Goal "!!x y. basevars (x,y) ==> basevars x"; |
|
15 by (simp_tac (simpset() addsimps [basevars_def]) 1); |
|
16 by (rtac equalityI 1); |
|
17 by (rtac subset_UNIV 1); |
|
18 by (rtac subsetI 1); |
|
19 by (dres_inst_tac [("c", "(xa, arbitrary)")] basevars 1); |
|
20 by Auto_tac; |
|
21 qed "base_pair1"; |
|
22 |
|
23 Goal "!!x y. basevars (x,y) ==> basevars y"; |
|
24 by (simp_tac (simpset() addsimps [basevars_def]) 1); |
|
25 by (rtac equalityI 1); |
|
26 by (rtac subset_UNIV 1); |
|
27 by (rtac subsetI 1); |
|
28 by (dres_inst_tac [("c", "(arbitrary, xa)")] basevars 1); |
|
29 by Auto_tac; |
|
30 qed "base_pair2"; |
|
31 |
|
32 Goal "!!x y. basevars (x,y) ==> basevars x & basevars y"; |
|
33 by (rtac conjI 1); |
|
34 by (etac base_pair1 1); |
|
35 by (etac base_pair2 1); |
|
36 qed "base_pair"; |
|
37 |
|
38 (* Since the unit type has just one value, any state function can be |
|
39 regarded as "base". The following axiom can sometimes be useful |
|
40 because it gives a trivial solution for "basevars" premises. |
|
41 *) |
|
42 Goalw [basevars_def] "basevars (v::unit stfun)"; |
|
43 by Auto_tac; |
|
44 qed "unit_base"; |
8 |
45 |
9 (* [| basevars v; !!x. v x = c ==> Q |] ==> Q *) |
46 (* [| basevars v; !!x. v x = c ==> Q |] ==> Q *) |
10 bind_thm("baseE", (standard (basevars RS exE))); |
47 bind_thm("baseE", (standard (basevars RS exE))); |
11 |
48 |
12 (* ------------------------------------------------------------------------------- |
49 (* ------------------------------------------------------------------------------- |