--- a/src/HOL/TLA/TLA.thy Mon Mar 17 18:37:05 2008 +0100
+++ b/src/HOL/TLA/TLA.thy Mon Mar 17 18:37:07 2008 +0100
@@ -115,26 +115,19 @@
functions defined in theory Intensional in that they introduce a
"world" parameter of type "behavior".
*)
-local
- val action_rews = thms "action_rews";
- val tempD = thm "tempD";
-in
-
fun temp_unlift th =
- (rewrite_rule action_rews (th RS tempD)) handle THM _ => action_unlift th;
+ (rewrite_rule @{thms action_rews} (th RS @{thm tempD})) handle THM _ => action_unlift th;
(* Turn |- F = G into meta-level rewrite rule F == G *)
val temp_rewrite = int_rewrite
fun temp_use th =
case (concl_of th) of
- Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+ Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
((flatten (temp_unlift th)) handle THM _ => th)
| _ => th;
fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
-
-end
*}
setup {*
@@ -150,7 +143,7 @@
declare tempI [intro!]
declare tempD [dest]
ML {*
-val temp_css = (claset(), simpset())
+val temp_css = (@{claset}, @{simpset})
val temp_cs = op addss temp_css
*}
@@ -309,30 +302,20 @@
lemma box_thin: "[| sigma |= []F; PROP W |] ==> PROP W" .
ML {*
-local
- val box_conjE = thm "box_conjE";
- val box_thin = thm "box_thin";
- val box_conjE_temp = thm "box_conjE_temp";
- val box_conjE_stp = thm "box_conjE_stp";
- val box_conjE_act = thm "box_conjE_act";
-in
-
fun merge_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE i, atac i, etac box_thin i])
+ REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
fun merge_temp_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_temp i, atac i,
- eres_inst_tac [("'a","behavior")] box_thin i])
+ REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
+ eres_inst_tac [("'a","behavior")] @{thm box_thin} i])
fun merge_stp_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_stp i, atac i,
- eres_inst_tac [("'a","state")] box_thin i])
+ REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
+ eres_inst_tac [("'a","state")] @{thm box_thin} i])
fun merge_act_box_tac i =
- REPEAT_DETERM (EVERY [etac box_conjE_act i, atac i,
- eres_inst_tac [("'a","state * state")] box_thin i])
-
-end
+ REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
+ eres_inst_tac [("'a","state * state")] @{thm box_thin} i])
*}
(* rewrite rule to push universal quantification through box:
@@ -450,7 +433,7 @@
(* Make these rewrites active by default *)
ML {*
-val temp_css = temp_css addsimps2 (thms "temp_simps")
+val temp_css = temp_css addsimps2 @{thms temp_simps}
val temp_cs = op addss temp_css
*}
@@ -466,7 +449,7 @@
(* These are not declared by default, because they could be harmful,
e.g. []F & ~[]F becomes []F & <>~F !! *)
-lemmas more_temp_simps =
+lemmas more_temp_simps1 =
STL3 [temp_rewrite] DmdDmd [temp_rewrite] NotBox [temp_rewrite] NotDmd [temp_rewrite]
NotBox [temp_unlift, THEN eq_reflection]
NotDmd [temp_unlift, THEN eq_reflection]
@@ -480,7 +463,7 @@
apply (drule STL6 [temp_use])
apply assumption
apply simp
- apply (simp_all add: more_temp_simps)
+ apply (simp_all add: more_temp_simps1)
done
lemma DmdBoxDmd: "|- (<>[]<>F) = ([]<>F)"
@@ -488,7 +471,7 @@
apply (auto simp: BoxDmdBox [unfolded dmd_def, try_rewrite])
done
-lemmas more_temp_simps = more_temp_simps BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
+lemmas more_temp_simps2 = more_temp_simps1 BoxDmdBox [temp_rewrite] DmdBoxDmd [temp_rewrite]
(* ------------------------ Miscellaneous ----------------------------------- *)
@@ -500,7 +483,7 @@
lemma DBImplBD: "|- <>[]F --> []<>F"
apply clarsimp
apply (rule ccontr)
- apply (simp add: more_temp_simps)
+ apply (simp add: more_temp_simps2)
apply (drule STL6 [temp_use])
apply assumption
apply simp
@@ -509,7 +492,7 @@
lemma BoxDmdDmdBox: "|- []<>F & <>[]G --> []<>(F & G)"
apply clarsimp
apply (rule ccontr)
- apply (unfold more_temp_simps)
+ apply (unfold more_temp_simps2)
apply (drule STL6 [temp_use])
apply assumption
apply (subgoal_tac "sigma |= <>[]~F")
@@ -571,7 +554,7 @@
lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
-lemmas more_temp_simps = box_stp_act [temp_rewrite] more_temp_simps
+lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
lemma INV1:
"|- (Init P) --> (stable P) --> []P"
@@ -609,20 +592,12 @@
(* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
ML {*
-local
- val INV1 = thm "INV1";
- val Stable = thm "Stable";
- val Init_stp = thm "Init_stp";
- val Init_act = thm "Init_act";
- val squareE = thm "squareE";
-in
-
(* inv_tac reduces goals of the form ... ==> sigma |= []P *)
fun inv_tac css = SELECT_GOAL
(EVERY [auto_tac css,
TRY (merge_box_tac 1),
- rtac (temp_use INV1) 1, (* fail if the goal is not a box *)
- TRYALL (etac Stable)]);
+ rtac (temp_use @{thm INV1}) 1, (* fail if the goal is not a box *)
+ TRYALL (etac @{thm Stable})]);
(* auto_inv_tac applies inv_tac and then tries to attack the subgoals
in simple cases it may be able to handle goals like |- MyProg --> []Inv.
@@ -631,9 +606,9 @@
too late.
*)
fun auto_inv_tac ss = SELECT_GOAL
- ((inv_tac (claset(),ss) 1) THEN
- (TRYALL (action_simp_tac (ss addsimps [Init_stp, Init_act]) [] [squareE])));
-end
+ ((inv_tac (@{claset}, ss) 1) THEN
+ (TRYALL (action_simp_tac
+ (ss addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
*}
lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
@@ -673,7 +648,7 @@
apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
apply (force simp: boxInit_stp [temp_use]
elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
- apply (force intro!: STL6 [temp_use] simp: more_temp_simps)
+ apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
apply (fastsimp intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
done
@@ -700,18 +675,18 @@
(* theorems to "box" fairness conditions *)
lemma BoxWFI: "|- WF(A)_v --> []WF(A)_v"
- by (auto simp: WF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
+ by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
by (fastsimp intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
- by (auto simp: SF_alt [try_rewrite] more_temp_simps intro!: BoxOr [temp_use])
+ by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
by (fastsimp intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
-lemmas more_temp_simps = more_temp_simps WF_Box [temp_rewrite] SF_Box [temp_rewrite]
+lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
apply (unfold SF_def WF_def)
@@ -720,12 +695,7 @@
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
ML {*
-local
- val BoxWFI = thm "BoxWFI";
- val BoxSFI = thm "BoxSFI";
-in
-val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [BoxWFI,BoxSFI] 1))
-end
+val box_fair_tac = SELECT_GOAL (REPEAT (dresolve_tac [@{thm BoxWFI}, @{thm BoxSFI}] 1))
*}
--- a/src/HOLCF/IOA/NTP/Impl.thy Mon Mar 17 18:37:05 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy Mon Mar 17 18:37:07 2008 +0100
@@ -112,17 +112,17 @@
3) renname_ss unfolds transitions and the abstract channel *)
ML {*
-val ss = simpset() addsimps thms "transitions";
-val rename_ss = ss addsimps thms "unfold_renaming";
+val ss = @{simpset} addsimps @{thms transitions};
+val rename_ss = ss addsimps @{thms unfold_renaming};
-val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if])
-val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if])
+val tac = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
+val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
*}
subsubsection {* Invariant 1 *}
-lemma inv1: "invariant impl_ioa inv1"
+lemma raw_inv1: "invariant impl_ioa inv1"
apply (unfold impl_ioas)
apply (rule invariantI)
@@ -197,7 +197,7 @@
subsubsection {* INVARIANT 2 *}
-lemma inv2: "invariant impl_ioa inv2"
+lemma raw_inv2: "invariant impl_ioa inv2"
apply (rule invariantI1)
txt {* Base case *}
@@ -208,45 +208,45 @@
txt {* 10 cases. First 4 are simple, since state doesn't change *}
-ML {* val tac2 = asm_full_simp_tac (ss addsimps [thm "inv2_def"]) *}
+ML {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
txt {* 10 - 7 *}
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
txt {* 6 *}
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
- (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
txt {* 6 - 5 *}
apply (tactic "EVERY1 [tac2,tac2]")
txt {* 4 *}
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
- (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
apply (tactic "tac2 1")
txt {* 3 *}
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
- (thm "inv1" RS thm "invariantE")] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
apply (tactic "tac2 1")
- apply (tactic {* fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
+ apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
apply arith
txt {* 2 *}
apply (tactic "tac2 1")
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
- (thm "inv1" RS thm "invariantE") RS conjunct1] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
apply (intro strip)
apply (erule conjE)+
apply simp
txt {* 1 *}
apply (tactic "tac2 1")
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv1_def"]
- (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
apply (intro strip)
apply (erule conjE)+
- apply (tactic {* fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")] *})
+ apply (tactic {* fold_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
apply simp
done
@@ -254,7 +254,7 @@
subsubsection {* INVARIANT 3 *}
-lemma inv3: "invariant impl_ioa inv3"
+lemma raw_inv3: "invariant impl_ioa inv3"
apply (rule invariantI)
txt {* Base case *}
@@ -263,7 +263,7 @@
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
-ML {* val tac3 = asm_full_simp_tac (ss addsimps [thm "inv3_def"]) *}
+ML {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
txt {* 10 - 8 *}
@@ -290,14 +290,14 @@
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
- (thm "inv2" RS thm "invariantE")] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
apply (erule conjE)+
apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
- apply (tactic {* forward_tac [rewrite_rule [thm "inv1_def"]
- (thm "inv1" RS thm "invariantE") RS conjunct2] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
apply (simp add: hdr_sum_def Multiset.count_def)
apply (rule add_le_mono)
apply (rule countm_props)
@@ -311,15 +311,15 @@
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
- (thm "inv2" RS thm "invariantE")] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
done
subsubsection {* INVARIANT 4 *}
-lemma inv4: "invariant impl_ioa inv4"
+lemma raw_inv4: "invariant impl_ioa inv4"
apply (rule invariantI)
txt {* Base case *}
@@ -328,7 +328,7 @@
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
-ML {* val tac4 = asm_full_simp_tac (ss addsimps [thm "inv4_def"]) *}
+ML {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
txt {* 10 - 2 *}
@@ -337,18 +337,18 @@
txt {* 2 b *}
apply (intro strip, (erule conjE)+)
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
- (thm "inv2" RS thm "invariantE")] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
apply simp
txt {* 1 *}
apply (tactic "tac4 1")
apply (intro strip, (erule conjE)+)
apply (rule ccontr)
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv2_def"]
- (thm "inv2" RS thm "invariantE")] 1 *})
- apply (tactic {* forward_tac [rewrite_rule [thm "Impl.inv3_def"]
- (thm "inv3" RS thm "invariantE")] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+ apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
+ (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
apply simp
apply (erule_tac x = "m" in allE)
apply simp
@@ -357,9 +357,9 @@
text {* rebind them *}
-lemmas inv1 = inv1 [THEN invariantE, unfolded inv1_def]
- and inv2 = inv2 [THEN invariantE, unfolded inv2_def]
- and inv3 = inv3 [THEN invariantE, unfolded inv3_def]
- and inv4 = inv4 [THEN invariantE, unfolded inv4_def]
+lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
+ and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
+ and inv3 = raw_inv3 [THEN invariantE, unfolded inv3_def]
+ and inv4 = raw_inv4 [THEN invariantE, unfolded inv4_def]
end