author | wenzelm |
Tue, 17 Nov 1998 14:07:25 +0100 | |
changeset 5906 | 1f58694fc3e2 |
parent 5648 | fe887910e32e |
child 5969 | e4fe567d10e5 |
permissions | -rw-r--r-- |
5111 | 1 |
(* Title: HOL/UNITY/Traces |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Definitions of |
|
7 |
* traces: the possible execution traces |
|
8 |
* reachable: the set of reachable states |
|
9 |
||
10 |
*) |
|
11 |
||
5596 | 12 |
|
13 |
(*** The abstract type of programs ***) |
|
14 |
||
15 |
val rep_ss = simpset() addsimps |
|
16 |
[Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, |
|
17 |
Rep_Program_inverse, Abs_Program_inverse]; |
|
18 |
||
19 |
||
5620 | 20 |
Goal "Id: Acts F"; |
21 |
by (cut_inst_tac [("x", "F")] Rep_Program 1); |
|
5596 | 22 |
by (auto_tac (claset(), rep_ss)); |
5608 | 23 |
qed "Id_in_Acts"; |
24 |
AddIffs [Id_in_Acts]; |
|
5584 | 25 |
|
26 |
||
5596 | 27 |
Goal "Init (mk_program (init,acts)) = init"; |
28 |
by (auto_tac (claset(), rep_ss)); |
|
29 |
qed "Init_eq"; |
|
4776 | 30 |
|
5608 | 31 |
Goal "Acts (mk_program (init,acts)) = insert Id acts"; |
5596 | 32 |
by (auto_tac (claset(), rep_ss)); |
5423 | 33 |
qed "Acts_eq"; |
34 |
||
5596 | 35 |
Addsimps [Acts_eq, Init_eq]; |
36 |
||
5423 | 37 |
|
5620 | 38 |
Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; |
39 |
by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1); |
|
5596 | 40 |
by (auto_tac (claset(), rep_ss)); |
41 |
by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1); |
|
42 |
by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1); |
|
43 |
qed "program_equalityI"; |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
44 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
45 |
|
5648 | 46 |
(*** These rules allow "lazy" definition expansion ***) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
47 |
|
5648 | 48 |
(*The program is not expanded, but its Init is*) |
49 |
val [rew] = goal thy |
|
50 |
"[| F == mk_program (init,acts) |] \ |
|
51 |
\ ==> Init F = init"; |
|
52 |
by (rewtac rew); |
|
53 |
by Auto_tac; |
|
54 |
qed "def_prg_Init"; |
|
55 |
||
56 |
(*The program is not expanded, but its Init and Acts are*) |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
57 |
val [rew] = goal thy |
5620 | 58 |
"[| F == mk_program (init,acts) |] \ |
59 |
\ ==> Init F = init & Acts F = insert Id acts"; |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
60 |
by (rewtac rew); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
61 |
by Auto_tac; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
62 |
qed "def_prg_simps"; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
63 |
|
5648 | 64 |
(*An action is expanded only if a pair of states is being tested against it*) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
65 |
val [rew] = goal thy |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
66 |
"[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
67 |
by (rewtac rew); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
68 |
by Auto_tac; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
69 |
qed "def_act_simp"; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
70 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
71 |
fun simp_of_act def = def RS def_act_simp; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
72 |
|
5648 | 73 |
(*A set is expanded only if an element is being tested against it*) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
74 |
val [rew] = goal thy |
5648 | 75 |
"A == B ==> (x : A) = (x : B)"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
76 |
by (rewtac rew); |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
77 |
by Auto_tac; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
78 |
qed "def_set_simp"; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
79 |
|
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
80 |
fun simp_of_set def = def RS def_set_simp; |
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5423
diff
changeset
|
81 |
|
5596 | 82 |
|
83 |
(*** traces and reachable ***) |
|
84 |
||
5620 | 85 |
Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"; |
5596 | 86 |
by Safe_tac; |
87 |
by (etac traces.induct 2); |
|
88 |
by (etac reachable.induct 1); |
|
5620 | 89 |
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs))); |
5596 | 90 |
qed "reachable_equiv_traces"; |