
diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/Hoare_Parallel/OG_Tactics.thy
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -273,11 +273,16 @@
 lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
 
 ML {*
-val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
+fun before_interfree_simp_tac ctxt =
+  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm com.simps}, @{thm post.simps}])
 
-val  interfree_simp_tac = asm_simp_tac (HOL_ss addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
+fun interfree_simp_tac ctxt =
+  asm_simp_tac (put_simpset HOL_ss ctxt
+    addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
 
-val ParallelConseq = simp_tac (HOL_basic_ss addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
+fun ParallelConseq ctxt =
+  simp_tac (put_simpset HOL_basic_ss ctxt
+    addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
 *}
 
 text {* The following tactic applies @{text tac} to each conjunct in a
@@ -320,120 +325,120 @@
 
 ML {*
 
- fun WlpTac i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac false (i+1))
-and HoareRuleTac precond i st = st |>  
-    ( (WlpTac i THEN HoareRuleTac precond i)
+fun WlpTac ctxt i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac ctxt false (i+1))
+and HoareRuleTac ctxt precond i st = st |>  
+    ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i)
       ORELSE
       (FIRST[rtac (@{thm SkipRule}) i,
              rtac (@{thm BasicRule}) i,
              EVERY[rtac (@{thm ParallelConseqRule}) i,
-                   ParallelConseq (i+2),
-                   ParallelTac (i+1),
-                   ParallelConseq i], 
+                   ParallelConseq ctxt (i+2),
+                   ParallelTac ctxt (i+1),
+                   ParallelConseq ctxt i], 
              EVERY[rtac (@{thm CondRule}) i,
-                   HoareRuleTac false (i+2),
-                   HoareRuleTac false (i+1)],
+                   HoareRuleTac ctxt false (i+2),
+                   HoareRuleTac ctxt false (i+1)],
              EVERY[rtac (@{thm WhileRule}) i,
-                   HoareRuleTac true (i+1)],
+                   HoareRuleTac ctxt true (i+1)],
              K all_tac i ]
        THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
 
-and  AnnWlpTac i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac (i+1))
-and AnnHoareRuleTac i st = st |>  
-    ( (AnnWlpTac i THEN AnnHoareRuleTac i )
+and AnnWlpTac ctxt i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac ctxt (i+1))
+and AnnHoareRuleTac ctxt i st = st |>  
+    ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i )
      ORELSE
       (FIRST[(rtac (@{thm AnnskipRule}) i),
              EVERY[rtac (@{thm AnnatomRule}) i,
-                   HoareRuleTac true (i+1)],
+                   HoareRuleTac ctxt true (i+1)],
              (rtac (@{thm AnnwaitRule}) i),
              rtac (@{thm AnnBasic}) i,
              EVERY[rtac (@{thm AnnCond1}) i,
-                   AnnHoareRuleTac (i+3),
-                   AnnHoareRuleTac (i+1)],
+                   AnnHoareRuleTac ctxt (i+3),
+                   AnnHoareRuleTac ctxt (i+1)],
              EVERY[rtac (@{thm AnnCond2}) i,
-                   AnnHoareRuleTac (i+1)],
+                   AnnHoareRuleTac ctxt (i+1)],
              EVERY[rtac (@{thm AnnWhile}) i,
-                   AnnHoareRuleTac (i+2)],
+                   AnnHoareRuleTac ctxt (i+2)],
              EVERY[rtac (@{thm AnnAwait}) i,
-                   HoareRuleTac true (i+1)],
+                   HoareRuleTac ctxt true (i+1)],
              K all_tac i]))
 
-and ParallelTac i = EVERY[rtac (@{thm ParallelRule}) i,
-                          interfree_Tac (i+1),
-                           MapAnn_Tac i]
+and ParallelTac ctxt i = EVERY[rtac (@{thm ParallelRule}) i,
+                          interfree_Tac ctxt (i+1),
+                           MapAnn_Tac ctxt i]
 
-and MapAnn_Tac i st = st |>
+and MapAnn_Tac ctxt i st = st |>
     (FIRST[rtac (@{thm MapAnnEmpty}) i,
            EVERY[rtac (@{thm MapAnnList}) i,
-                 MapAnn_Tac (i+1),
-                 AnnHoareRuleTac i],
+                 MapAnn_Tac ctxt (i+1),
+                 AnnHoareRuleTac ctxt i],
            EVERY[rtac (@{thm MapAnnMap}) i,
-                 rtac (@{thm allI}) i,rtac (@{thm impI}) i,
-                 AnnHoareRuleTac i]])
+                 rtac (@{thm allI}) i, rtac (@{thm impI}) i,
+                 AnnHoareRuleTac ctxt i]])
 
-and interfree_swap_Tac i st = st |>
+and interfree_swap_Tac ctxt i st = st |>
     (FIRST[rtac (@{thm interfree_swap_Empty}) i,
            EVERY[rtac (@{thm interfree_swap_List}) i,
-                 interfree_swap_Tac (i+2),
-                 interfree_aux_Tac (i+1),
-                 interfree_aux_Tac i ],
+                 interfree_swap_Tac ctxt (i+2),
+                 interfree_aux_Tac ctxt (i+1),
+                 interfree_aux_Tac ctxt i ],
            EVERY[rtac (@{thm interfree_swap_Map}) i,
                  rtac (@{thm allI}) i,rtac (@{thm impI}) i,
-                 conjI_Tac (interfree_aux_Tac) i]])
+                 conjI_Tac (interfree_aux_Tac ctxt) i]])
 
-and interfree_Tac i st = st |> 
+and interfree_Tac ctxt i st = st |> 
    (FIRST[rtac (@{thm interfree_Empty}) i,
           EVERY[rtac (@{thm interfree_List}) i,
-                interfree_Tac (i+1),
-                interfree_swap_Tac i],
+                interfree_Tac ctxt (i+1),
+                interfree_swap_Tac ctxt i],
           EVERY[rtac (@{thm interfree_Map}) i,
                 rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
-                interfree_aux_Tac i ]])
+                interfree_aux_Tac ctxt i ]])
 
-and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN 
+and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN 
         (FIRST[rtac (@{thm interfree_aux_rule1}) i,
-               dest_assertions_Tac i])
+               dest_assertions_Tac ctxt i])
 
-and dest_assertions_Tac i st = st |>
+and dest_assertions_Tac ctxt i st = st |>
     (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
-                 dest_atomics_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_atomics_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnSeq_assertions}) i,
-                 dest_assertions_Tac (i+1),
-                 dest_assertions_Tac i],
+                 dest_assertions_Tac ctxt (i+1),
+                 dest_assertions_Tac ctxt i],
            EVERY[rtac (@{thm AnnCond1_assertions}) i,
-                 dest_assertions_Tac (i+2),
-                 dest_assertions_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_assertions_Tac ctxt (i+2),
+                 dest_assertions_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnCond2_assertions}) i,
-                 dest_assertions_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_assertions_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnWhile_assertions}) i,
-                 dest_assertions_Tac (i+2),
-                 dest_atomics_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_assertions_Tac ctxt (i+2),
+                 dest_atomics_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnAwait_assertions}) i,
-                 dest_atomics_Tac (i+1),
-                 dest_atomics_Tac i],
-           dest_atomics_Tac i])
+                 dest_atomics_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
+           dest_atomics_Tac ctxt i])
 
-and dest_atomics_Tac i st = st |>
+and dest_atomics_Tac ctxt i st = st |>
     (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
-                 HoareRuleTac true i],
+                 HoareRuleTac ctxt true i],
            EVERY[rtac (@{thm AnnSeq_atomics}) i,
-                 dest_atomics_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_atomics_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnCond1_atomics}) i,
-                 dest_atomics_Tac (i+1),
-                 dest_atomics_Tac i],
+                 dest_atomics_Tac ctxt (i+1),
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnCond2_atomics}) i,
-                 dest_atomics_Tac i],
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm AnnWhile_atomics}) i,
-                 dest_atomics_Tac i],
+                 dest_atomics_Tac ctxt i],
            EVERY[rtac (@{thm Annatom_atomics}) i,
-                 HoareRuleTac true i],
+                 HoareRuleTac ctxt true i],
            EVERY[rtac (@{thm AnnAwait_atomics}) i,
-                 HoareRuleTac true i],
+                 HoareRuleTac ctxt true i],
                  K all_tac i])
 *}
 
@@ -441,8 +446,7 @@
 text {* The final tactic is given the name @{text oghoare}: *}
 
 ML {* 
-val oghoare_tac = SUBGOAL (fn (_, i) =>
-   (HoareRuleTac true i))
+fun oghoare_tac ctxt = SUBGOAL (fn (_, i) => HoareRuleTac ctxt true i)
 *}
 
 text {* Notice that the tactic for parallel programs @{text
@@ -453,26 +457,25 @@
 verification conditions for annotated sequential programs and to
 generate verification conditions out of interference freedom tests: *}
 
-ML {* val annhoare_tac = SUBGOAL (fn (_, i) =>
-  (AnnHoareRuleTac i))
+ML {*
+fun annhoare_tac ctxt = SUBGOAL (fn (_, i) => AnnHoareRuleTac ctxt i)
 
-val interfree_aux_tac = SUBGOAL (fn (_, i) =>
-   (interfree_aux_Tac i))
+fun interfree_aux_tac ctxt = SUBGOAL (fn (_, i) => interfree_aux_Tac ctxt i)
 *}
 
 text {* The so defined ML tactics are then ``exported'' to be used in
 Isabelle proofs. *}
 
 method_setup oghoare = {*
-  Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
+  Scan.succeed (SIMPLE_METHOD' o oghoare_tac) *}
   "verification condition generator for the oghoare logic"
 
 method_setup annhoare = {*
-  Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
+  Scan.succeed (SIMPLE_METHOD' o annhoare_tac) *}
   "verification condition generator for the ann_hoare logic"
 
 method_setup interfree_aux = {*
-  Scan.succeed (K (SIMPLE_METHOD' interfree_aux_tac)) *}
+  Scan.succeed (SIMPLE_METHOD' o interfree_aux_tac) *}
   "verification condition generator for interference freedom tests"
 
 text {* Tactics useful for dealing with the generated verification conditions: *}




