src/HOL/UNITY/UNITY_tactics.ML
author wenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773 d09c66a0ea10
parent 60754 02924903a6fd
child 60774 6c28d8ed2488
permissions -rw-r--r--
more symbols by default, without xsymbols mode;
     1 (*  Title:      HOL/UNITY/UNITY_tactics.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2003  University of Cambridge
     4 
     5 Specialized UNITY tactics.
     6 *)
     7 
     8 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
     9 fun 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.*)
    15 val 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.*)
    19 fun 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*)
    38 fun 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 [@{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 
    61 fun 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