# HG changeset patch
# User wenzelm
# Date 1305217086 -7200
# Node ID e6d920bea7a6816022067cc2b7a4c79f4af5343f
# Parent  92173262cfe90c266222f0138656368937a213a9
prefer Proof.context over old-style clasimpset;

diff -r 92173262cfe9 -r e6d920bea7a6 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:18:06 2011 +0200
@@ -330,15 +330,15 @@
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 ML {*
-fun record_auto_tac (cs, ss) =
-  auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper,
-    ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+fun record_auto_tac ctxt =
+  auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
+    simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
       @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
       @{thm o_apply}, @{thm Let_def}])
 *}
 
 method_setup record_auto = {*
-  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
+  Scan.succeed (SIMPLE_METHOD o record_auto_tac)
 *} ""
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
diff -r 92173262cfe9 -r e6d920bea7a6 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu May 12 18:18:06 2011 +0200
@@ -101,7 +101,11 @@
 
 text{*This ML code does the inductions directly.*}
 ML{*
-fun ns_constrains_tac(cs,ss) i =
+fun ns_constrains_tac ctxt i =
+  let
+    val cs = claset_of ctxt;
+    val ss = simpset_of ctxt;
+  in
    SELECT_GOAL
       (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1),
               REPEAT (resolve_tac [@{thm StableI}, @{thm stableI},
@@ -111,21 +115,26 @@
               REPEAT (FIRSTGOAL (etac disjE)),
               ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])),
               REPEAT (FIRSTGOAL analz_mono_contra_tac),
-              ALLGOALS (asm_simp_tac ss)]) i;
+              ALLGOALS (asm_simp_tac ss)]) i
+  end;
 
 (*Tactic for proving secrecy theorems*)
-fun ns_induct_tac(cs,ss) =
-  (SELECT_GOAL o EVERY)
-     [rtac @{thm AlwaysI} 1,
-      force_tac (cs,ss) 1,
-      (*"reachable" gets in here*)
-      rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
-      ns_constrains_tac(cs,ss) 1];
+fun ns_induct_tac ctxt =
+  let
+    val cs = claset_of ctxt;
+    val ss = simpset_of ctxt;
+  in
+    (SELECT_GOAL o EVERY)
+       [rtac @{thm AlwaysI} 1,
+        force_tac (cs,ss) 1,
+        (*"reachable" gets in here*)
+        rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1,
+        ns_constrains_tac ctxt 1]
+  end;
 *}
 
 method_setup ns_induct = {*
-    Scan.succeed (fn ctxt =>
-        SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *}
+    Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *}
     "for inductive reasoning about the Needham-Schroeder protocol"
 
 text{*Converts invariants into statements about reachable states*}
diff -r 92173262cfe9 -r e6d920bea7a6 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Thu May 12 18:18:06 2011 +0200
@@ -11,13 +11,12 @@
 begin
 
 method_setup safety = {*
-    Scan.succeed (fn ctxt =>
-        SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
+    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
     "for proving safety properties"
 
 method_setup ensures_tac = {*
   Args.goal_spec -- Scan.lift Args.name_source >>
-  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
+  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"
 
 end
diff -r 92173262cfe9 -r e6d920bea7a6 src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu May 12 18:18:06 2011 +0200
@@ -13,7 +13,11 @@
 
 (*Proves "co" properties when the program is specified.  Any use of invariants
   (from weak constrains) must have been done already.*)
-fun constrains_tac(cs,ss) i =
+fun constrains_tac ctxt i =
+  let
+    val cs = claset_of ctxt;
+    val ss = simpset_of ctxt;
+  in
    SELECT_GOAL
       (EVERY [REPEAT (Always_Int_tac 1),
               (*reduce the fancy safety properties to "constrains"*)
@@ -28,10 +32,15 @@
               full_simp_tac ss 1,
               REPEAT (FIRSTGOAL (etac disjE)),
               ALLGOALS (clarify_tac cs),
-              ALLGOALS (asm_full_simp_tac ss)]) i;
+              ALLGOALS (asm_full_simp_tac ss)]) i
+  end;
 
 (*proves "ensures/leadsTo" properties when the program is specified*)
-fun ensures_tac(cs,ss) sact =
+fun ensures_tac ctxt sact =
+  let
+    val cs = claset_of ctxt;
+    val ss = simpset_of ctxt;
+  in
     SELECT_GOAL
       (EVERY [REPEAT (Always_Int_tac 1),
               etac @{thm Always_LeadsTo_Basis} 1
@@ -46,9 +55,10 @@
                 [(("act", 0), sact)] @{thm transientI} 2,
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [@{thm Domain_def}]) 3,
-              constrains_tac (cs,ss) 1,
+              constrains_tac ctxt 1,
               ALLGOALS (clarify_tac cs),
-              ALLGOALS (asm_lr_simp_tac ss)]);
+              ALLGOALS (asm_lr_simp_tac ss)])
+  end;
 
 
 (*Composition equivalences, from Lift_prog*)