src/HOL/UNITY/UNITY_tactics.ML
author wenzelm
Thu Apr 18 17:07:01 2013 +0200 (2013-04-18)
changeset 51717 9e7d1c139569
parent 46752 e9e7209eb375
child 58963 26bf09b95dda
permissions -rw-r--r--
simplifier uses proper Proof.context instead of historic type simpset;
     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   SELECT_GOAL
    18     (EVERY
    19      [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 (put_simpset HOL_ss ctxt
    27         addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    28       rtac @{thm constrainsI} 1,
    29       full_simp_tac ctxt 1,
    30       REPEAT (FIRSTGOAL (etac disjE)),
    31       ALLGOALS (clarify_tac ctxt),
    32       ALLGOALS (asm_full_simp_tac ctxt)]) i;
    33 
    34 (*proves "ensures/leadsTo" properties when the program is specified*)
    35 fun ensures_tac ctxt sact =
    36   SELECT_GOAL
    37     (EVERY
    38      [REPEAT (Always_Int_tac 1),
    39       etac @{thm Always_LeadsTo_Basis} 1
    40           ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    41           REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    42                             @{thm EnsuresI}, @{thm ensuresI}] 1),
    43       (*now there are two subgoals: co & transient*)
    44       simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
    45       res_inst_tac ctxt
    46         [(("act", 0), sact)] @{thm totalize_transientI} 2
    47       ORELSE res_inst_tac ctxt
    48         [(("act", 0), sact)] @{thm transientI} 2,
    49          (*simplify the command's domain*)
    50       simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
    51       constrains_tac ctxt 1,
    52       ALLGOALS (clarify_tac ctxt),
    53       ALLGOALS (asm_lr_simp_tac ctxt)]);
    54 
    55 
    56 (*Composition equivalences, from Lift_prog*)
    57 
    58 fun make_o_equivs ctxt th =
    59   [th,
    60    th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
    61    th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
    62