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