src/HOL/TLA/TLA.thy
changeset 60754 02924903a6fd
parent 60592 c9bd1d902f04
child 61853 fb7756087101
     1.1 --- a/src/HOL/TLA/TLA.thy	Sat Jul 18 20:53:05 2015 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Sat Jul 18 20:54:56 2015 +0200
     1.3 @@ -284,23 +284,24 @@
     1.4  lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
     1.5  
     1.6  ML \<open>
     1.7 -fun merge_box_tac i =
     1.8 -   REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
     1.9 +fun merge_box_tac ctxt i =
    1.10 +   REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE} i, assume_tac ctxt i,
    1.11 +    eresolve_tac ctxt @{thms box_thin} i])
    1.12  
    1.13  fun merge_temp_box_tac ctxt i =
    1.14 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
    1.15 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_temp} i, assume_tac ctxt i,
    1.16      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
    1.17  
    1.18  fun merge_stp_box_tac ctxt i =
    1.19 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
    1.20 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_stp} i, assume_tac ctxt i,
    1.21      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
    1.22  
    1.23  fun merge_act_box_tac ctxt i =
    1.24 -  REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
    1.25 +  REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_act} i, assume_tac ctxt i,
    1.26      Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
    1.27  \<close>
    1.28  
    1.29 -method_setup merge_box = \<open>Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\<close>
    1.30 +method_setup merge_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\<close>
    1.31  method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
    1.32  method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
    1.33  method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
    1.34 @@ -577,9 +578,9 @@
    1.35    SELECT_GOAL
    1.36      (EVERY
    1.37       [auto_tac ctxt,
    1.38 -      TRY (merge_box_tac 1),
    1.39 -      rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *)
    1.40 -      TRYALL (etac @{thm Stable})]);
    1.41 +      TRY (merge_box_tac ctxt 1),
    1.42 +      resolve_tac ctxt [temp_use ctxt @{thm INV1}] 1, (* fail if the goal is not a box *)
    1.43 +      TRYALL (eresolve_tac ctxt @{thms Stable})]);
    1.44  
    1.45  (* auto_inv_tac applies inv_tac and then tries to attack the subgoals
    1.46     in simple cases it may be able to handle goals like \<turnstile> MyProg \<longrightarrow> \<box>Inv.