src/HOL/HOLCF/IOA/NTP/Impl.thy
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 58270 16648edf16e3
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -208,29 +208,29 @@
     1.4    txt {* 10 - 7 *}
     1.5    apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
     1.6    txt {* 6 *}
     1.7 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
     1.8 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
     1.9                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    1.10  
    1.11    txt {* 6 - 5 *}
    1.12    apply (tactic "EVERY1 [tac2,tac2]")
    1.13  
    1.14    txt {* 4 *}
    1.15 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    1.16 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
    1.17                                  (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    1.18    apply (tactic "tac2 1")
    1.19  
    1.20    txt {* 3 *}
    1.21 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    1.22 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
    1.23      (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
    1.24  
    1.25    apply (tactic "tac2 1")
    1.26 -  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
    1.27 +  apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
    1.28      (@{thm Impl.hdr_sum_def})] *})
    1.29    apply arith
    1.30  
    1.31    txt {* 2 *}
    1.32    apply (tactic "tac2 1")
    1.33 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    1.34 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
    1.35                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
    1.36    apply (intro strip)
    1.37    apply (erule conjE)+
    1.38 @@ -238,11 +238,12 @@
    1.39  
    1.40    txt {* 1 *}
    1.41    apply (tactic "tac2 1")
    1.42 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
    1.43 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
    1.44                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
    1.45    apply (intro strip)
    1.46    apply (erule conjE)+
    1.47 -  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
    1.48 +  apply (tactic {* fold_goals_tac @{context}
    1.49 +    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
    1.50    apply simp
    1.51  
    1.52    done
    1.53 @@ -286,13 +287,13 @@
    1.54    apply (intro strip, (erule conjE)+)
    1.55    apply (rule imp_disjL [THEN iffD1])
    1.56    apply (rule impI)
    1.57 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
    1.58 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
    1.59      (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
    1.60    apply simp
    1.61    apply (erule conjE)+
    1.62    apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
    1.63      k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
    1.64 -  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
    1.65 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
    1.66                                  (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
    1.67    apply (simp add: hdr_sum_def Multiset.count_def)
    1.68    apply (rule add_le_mono)
    1.69 @@ -307,7 +308,7 @@
    1.70    apply (intro strip, (erule conjE)+)
    1.71    apply (rule imp_disjL [THEN iffD1])
    1.72    apply (rule impI)
    1.73 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
    1.74 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
    1.75      (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
    1.76    apply simp
    1.77    done
    1.78 @@ -333,7 +334,7 @@
    1.79    txt {* 2 b *}
    1.80  
    1.81    apply (intro strip, (erule conjE)+)
    1.82 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
    1.83 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
    1.84                                 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
    1.85    apply simp
    1.86  
    1.87 @@ -341,9 +342,9 @@
    1.88    apply (tactic "tac4 1")
    1.89    apply (intro strip, (erule conjE)+)
    1.90    apply (rule ccontr)
    1.91 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
    1.92 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
    1.93                                 (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
    1.94 -  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
    1.95 +  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
    1.96                                 (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
    1.97    apply simp
    1.98    apply (erule_tac x = "m" in allE)