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