--- a/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri May 13 22:55:00 2011 +0200
@@ -14,51 +14,42 @@
(*Proves "co" properties when the program is specified. Any use of invariants
(from weak constrains) must have been done already.*)
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"*)
- REPEAT (etac @{thm Always_ConstrainsI} 1
- ORELSE
- resolve_tac [@{thm StableI}, @{thm stableI},
- @{thm constrains_imp_Constrains}] 1),
- (*for safety, the totalize operator can be ignored*)
- simp_tac (HOL_ss addsimps
- [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
- rtac @{thm constrainsI} 1,
- full_simp_tac ss 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_full_simp_tac ss)]) i
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ (*reduce the fancy safety properties to "constrains"*)
+ REPEAT (etac @{thm Always_ConstrainsI} 1
+ ORELSE
+ resolve_tac [@{thm StableI}, @{thm stableI},
+ @{thm constrains_imp_Constrains}] 1),
+ (*for safety, the totalize operator can be ignored*)
+ simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
+ rtac @{thm constrainsI} 1,
+ full_simp_tac (simpset_of ctxt) 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
(*proves "ensures/leadsTo" properties when the program is specified*)
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
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
- @{thm EnsuresI}, @{thm ensuresI}] 1),
- (*now there are two subgoals: co & transient*)
- simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
- res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm totalize_transientI} 2
- ORELSE res_inst_tac (Simplifier.the_context ss)
- [(("act", 0), sact)] @{thm transientI} 2,
- (*simplify the command's domain*)
- simp_tac (ss addsimps [@{thm Domain_def}]) 3,
- constrains_tac ctxt 1,
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_lr_simp_tac ss)])
- end;
+ SELECT_GOAL
+ (EVERY
+ [REPEAT (Always_Int_tac 1),
+ etac @{thm Always_LeadsTo_Basis} 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
+ @{thm EnsuresI}, @{thm ensuresI}] 1),
+ (*now there are two subgoals: co & transient*)
+ simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
+ res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm totalize_transientI} 2
+ ORELSE res_inst_tac ctxt
+ [(("act", 0), sact)] @{thm transientI} 2,
+ (*simplify the command's domain*)
+ simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
+ constrains_tac ctxt 1,
+ ALLGOALS (clarify_tac ctxt),
+ ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
(*Composition equivalences, from Lift_prog*)