# HG changeset patch # User wenzelm # Date 1205775427 -3600 # Node ID 651371f29e0089c097855794e91ca72587f86c00 # Parent 02fbd0e7954a503cbb4afb4381d174cfedb97610 avoid rebinding of existing facts; proper ML antiquotations; diff -r 02fbd0e7954a -r 651371f29e00 src/HOL/TLA/TLA.thy --- 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)) *} diff -r 02fbd0e7954a -r 651371f29e00 src/HOLCF/IOA/NTP/Impl.thy --- 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