--- 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));
--- 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
--- 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 (<N1>_(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 (<N2>_(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 (<N2>_(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 (<N1>_(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 (<N1>_(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
--- 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 {*
--- 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
--- 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])