proper method_setup "enabled";
authorwenzelm
Fri May 13 14:04:47 2011 +0200 (2011-05-13)
changeset 4278515ec9b3c14cc
parent 42784 a2dca9a3d0da
child 42786 06a38b936342
proper method_setup "enabled";
src/HOL/TLA/Action.thy
src/HOL/TLA/Inc/Inc.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Fri May 13 13:45:20 2011 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri May 13 14:04:47 2011 +0200
     1.3 @@ -277,16 +277,20 @@
     1.4     The following tactic combines these steps except the final one.
     1.5  *)
     1.6  
     1.7 -fun enabled_tac (cs, ss) base_vars =
     1.8 -  clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss);
     1.9 +fun enabled_tac ctxt base_vars =
    1.10 +  clarsimp_tac (claset_of ctxt addSIs [base_vars RS @{thm base_enabled}], simpset_of ctxt);
    1.11  *}
    1.12  
    1.13 +method_setup enabled = {*
    1.14 +  Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
    1.15 +*} ""
    1.16 +
    1.17  (* Example *)
    1.18  
    1.19  lemma
    1.20    assumes "basevars (x,y,z)"
    1.21    shows "|- x --> Enabled ($x & (y$ = #False))"
    1.22 -  apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *})
    1.23 +  apply (enabled assms)
    1.24    apply auto
    1.25    done
    1.26  
     2.1 --- a/src/HOL/TLA/Inc/Inc.thy	Fri May 13 13:45:20 2011 +0200
     2.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Fri May 13 14:04:47 2011 +0200
     2.3 @@ -161,7 +161,7 @@
     2.4  lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
     2.5    apply clarsimp
     2.6    apply (rule_tac F = gamma1 in enabled_mono)
     2.7 -   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
     2.8 +   apply (enabled Inc_base)
     2.9    apply (force simp: gamma1_def)
    2.10    apply (force simp: angle_def gamma1_def N1_def)
    2.11    done
    2.12 @@ -183,7 +183,7 @@
    2.13  lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
    2.14    apply clarsimp
    2.15    apply (rule_tac F = gamma2 in enabled_mono)
    2.16 -  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    2.17 +  apply (enabled Inc_base)
    2.18     apply (force simp: gamma2_def)
    2.19    apply (force simp: angle_def gamma2_def N2_def)
    2.20    done
    2.21 @@ -202,7 +202,7 @@
    2.22  lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
    2.23    apply clarsimp
    2.24    apply (rule_tac F = beta2 in enabled_mono)
    2.25 -   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    2.26 +   apply (enabled Inc_base)
    2.27     apply (force simp: beta2_def)
    2.28    apply (force simp: angle_def beta2_def N2_def)
    2.29    done
    2.30 @@ -244,7 +244,7 @@
    2.31    "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
    2.32    apply clarsimp
    2.33    apply (rule_tac F = alpha1 in enabled_mono)
    2.34 -  apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    2.35 +  apply (enabled Inc_base)
    2.36     apply (force simp: alpha1_def PsiInv_defs)
    2.37    apply (force simp: angle_def alpha1_def N1_def)
    2.38    done
    2.39 @@ -285,7 +285,7 @@
    2.40  lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
    2.41    apply clarsimp
    2.42    apply (rule_tac F = beta1 in enabled_mono)
    2.43 -   apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *})
    2.44 +   apply (enabled Inc_base)
    2.45     apply (force simp: beta1_def)
    2.46    apply (force simp: angle_def beta1_def N1_def)
    2.47    done