--- 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*)