author | haftmann |
Fri, 10 Dec 2010 16:10:50 +0100 | |
changeset 41107 | 8795cd75965e |
parent 37936 | 1e4c5015a72e |
child 42767 | e6d920bea7a6 |
permissions | -rw-r--r-- |
13786 | 1 |
(* Title: HOL/UNITY/UNITY_tactics.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 2003 University of Cambridge |
|
4 |
||
24147 | 5 |
Specialized UNITY tactics. |
13786 | 6 |
*) |
7 |
||
13797 | 8 |
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) |
24147 | 9 |
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin} |
13797 | 10 |
|
11 |
(*Combines a list of invariance THEOREMS into one.*) |
|
24147 | 12 |
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) |
13797 | 13 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
14 |
(*Proves "co" properties when the program is specified. Any use of invariants |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
15 |
(from weak constrains) must have been done already.*) |
24147 | 16 |
fun constrains_tac(cs,ss) i = |
13786 | 17 |
SELECT_GOAL |
18 |
(EVERY [REPEAT (Always_Int_tac 1), |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
19 |
(*reduce the fancy safety properties to "constrains"*) |
24147 | 20 |
REPEAT (etac @{thm Always_ConstrainsI} 1 |
21 |
ORELSE |
|
22 |
resolve_tac [@{thm StableI}, @{thm stableI}, |
|
23 |
@{thm constrains_imp_Constrains}] 1), |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
24 |
(*for safety, the totalize operator can be ignored*) |
24147 | 25 |
simp_tac (HOL_ss addsimps |
26 |
[@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, |
|
27 |
rtac @{thm constrainsI} 1, |
|
28 |
full_simp_tac ss 1, |
|
29 |
REPEAT (FIRSTGOAL (etac disjE)), |
|
30 |
ALLGOALS (clarify_tac cs), |
|
34234 | 31 |
ALLGOALS (asm_full_simp_tac ss)]) i; |
13786 | 32 |
|
33 |
(*proves "ensures/leadsTo" properties when the program is specified*) |
|
24147 | 34 |
fun ensures_tac(cs,ss) sact = |
13786 | 35 |
SELECT_GOAL |
36 |
(EVERY [REPEAT (Always_Int_tac 1), |
|
24147 | 37 |
etac @{thm Always_LeadsTo_Basis} 1 |
38 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
|
39 |
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
|
40 |
@{thm EnsuresI}, @{thm ensuresI}] 1), |
|
41 |
(*now there are two subgoals: co & transient*) |
|
42 |
simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2, |
|
27239 | 43 |
res_inst_tac (Simplifier.the_context ss) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24147
diff
changeset
|
44 |
[(("act", 0), sact)] @{thm totalize_transientI} 2 |
27239 | 45 |
ORELSE res_inst_tac (Simplifier.the_context ss) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24147
diff
changeset
|
46 |
[(("act", 0), sact)] @{thm transientI} 2, |
13786 | 47 |
(*simplify the command's domain*) |
24147 | 48 |
simp_tac (ss addsimps [@{thm Domain_def}]) 3, |
49 |
constrains_tac (cs,ss) 1, |
|
50 |
ALLGOALS (clarify_tac cs), |
|
51 |
ALLGOALS (asm_lr_simp_tac ss)]); |
|
13796 | 52 |
|
13786 | 53 |
|
54 |
(*Composition equivalences, from Lift_prog*) |
|
55 |
||
56 |
fun make_o_equivs th = |
|
57 |
[th, |
|
24147 | 58 |
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]), |
59 |
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])]; |
|
13786 | 60 |
|
30610 | 61 |
Simplifier.change_simpset (fn ss => ss |
62 |
addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair}) |
|
63 |
addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map})); |