src/HOL/UNITY/UNITY_tactics.ML
author wenzelm
Thu May 12 18:18:06 2011 +0200 (2011-05-12)
changeset 42767 e6d920bea7a6
parent 37936 1e4c5015a72e
child 42793 88bee9f6eec7
permissions -rw-r--r--
prefer Proof.context over old-style clasimpset;
     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 val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
    10 
    11 (*Combines a list of invariance THEOREMS into one.*)
    12 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
    13 
    14 (*Proves "co" properties when the program is specified.  Any use of invariants
    15   (from weak constrains) must have been done already.*)
    16 fun constrains_tac ctxt i =
    17   let
    18     val cs = claset_of ctxt;
    19     val ss = simpset_of ctxt;
    20   in
    21    SELECT_GOAL
    22       (EVERY [REPEAT (Always_Int_tac 1),
    23               (*reduce the fancy safety properties to "constrains"*)
    24               REPEAT (etac @{thm Always_ConstrainsI} 1
    25                       ORELSE
    26                       resolve_tac [@{thm StableI}, @{thm stableI},
    27                                    @{thm constrains_imp_Constrains}] 1),
    28               (*for safety, the totalize operator can be ignored*)
    29               simp_tac (HOL_ss addsimps
    30                          [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    31               rtac @{thm constrainsI} 1,
    32               full_simp_tac ss 1,
    33               REPEAT (FIRSTGOAL (etac disjE)),
    34               ALLGOALS (clarify_tac cs),
    35               ALLGOALS (asm_full_simp_tac ss)]) i
    36   end;
    37 
    38 (*proves "ensures/leadsTo" properties when the program is specified*)
    39 fun ensures_tac ctxt sact =
    40   let
    41     val cs = claset_of ctxt;
    42     val ss = simpset_of ctxt;
    43   in
    44     SELECT_GOAL
    45       (EVERY [REPEAT (Always_Int_tac 1),
    46               etac @{thm Always_LeadsTo_Basis} 1
    47                   ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    48                   REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    49                                     @{thm EnsuresI}, @{thm ensuresI}] 1),
    50               (*now there are two subgoals: co & transient*)
    51               simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
    52               res_inst_tac (Simplifier.the_context ss)
    53                 [(("act", 0), sact)] @{thm totalize_transientI} 2
    54               ORELSE res_inst_tac (Simplifier.the_context ss)
    55                 [(("act", 0), sact)] @{thm transientI} 2,
    56                  (*simplify the command's domain*)
    57               simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    58               constrains_tac ctxt 1,
    59               ALLGOALS (clarify_tac cs),
    60               ALLGOALS (asm_lr_simp_tac ss)])
    61   end;
    62 
    63 
    64 (*Composition equivalences, from Lift_prog*)
    65 
    66 fun make_o_equivs th =
    67     [th,
    68      th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
    69      th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
    70 
    71 Simplifier.change_simpset (fn ss => ss
    72   addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
    73   addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}));