author | wenzelm |
Mon, 10 Nov 2014 21:49:48 +0100 | |
changeset 58963 | 26bf09b95dda |
parent 51717 | 9e7d1c139569 |
child 59498 | 50b60f501b05 |
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??*) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
51717
diff
changeset
|
9 |
fun Always_Int_tac ctxt = |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
51717
diff
changeset
|
10 |
dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin} |
13797 | 11 |
|
12 |
(*Combines a list of invariance THEOREMS into one.*) |
|
24147 | 13 |
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) |
13797 | 14 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
15 |
(*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
|
16 |
(from weak constrains) must have been done already.*) |
42767 | 17 |
fun constrains_tac ctxt i = |
42793 | 18 |
SELECT_GOAL |
19 |
(EVERY |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
51717
diff
changeset
|
20 |
[REPEAT (Always_Int_tac ctxt 1), |
42793 | 21 |
(*reduce the fancy safety properties to "constrains"*) |
22 |
REPEAT (etac @{thm Always_ConstrainsI} 1 |
|
23 |
ORELSE |
|
24 |
resolve_tac [@{thm StableI}, @{thm stableI}, |
|
25 |
@{thm constrains_imp_Constrains}] 1), |
|
26 |
(*for safety, the totalize operator can be ignored*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
27 |
simp_tac (put_simpset HOL_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
28 |
addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, |
42793 | 29 |
rtac @{thm constrainsI} 1, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
30 |
full_simp_tac ctxt 1, |
42793 | 31 |
REPEAT (FIRSTGOAL (etac disjE)), |
32 |
ALLGOALS (clarify_tac ctxt), |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
33 |
ALLGOALS (asm_full_simp_tac ctxt)]) i; |
13786 | 34 |
|
35 |
(*proves "ensures/leadsTo" properties when the program is specified*) |
|
42767 | 36 |
fun ensures_tac ctxt sact = |
42793 | 37 |
SELECT_GOAL |
38 |
(EVERY |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
51717
diff
changeset
|
39 |
[REPEAT (Always_Int_tac ctxt 1), |
42793 | 40 |
etac @{thm Always_LeadsTo_Basis} 1 |
41 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
|
42 |
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
|
43 |
@{thm EnsuresI}, @{thm ensuresI}] 1), |
|
44 |
(*now there are two subgoals: co & transient*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
45 |
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2, |
42793 | 46 |
res_inst_tac ctxt |
47 |
[(("act", 0), sact)] @{thm totalize_transientI} 2 |
|
48 |
ORELSE res_inst_tac ctxt |
|
49 |
[(("act", 0), sact)] @{thm transientI} 2, |
|
50 |
(*simplify the command's domain*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
51 |
simp_tac (ctxt addsimps @{thms Domain_unfold}) 3, |
42793 | 52 |
constrains_tac ctxt 1, |
53 |
ALLGOALS (clarify_tac ctxt), |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
54 |
ALLGOALS (asm_lr_simp_tac ctxt)]); |
13796 | 55 |
|
13786 | 56 |
|
57 |
(*Composition equivalences, from Lift_prog*) |
|
58 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
59 |
fun make_o_equivs ctxt th = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
60 |
[th, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
61 |
th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46752
diff
changeset
|
62 |
th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])]; |
13786 | 63 |