src/HOL/HOLCF/IOA/NTP/Impl.thy
changeset 51717 9e7d1c139569
parent 45620 f2a587696afb
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -102,13 +102,15 @@
     1.4  3) renname_ss unfolds transitions and the abstract channel *)
     1.5  
     1.6  ML {*
     1.7 -val ss = @{simpset} addsimps @{thms "transitions"};
     1.8 -val rename_ss = ss addsimps @{thms unfold_renaming};
     1.9 +val ss = simpset_of (@{context} addsimps @{thms "transitions"});
    1.10 +val rename_ss = simpset_of (put_simpset ss @{context} addsimps @{thms unfold_renaming});
    1.11  
    1.12 -val tac =
    1.13 -  asm_simp_tac (ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.14 -val tac_ren =
    1.15 -  asm_simp_tac (rename_ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.16 +fun tac ctxt =
    1.17 +  asm_simp_tac (put_simpset ss ctxt
    1.18 +    |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.19 +fun tac_ren ctxt =
    1.20 +  asm_simp_tac (put_simpset rename_ss ctxt
    1.21 +    |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.22  *}
    1.23  
    1.24  
    1.25 @@ -129,34 +131,34 @@
    1.26  apply (simp add: Impl.inv1_def split del: split_if)
    1.27  apply (induct_tac a)
    1.28  
    1.29 -apply (tactic "EVERY1[tac, tac, tac, tac]")
    1.30 -apply (tactic "tac 1")
    1.31 -apply (tactic "tac_ren 1")
    1.32 +apply (tactic "EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]")
    1.33 +apply (tactic "tac @{context} 1")
    1.34 +apply (tactic "tac_ren @{context} 1")
    1.35  
    1.36  txt {* 5 + 1 *}
    1.37  
    1.38 -apply (tactic "tac 1")
    1.39 -apply (tactic "tac_ren 1")
    1.40 +apply (tactic "tac @{context} 1")
    1.41 +apply (tactic "tac_ren @{context} 1")
    1.42  
    1.43  txt {* 4 + 1 *}
    1.44 -apply (tactic {* EVERY1[tac, tac, tac, tac] *})
    1.45 +apply (tactic {* EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}] *})
    1.46  
    1.47  
    1.48  txt {* Now the other half *}
    1.49  apply (simp add: Impl.inv1_def split del: split_if)
    1.50  apply (induct_tac a)
    1.51 -apply (tactic "EVERY1 [tac, tac]")
    1.52 +apply (tactic "EVERY1 [tac @{context}, tac @{context}]")
    1.53  
    1.54  txt {* detour 1 *}
    1.55 -apply (tactic "tac 1")
    1.56 -apply (tactic "tac_ren 1")
    1.57 +apply (tactic "tac @{context} 1")
    1.58 +apply (tactic "tac_ren @{context} 1")
    1.59  apply (rule impI)
    1.60  apply (erule conjE)+
    1.61  apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
    1.62    split add: split_if)
    1.63  txt {* detour 2 *}
    1.64 -apply (tactic "tac 1")
    1.65 -apply (tactic "tac_ren 1")
    1.66 +apply (tactic "tac @{context} 1")
    1.67 +apply (tactic "tac_ren @{context} 1")
    1.68  apply (rule impI)
    1.69  apply (erule conjE)+
    1.70  apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
    1.71 @@ -181,7 +183,8 @@
    1.72  apply (rule countm_spurious_delm)
    1.73  apply (simp (no_asm))
    1.74  
    1.75 -apply (tactic "EVERY1 [tac, tac, tac, tac, tac, tac]")
    1.76 +apply (tactic "EVERY1 [tac @{context}, tac @{context}, tac @{context},
    1.77 +  tac @{context}, tac @{context}, tac @{context}]")
    1.78  
    1.79  done
    1.80  
    1.81 @@ -200,7 +203,7 @@
    1.82  
    1.83    txt {* 10 cases. First 4 are simple, since state doesn't change *}
    1.84  
    1.85 -  ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
    1.86 +  ML_prf {* val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}]) *}
    1.87  
    1.88    txt {* 10 - 7 *}
    1.89    apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
    1.90 @@ -256,13 +259,13 @@
    1.91    apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
    1.92    apply (induct_tac "a")
    1.93  
    1.94 -  ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
    1.95 +  ML_prf {* val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}]) *}
    1.96  
    1.97    txt {* 10 - 8 *}
    1.98  
    1.99    apply (tactic "EVERY1[tac3,tac3,tac3]")
   1.100  
   1.101 -  apply (tactic "tac_ren 1")
   1.102 +  apply (tactic "tac_ren @{context} 1")
   1.103    apply (intro strip, (erule conjE)+)
   1.104    apply hypsubst
   1.105    apply (erule exE)
   1.106 @@ -270,7 +273,7 @@
   1.107  
   1.108    txt {* 7 *}
   1.109    apply (tactic "tac3 1")
   1.110 -  apply (tactic "tac_ren 1")
   1.111 +  apply (tactic "tac_ren @{context} 1")
   1.112    apply force
   1.113  
   1.114    txt {* 6 - 3 *}
   1.115 @@ -278,7 +281,7 @@
   1.116    apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
   1.117  
   1.118    txt {* 2 *}
   1.119 -  apply (tactic "asm_full_simp_tac ss 1")
   1.120 +  apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1")
   1.121    apply (simp (no_asm) add: inv3_def)
   1.122    apply (intro strip, (erule conjE)+)
   1.123    apply (rule imp_disjL [THEN iffD1])
   1.124 @@ -321,7 +324,7 @@
   1.125    apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   1.126    apply (induct_tac "a")
   1.127  
   1.128 -  ML_prf {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
   1.129 +  ML_prf {* val tac4 =  asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}]) *}
   1.130  
   1.131    txt {* 10 - 2 *}
   1.132