src/HOL/UNITY/UNITY_tactics.ML
author paulson
Sun Jan 03 11:03:00 2010 +0000 (2010-01-03)
changeset 34234 86a985e9b4df
parent 30610 bcbc34cb9749
child 37936 1e4c5015a72e
permissions -rw-r--r--
removed legacy asm_lr_simp_tac
     1 (*  Title:      HOL/UNITY/UNITY_tactics.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2003  University of Cambridge
     5 
     6 Specialized UNITY tactics.
     7 *)
     8 
     9 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    10 val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
    11 
    12 (*Combines a list of invariance THEOREMS into one.*)
    13 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
    14 
    15 (*Proves "co" properties when the program is specified.  Any use of invariants
    16   (from weak constrains) must have been done already.*)
    17 fun constrains_tac(cs,ss) i =
    18    SELECT_GOAL
    19       (EVERY [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
    27                          [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    28               rtac @{thm constrainsI} 1,
    29               full_simp_tac ss 1,
    30               REPEAT (FIRSTGOAL (etac disjE)),
    31               ALLGOALS (clarify_tac cs),
    32               ALLGOALS (asm_full_simp_tac ss)]) i;
    33 
    34 (*proves "ensures/leadsTo" properties when the program is specified*)
    35 fun ensures_tac(cs,ss) sact =
    36     SELECT_GOAL
    37       (EVERY [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 (ss addsimps [@{thm mk_total_program_def}]) 2,
    44               res_inst_tac (Simplifier.the_context ss)
    45                 [(("act", 0), sact)] @{thm totalize_transientI} 2
    46               ORELSE res_inst_tac (Simplifier.the_context ss)
    47                 [(("act", 0), sact)] @{thm transientI} 2,
    48                  (*simplify the command's domain*)
    49               simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    50               constrains_tac (cs,ss) 1,
    51               ALLGOALS (clarify_tac cs),
    52               ALLGOALS (asm_lr_simp_tac ss)]);
    53 
    54 
    55 (*Composition equivalences, from Lift_prog*)
    56 
    57 fun make_o_equivs th =
    58     [th,
    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}])];
    61 
    62 Simplifier.change_simpset (fn ss => ss
    63   addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
    64   addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));