author | wenzelm |
Mon, 19 Nov 2012 16:14:18 +0100 | |
changeset 50122 | 7ae7efef5ad8 |
parent 46752 | e9e7209eb375 |
child 51717 | 9e7d1c139569 |
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.*) |
42767 | 16 |
fun constrains_tac ctxt i = |
42793 | 17 |
SELECT_GOAL |
18 |
(EVERY |
|
19 |
[REPEAT (Always_Int_tac 1), |
|
20 |
(*reduce the fancy safety properties to "constrains"*) |
|
21 |
REPEAT (etac @{thm Always_ConstrainsI} 1 |
|
22 |
ORELSE |
|
23 |
resolve_tac [@{thm StableI}, @{thm stableI}, |
|
24 |
@{thm constrains_imp_Constrains}] 1), |
|
25 |
(*for safety, the totalize operator can be ignored*) |
|
26 |
simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, |
|
27 |
rtac @{thm constrainsI} 1, |
|
28 |
full_simp_tac (simpset_of ctxt) 1, |
|
29 |
REPEAT (FIRSTGOAL (etac disjE)), |
|
30 |
ALLGOALS (clarify_tac ctxt), |
|
31 |
ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i; |
|
13786 | 32 |
|
33 |
(*proves "ensures/leadsTo" properties when the program is specified*) |
|
42767 | 34 |
fun ensures_tac ctxt sact = |
42793 | 35 |
SELECT_GOAL |
36 |
(EVERY |
|
37 |
[REPEAT (Always_Int_tac 1), |
|
38 |
etac @{thm Always_LeadsTo_Basis} 1 |
|
39 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
|
40 |
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
|
41 |
@{thm EnsuresI}, @{thm ensuresI}] 1), |
|
42 |
(*now there are two subgoals: co & transient*) |
|
43 |
simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2, |
|
44 |
res_inst_tac ctxt |
|
45 |
[(("act", 0), sact)] @{thm totalize_transientI} 2 |
|
46 |
ORELSE res_inst_tac ctxt |
|
47 |
[(("act", 0), sact)] @{thm transientI} 2, |
|
48 |
(*simplify the command's domain*) |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45138
diff
changeset
|
49 |
simp_tac (simpset_of ctxt addsimps @{thms Domain_unfold}) 3, |
42793 | 50 |
constrains_tac ctxt 1, |
51 |
ALLGOALS (clarify_tac ctxt), |
|
52 |
ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]); |
|
13796 | 53 |
|
13786 | 54 |
|
55 |
(*Composition equivalences, from Lift_prog*) |
|
56 |
||
57 |
fun make_o_equivs th = |
|
58 |
[th, |
|
24147 | 59 |
th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]), |
60 |
th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])]; |
|
13786 | 61 |