1(* Title: HOL/UNITY/UNITY_tactics.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2003 University of Cambridge 4 5Specialized UNITY tactics. 6*) 7 8(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) 9fun Always_Int_tac ctxt = 10 dresolve_tac ctxt @{thms Always_Int_I} THEN' 11 assume_tac ctxt THEN' 12 eresolve_tac ctxt @{thms Always_thin} 13 14(*Combines a list of invariance THEOREMS into one.*) 15val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) 16 17(*Proves "co" properties when the program is specified. Any use of invariants 18 (from weak constrains) must have been done already.*) 19fun constrains_tac ctxt i = 20 SELECT_GOAL 21 (EVERY 22 [REPEAT (Always_Int_tac ctxt 1), 23 (*reduce the fancy safety properties to "constrains"*) 24 REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1 25 ORELSE 26 resolve_tac ctxt [@{thm StableI}, @{thm stableI}, 27 @{thm constrains_imp_Constrains}] 1), 28 (*for safety, the totalize operator can be ignored*) 29 simp_tac (put_simpset HOL_ss ctxt 30 addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, 31 resolve_tac ctxt @{thms constrainsI} 1, 32 full_simp_tac ctxt 1, 33 REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])), 34 ALLGOALS (clarify_tac ctxt), 35 ALLGOALS (asm_full_simp_tac ctxt)]) i; 36 37(*proves "ensures/leadsTo" properties when the program is specified*) 38fun ensures_tac ctxt sact = 39 SELECT_GOAL 40 (EVERY 41 [REPEAT (Always_Int_tac ctxt 1), 42 eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 43 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) 44 REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, 45 @{thm EnsuresI}, @{thm ensuresI}] 1), 46 (*now there are two subgoals: co & transient*) 47 simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2, 48 Rule_Insts.res_inst_tac ctxt 49 [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2 50 ORELSE Rule_Insts.res_inst_tac ctxt 51 [((("act", 0), Position.none), sact)] [] @{thm transientI} 2, 52 (*simplify the command's domain*) 53 simp_tac (ctxt addsimps @{thms Domain_unfold}) 3, 54 constrains_tac ctxt 1, 55 ALLGOALS (clarify_tac ctxt), 56 ALLGOALS (asm_lr_simp_tac ctxt)]); 57 58 59(*Composition equivalences, from Lift_prog*) 60 61fun make_o_equivs ctxt th = 62 [th, 63 th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]), 64 th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])]; 65 66