src/HOL/TLA/Action.thy
changeset 24180 9f818139951b
parent 21624 6f79647cf536
child 27104 791607529f6d
     1.1 --- a/src/HOL/TLA/Action.thy	Tue Aug 07 20:43:36 2007 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Tue Aug 07 23:24:10 2007 +0200
     1.3 @@ -109,13 +109,9 @@
     1.4     functions defined in Intensional.ML in that they introduce a
     1.5     "world" parameter of the form (s,t) and apply additional rewrites.
     1.6  *)
     1.7 -local
     1.8 -  val action_rews = thms "action_rews";
     1.9 -  val actionD = thm "actionD";
    1.10 -in
    1.11  
    1.12  fun action_unlift th =
    1.13 -  (rewrite_rule action_rews (th RS actionD))
    1.14 +  (rewrite_rule @{thms action_rews} (th RS @{thm actionD}))
    1.15      handle THM _ => int_unlift th;
    1.16  
    1.17  (* Turn  |- A = B  into meta-level rewrite rule  A == B *)
    1.18 @@ -126,8 +122,6 @@
    1.19        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    1.20                (flatten (action_unlift th) handle THM _ => th)
    1.21      | _ => th;
    1.22 -
    1.23 -end
    1.24  *}
    1.25  
    1.26  setup {*
    1.27 @@ -269,22 +263,12 @@
    1.28     should plug in only "very safe" rules that can be applied blindly.
    1.29     Note that it applies whatever simplifications are currently active.
    1.30  *)
    1.31 -local
    1.32 -  val actionI = thm "actionI";
    1.33 -  val intI = thm "intI";
    1.34 -in
    1.35 -
    1.36  fun action_simp_tac ss intros elims =
    1.37      asm_full_simp_tac
    1.38           (ss setloop ((resolve_tac ((map action_use intros)
    1.39 -                                    @ [refl,impI,conjI,actionI,intI,allI]))
    1.40 +                                    @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
    1.41                        ORELSE' (eresolve_tac ((map action_use elims)
    1.42                                               @ [conjE,disjE,exE]))));
    1.43 -
    1.44 -(* default version without additional plug-in rules *)
    1.45 -val Action_simp_tac = action_simp_tac (simpset()) [] []
    1.46 -
    1.47 -end
    1.48  *}
    1.49  
    1.50  (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
    1.51 @@ -299,14 +283,9 @@
    1.52     - Solve for the unknowns using standard HOL reasoning.
    1.53     The following tactic combines these steps except the final one.
    1.54  *)
    1.55 -local
    1.56 -  val base_enabled = thm "base_enabled";
    1.57 -in
    1.58  
    1.59 -fun enabled_tac base_vars =
    1.60 -  clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset());
    1.61 -
    1.62 -end
    1.63 +fun enabled_tac (cs, ss) base_vars =
    1.64 +  clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
    1.65  *}
    1.66  
    1.67  (* Example *)
    1.68 @@ -314,7 +293,7 @@
    1.69  lemma
    1.70    assumes "basevars (x,y,z)"
    1.71    shows "|- x --> Enabled ($x & (y$ = #False))"
    1.72 -  apply (tactic {* enabled_tac (thm "assms") 1 *})
    1.73 +  apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
    1.74    apply auto
    1.75    done
    1.76