1 (* |
|
2 File: Stfun.ML |
|
3 ID: $Id$ |
|
4 Author: Stephan Merz |
|
5 Copyright: 1998 University of Munich |
|
6 |
|
7 Lemmas and tactics for states and state functions. |
|
8 *) |
|
9 |
|
10 Goalw [basevars_def] "!!vs. basevars vs ==> EX u. vs u = c"; |
|
11 by (res_inst_tac [("b","c"),("f","vs")] rangeE 1); |
|
12 by Auto_tac; |
|
13 qed "basevars"; |
|
14 |
|
15 Goal "!!x y. basevars (x,y) ==> basevars x"; |
|
16 by (simp_tac (simpset() addsimps [basevars_def]) 1); |
|
17 by (rtac equalityI 1); |
|
18 by (rtac subset_UNIV 1); |
|
19 by (rtac subsetI 1); |
|
20 by (dres_inst_tac [("c", "(xa, arbitrary)")] basevars 1); |
|
21 by Auto_tac; |
|
22 qed "base_pair1"; |
|
23 |
|
24 Goal "!!x y. basevars (x,y) ==> basevars y"; |
|
25 by (simp_tac (simpset() addsimps [basevars_def]) 1); |
|
26 by (rtac equalityI 1); |
|
27 by (rtac subset_UNIV 1); |
|
28 by (rtac subsetI 1); |
|
29 by (dres_inst_tac [("c", "(arbitrary, xa)")] basevars 1); |
|
30 by Auto_tac; |
|
31 qed "base_pair2"; |
|
32 |
|
33 Goal "!!x y. basevars (x,y) ==> basevars x & basevars y"; |
|
34 by (rtac conjI 1); |
|
35 by (etac base_pair1 1); |
|
36 by (etac base_pair2 1); |
|
37 qed "base_pair"; |
|
38 |
|
39 (* Since the unit type has just one value, any state function can be |
|
40 regarded as "base". The following axiom can sometimes be useful |
|
41 because it gives a trivial solution for "basevars" premises. |
|
42 *) |
|
43 Goalw [basevars_def] "basevars (v::unit stfun)"; |
|
44 by Auto_tac; |
|
45 qed "unit_base"; |
|
46 |
|
47 (* [| basevars v; !!x. v x = c ==> Q |] ==> Q *) |
|
48 bind_thm("baseE", (standard (basevars RS exE))); |
|
49 |
|
50 (* ------------------------------------------------------------------------------- |
|
51 The following shows that there should not be duplicates in a "stvars" tuple: |
|
52 |
|
53 Goal "!!v. basevars (v::bool stfun, v) ==> False"; |
|
54 by (etac baseE 1); |
|
55 by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); |
|
56 by (atac 2); |
|
57 by (Asm_full_simp_tac 1); |
|
58 |
|
59 ------------------------------------------------------------------------------- *) |
|