src/HOL/UNITY/UNITY_tactics.ML
changeset 51717 9e7d1c139569
parent 46752 e9e7209eb375
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -23,12 +23,13 @@
     1.4                resolve_tac [@{thm StableI}, @{thm stableI},
     1.5                             @{thm constrains_imp_Constrains}] 1),
     1.6        (*for safety, the totalize operator can be ignored*)
     1.7 -      simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
     1.8 +      simp_tac (put_simpset HOL_ss ctxt
     1.9 +        addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
    1.10        rtac @{thm constrainsI} 1,
    1.11 -      full_simp_tac (simpset_of ctxt) 1,
    1.12 +      full_simp_tac ctxt 1,
    1.13        REPEAT (FIRSTGOAL (etac disjE)),
    1.14        ALLGOALS (clarify_tac ctxt),
    1.15 -      ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
    1.16 +      ALLGOALS (asm_full_simp_tac ctxt)]) i;
    1.17  
    1.18  (*proves "ensures/leadsTo" properties when the program is specified*)
    1.19  fun ensures_tac ctxt sact =
    1.20 @@ -40,22 +41,22 @@
    1.21            REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    1.22                              @{thm EnsuresI}, @{thm ensuresI}] 1),
    1.23        (*now there are two subgoals: co & transient*)
    1.24 -      simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
    1.25 +      simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
    1.26        res_inst_tac ctxt
    1.27          [(("act", 0), sact)] @{thm totalize_transientI} 2
    1.28        ORELSE res_inst_tac ctxt
    1.29          [(("act", 0), sact)] @{thm transientI} 2,
    1.30           (*simplify the command's domain*)
    1.31 -      simp_tac (simpset_of ctxt addsimps @{thms Domain_unfold}) 3,
    1.32 +      simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
    1.33        constrains_tac ctxt 1,
    1.34        ALLGOALS (clarify_tac ctxt),
    1.35 -      ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
    1.36 +      ALLGOALS (asm_lr_simp_tac ctxt)]);
    1.37  
    1.38  
    1.39  (*Composition equivalences, from Lift_prog*)
    1.40  
    1.41 -fun make_o_equivs th =
    1.42 -    [th,
    1.43 -     th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
    1.44 -     th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
    1.45 +fun make_o_equivs ctxt th =
    1.46 +  [th,
    1.47 +   th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
    1.48 +   th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];
    1.49