src/HOL/UNITY/UNITY_tactics.ML
changeset 42793 88bee9f6eec7
parent 42767 e6d920bea7a6
child 42795 66fcc9882784
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -14,51 +14,42 @@
     1.4  (*Proves "co" properties when the program is specified.  Any use of invariants
     1.5    (from weak constrains) must have been done already.*)
     1.6  fun constrains_tac ctxt i =
     1.7 -  let
     1.8 -    val cs = claset_of ctxt;
     1.9 -    val ss = simpset_of ctxt;
    1.10 -  in
    1.11 -   SELECT_GOAL
    1.12 -      (EVERY [REPEAT (Always_Int_tac 1),
    1.13 -              (*reduce the fancy safety properties to "constrains"*)
    1.14 -              REPEAT (etac @{thm Always_ConstrainsI} 1
    1.15 -                      ORELSE
    1.16 -                      resolve_tac [@{thm StableI}, @{thm stableI},
    1.17 -                                   @{thm constrains_imp_Constrains}] 1),
    1.18 -              (*for safety, the totalize operator can be ignored*)
    1.19 -              simp_tac (HOL_ss addsimps
    1.20 -                         [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    1.21 -              rtac @{thm constrainsI} 1,
    1.22 -              full_simp_tac ss 1,
    1.23 -              REPEAT (FIRSTGOAL (etac disjE)),
    1.24 -              ALLGOALS (clarify_tac cs),
    1.25 -              ALLGOALS (asm_full_simp_tac ss)]) i
    1.26 -  end;
    1.27 +  SELECT_GOAL
    1.28 +    (EVERY
    1.29 +     [REPEAT (Always_Int_tac 1),
    1.30 +      (*reduce the fancy safety properties to "constrains"*)
    1.31 +      REPEAT (etac @{thm Always_ConstrainsI} 1
    1.32 +              ORELSE
    1.33 +              resolve_tac [@{thm StableI}, @{thm stableI},
    1.34 +                           @{thm constrains_imp_Constrains}] 1),
    1.35 +      (*for safety, the totalize operator can be ignored*)
    1.36 +      simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    1.37 +      rtac @{thm constrainsI} 1,
    1.38 +      full_simp_tac (simpset_of ctxt) 1,
    1.39 +      REPEAT (FIRSTGOAL (etac disjE)),
    1.40 +      ALLGOALS (clarify_tac ctxt),
    1.41 +      ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
    1.42  
    1.43  (*proves "ensures/leadsTo" properties when the program is specified*)
    1.44  fun ensures_tac ctxt sact =
    1.45 -  let
    1.46 -    val cs = claset_of ctxt;
    1.47 -    val ss = simpset_of ctxt;
    1.48 -  in
    1.49 -    SELECT_GOAL
    1.50 -      (EVERY [REPEAT (Always_Int_tac 1),
    1.51 -              etac @{thm Always_LeadsTo_Basis} 1
    1.52 -                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    1.53 -                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    1.54 -                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
    1.55 -              (*now there are two subgoals: co & transient*)
    1.56 -              simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
    1.57 -              res_inst_tac (Simplifier.the_context ss)
    1.58 -                [(("act", 0), sact)] @{thm totalize_transientI} 2
    1.59 -              ORELSE res_inst_tac (Simplifier.the_context ss)
    1.60 -                [(("act", 0), sact)] @{thm transientI} 2,
    1.61 -                 (*simplify the command's domain*)
    1.62 -              simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    1.63 -              constrains_tac ctxt 1,
    1.64 -              ALLGOALS (clarify_tac cs),
    1.65 -              ALLGOALS (asm_lr_simp_tac ss)])
    1.66 -  end;
    1.67 +  SELECT_GOAL
    1.68 +    (EVERY
    1.69 +     [REPEAT (Always_Int_tac 1),
    1.70 +      etac @{thm Always_LeadsTo_Basis} 1
    1.71 +          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
    1.72 +          REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    1.73 +                            @{thm EnsuresI}, @{thm ensuresI}] 1),
    1.74 +      (*now there are two subgoals: co & transient*)
    1.75 +      simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
    1.76 +      res_inst_tac ctxt
    1.77 +        [(("act", 0), sact)] @{thm totalize_transientI} 2
    1.78 +      ORELSE res_inst_tac ctxt
    1.79 +        [(("act", 0), sact)] @{thm transientI} 2,
    1.80 +         (*simplify the command's domain*)
    1.81 +      simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
    1.82 +      constrains_tac ctxt 1,
    1.83 +      ALLGOALS (clarify_tac ctxt),
    1.84 +      ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
    1.85  
    1.86  
    1.87  (*Composition equivalences, from Lift_prog*)