# HG changeset patch # User wenzelm # Date 1186521850 -7200 # Node ID 9f818139951be2a62bd68da2e8ec5ec35648198f # Parent c89d77d97f84d60b83d2046555c5120a6b6986d7 tuned ML setup; diff -r c89d77d97f84 -r 9f818139951b src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Aug 07 23:24:10 2007 +0200 @@ -29,31 +29,30 @@ by arith text{*A crude tactic to differentiate by proof.*} + +lemmas deriv_rulesI = + DERIV_ident DERIV_const DERIV_cos DERIV_cmult + DERIV_sin DERIV_exp DERIV_inverse DERIV_pow + DERIV_add DERIV_diff DERIV_mult DERIV_minus + DERIV_inverse_fun DERIV_quotient DERIV_fun_pow + DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos + DERIV_ident DERIV_const DERIV_cos + ML {* local -val deriv_rulesI = - [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult", - thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow", - thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus", - thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow", - thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos", - thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"]; - -val DERIV_chain2 = thm "DERIV_chain2"; - -in - exception DERIV_name; fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f | get_fun_name _ = raise DERIV_name; +in + val deriv_tac = SUBGOAL (fn (prem,i) => - (resolve_tac deriv_rulesI i) ORELSE + (resolve_tac @{thms deriv_rulesI} i) ORELSE ((rtac (read_instantiate [("f",get_fun_name prem)] - DERIV_chain2) i) handle DERIV_name => no_tac));; + @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));; val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); diff -r c89d77d97f84 -r 9f818139951b src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/TLA/Action.thy Tue Aug 07 23:24:10 2007 +0200 @@ -109,13 +109,9 @@ functions defined in Intensional.ML in that they introduce a "world" parameter of the form (s,t) and apply additional rewrites. *) -local - val action_rews = thms "action_rews"; - val actionD = thm "actionD"; -in fun action_unlift th = - (rewrite_rule action_rews (th RS actionD)) + (rewrite_rule @{thms action_rews} (th RS @{thm actionD})) handle THM _ => int_unlift th; (* Turn |- A = B into meta-level rewrite rule A == B *) @@ -126,8 +122,6 @@ Const _ $ (Const ("Intensional.Valid", _) $ _) => (flatten (action_unlift th) handle THM _ => th) | _ => th; - -end *} setup {* @@ -269,22 +263,12 @@ should plug in only "very safe" rules that can be applied blindly. Note that it applies whatever simplifications are currently active. *) -local - val actionI = thm "actionI"; - val intI = thm "intI"; -in - fun action_simp_tac ss intros elims = asm_full_simp_tac (ss setloop ((resolve_tac ((map action_use intros) - @ [refl,impI,conjI,actionI,intI,allI])) + @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) ORELSE' (eresolve_tac ((map action_use elims) @ [conjE,disjE,exE])))); - -(* default version without additional plug-in rules *) -val Action_simp_tac = action_simp_tac (simpset()) [] [] - -end *} (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *) @@ -299,14 +283,9 @@ - Solve for the unknowns using standard HOL reasoning. The following tactic combines these steps except the final one. *) -local - val base_enabled = thm "base_enabled"; -in -fun enabled_tac base_vars = - clarsimp_tac (claset() addSIs [base_vars RS base_enabled], simpset()); - -end +fun enabled_tac (cs, ss) base_vars = + clarsimp_tac (cs addSIs [base_vars RS @{thm base_enabled}], ss); *} (* Example *) @@ -314,7 +293,7 @@ lemma assumes "basevars (x,y,z)" shows "|- x --> Enabled ($x & (y$ = #False))" - apply (tactic {* enabled_tac (thm "assms") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm assms} 1 *}) apply auto done diff -r c89d77d97f84 -r 9f818139951b src/HOL/TLA/Inc/Inc.thy --- a/src/HOL/TLA/Inc/Inc.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/TLA/Inc/Inc.thy Tue Aug 07 23:24:10 2007 +0200 @@ -164,7 +164,7 @@ lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (_(x,y,sem,pc1,pc2))" apply clarsimp apply (rule_tac F = gamma1 in enabled_mono) - apply (tactic {* enabled_tac (thm "Inc_base") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *}) apply (force simp: gamma1_def) apply (force simp: angle_def gamma1_def N1_def) done @@ -186,7 +186,7 @@ lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (_(x,y,sem,pc1,pc2))" apply clarsimp apply (rule_tac F = gamma2 in enabled_mono) - apply (tactic {* enabled_tac (thm "Inc_base") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *}) apply (force simp: gamma2_def) apply (force simp: angle_def gamma2_def N2_def) done @@ -205,7 +205,7 @@ lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (_(x,y,sem,pc1,pc2))" apply clarsimp apply (rule_tac F = beta2 in enabled_mono) - apply (tactic {* enabled_tac (thm "Inc_base") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *}) apply (force simp: beta2_def) apply (force simp: angle_def beta2_def N2_def) done @@ -247,7 +247,7 @@ "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (_(x,y,sem,pc1,pc2))" apply clarsimp apply (rule_tac F = alpha1 in enabled_mono) - apply (tactic {* enabled_tac (thm "Inc_base") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *}) apply (force simp: alpha1_def PsiInv_defs) apply (force simp: angle_def alpha1_def N1_def) done @@ -288,7 +288,7 @@ lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (_(x,y,sem,pc1,pc2))" apply clarsimp apply (rule_tac F = beta1 in enabled_mono) - apply (tactic {* enabled_tac (thm "Inc_base") 1 *}) + apply (tactic {* enabled_tac @{clasimpset} @{thm Inc_base} 1 *}) apply (force simp: beta1_def) apply (force simp: angle_def beta1_def N1_def) done diff -r c89d77d97f84 -r 9f818139951b src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/TLA/Intensional.thy Tue Aug 07 23:24:10 2007 +0200 @@ -243,24 +243,17 @@ (* ======== Functions to "unlift" intensional implications into HOL rules ====== *) ML {* - -local - val intD = thm "intD"; - val inteq_reflection = thm "inteq_reflection"; - val intensional_rews = thms "intensional_rews"; -in - (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. |- F = G becomes F w = G w |- F --> G becomes F w --> G w *) fun int_unlift th = - rewrite_rule intensional_rews (th RS intD handle THM _ => th); + rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th); (* Turn |- F = G into meta-level rewrite rule F == G *) fun int_rewrite th = - zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection)) + zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection})) (* flattening turns "-->" into "==>" and eliminates conjunctions in the antecedent. For example, @@ -299,8 +292,6 @@ Const _ $ (Const ("Intensional.Valid", _) $ _) => (flatten (int_unlift th) handle THM _ => th) | _ => th - -end *} setup {* diff -r c89d77d97f84 -r 9f818139951b src/HOL/TLA/Memory/MIParameters.thy --- a/src/HOL/TLA/Memory/MIParameters.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/TLA/Memory/MIParameters.thy Tue Aug 07 23:24:10 2007 +0200 @@ -14,6 +14,4 @@ datatype histState = histA | histB -ML {* use_legacy_bindings (the_context ()) *} - end diff -r c89d77d97f84 -r 9f818139951b src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Aug 07 20:43:36 2007 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Aug 07 23:24:10 2007 +0200 @@ -115,7 +115,7 @@ (one- or two-element) set. NB: The second conjunct of the definition in the paper is taken care of by the type definitions. The last conjunct is asserted separately as the memory - invariant MemInv, proved in Memory.ML. *) + invariant MemInv, proved in Memory.thy. *) S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred" "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED Calling memCh p = #ecalling @@ -177,8 +177,8 @@ (* The main theorem is theorem "Implementation" at the end of this file, which shows that the composition of a reliable memory, an RPC component, and - a memory clerk implements an unreliable memory. The files "MIsafe.ML" and - "MIlive.ML" contain lower-level lemmas for the safety and liveness parts. + a memory clerk implements an unreliable memory. The files "MIsafe.thy" and + "MIlive.thy" contain lower-level lemmas for the safety and liveness parts. Steps are (roughly) numbered as in the hand proof. *) @@ -187,7 +187,7 @@ declare if_weak_cong [cong del] -ML {* val MI_css = (claset(), simpset()) *} +ML {* val MI_css = (@{claset}, @{simpset}) *} (* A more aggressive variant that tries to solve subgoals by assumption or contradiction during the simplification. @@ -200,7 +200,7 @@ let val (cs,ss) = MI_css in - (cs addSEs [temp_use (thm "squareE")], + (cs addSEs [temp_use @{thm squareE}], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE)))) end; @@ -762,19 +762,13 @@ steps of the implementation, and try to solve the idling case by simplification *) ML {* -local - val actionI = thm "actionI"; - val action_rews = thms "action_rews"; - val Step1_4_7 = thm "Step1_4_7"; -in -fun split_idle_tac simps i = - EVERY [TRY (rtac actionI i), +fun split_idle_tac ss simps i = + EVERY [TRY (rtac @{thm actionI} i), case_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i, - rewrite_goals_tac action_rews, - forward_tac [temp_use Step1_4_7] i, - asm_full_simp_tac (simpset() addsimps simps) i + rewrite_goals_tac @{thms action_rews}, + forward_tac [temp_use @{thm Step1_4_7}] i, + asm_full_simp_tac (ss addsimps simps) i ] -end *} (* ---------------------------------------------------------------------- Combine steps 1.2 and 1.4 to prove that the implementation satisfies @@ -786,7 +780,7 @@ lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" - apply (tactic {* split_idle_tac [thm "square_def"] 1 *}) + apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *}) apply force done (* turn into (unsafe, looping!) introduction rule *) @@ -858,7 +852,7 @@ lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) --> (S1 rmhist p)$ | (S2 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_1 [temp_use]) done @@ -892,7 +886,7 @@ lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) --> (S2 rmhist p)$ | (S3 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_2 [temp_use]) done @@ -918,7 +912,7 @@ lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_3 [temp_use]) done @@ -946,7 +940,7 @@ lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) --> (S4 rmhist p)$ | (S5 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_4 [temp_use]) done @@ -956,7 +950,7 @@ & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l) --> (S4 rmhist p & ires!p = #NotAResult)$ | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" - apply (tactic {* split_idle_tac [thm "m_def"] 1 *}) + apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *}) apply (auto dest!: Step1_2_4 [temp_use]) done @@ -987,7 +981,7 @@ lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult) & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$" - apply (tactic {* split_idle_tac [thm "m_def"] 1 *}) + apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *}) apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) done @@ -1016,7 +1010,7 @@ lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) --> (S5 rmhist p)$ | (S6 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_5 [temp_use]) done @@ -1042,7 +1036,7 @@ lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$" - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto dest!: Step1_2_6 [temp_use]) done @@ -1257,7 +1251,7 @@ apply clarsimp apply (drule WriteS4 [action_use]) apply assumption - apply (tactic "split_idle_tac [] 1") + apply (tactic "split_idle_tac @{simpset} [] 1") apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use] S4RPCUnch [temp_use]) apply (auto simp: square_def dest: S4Write [temp_use])