1(*  Title:      HOL/UNITY/UNITY_tactics.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   2003  University of Cambridge
4
5Specialized UNITY tactics.
6*)
7
8(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
9fun Always_Int_tac ctxt =
10  dresolve_tac ctxt @{thms Always_Int_I} THEN'
11  assume_tac ctxt THEN'
12  eresolve_tac ctxt @{thms Always_thin}
13
14(*Combines a list of invariance THEOREMS into one.*)
15val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
16
17(*Proves "co" properties when the program is specified.  Any use of invariants
18  (from weak constrains) must have been done already.*)
19fun constrains_tac ctxt i =
20  SELECT_GOAL
21    (EVERY
22     [REPEAT (Always_Int_tac ctxt 1),
23      (*reduce the fancy safety properties to "constrains"*)
24      REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
25              ORELSE
26              resolve_tac ctxt [@{thm StableI}, @{thm stableI},
27                           @{thm constrains_imp_Constrains}] 1),
28      (*for safety, the totalize operator can be ignored*)
29      simp_tac (put_simpset HOL_ss ctxt
30        addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
31      resolve_tac ctxt @{thms constrainsI} 1,
32      full_simp_tac ctxt 1,
33      REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
34      ALLGOALS (clarify_tac ctxt),
35      ALLGOALS (asm_full_simp_tac ctxt)]) i;
36
37(*proves "ensures/leadsTo" properties when the program is specified*)
38fun ensures_tac ctxt sact =
39  SELECT_GOAL
40    (EVERY
41     [REPEAT (Always_Int_tac ctxt 1),
42      eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
43          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
44          REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
45                            @{thm EnsuresI}, @{thm ensuresI}] 1),
46      (*now there are two subgoals: co & transient*)
47      simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
48      Rule_Insts.res_inst_tac ctxt
49        [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
50      ORELSE Rule_Insts.res_inst_tac ctxt
51        [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
52         (*simplify the command's domain*)
53      simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
54      constrains_tac ctxt 1,
55      ALLGOALS (clarify_tac ctxt),
56      ALLGOALS (asm_lr_simp_tac ctxt)]);
57
58
59(*Composition equivalences, from Lift_prog*)
60
61fun make_o_equivs ctxt th =
62  [th,
63   th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
64   th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
65
66