1(* Title: HOL/UNITY/UNITY_Main.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 2003 University of Cambridge 4*) 5 6section\<open>Comprehensive UNITY Theory\<close> 7 8theory UNITY_Main 9imports Detects PPROD Follows ProgressSets 10begin 11 12ML_file \<open>UNITY_tactics.ML\<close> 13 14method_setup safety = \<open> 15 Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close> 16 "for proving safety properties" 17 18method_setup ensures_tac = \<open> 19 Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >> 20 (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) 21\<close> "for proving progress properties" 22 23setup \<open> 24 map_theory_simpset (fn ctxt => ctxt 25 addsimps (make_o_equivs ctxt @{thm fst_o_funPair} @ make_o_equivs ctxt @{thm snd_o_funPair}) 26 addsimps (make_o_equivs ctxt @{thm fst_o_lift_map} @ make_o_equivs ctxt @{thm snd_o_lift_map})) 27\<close> 28 29end 30