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 "UNITY_tactics.ML"
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