src/HOL/UNITY/UNITY_Main.thy
author wenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773 d09c66a0ea10
parent 58889 5b7a9633cfa8
child 63120 629a4c5e953e
permissions -rw-r--r--
more symbols by default, without xsymbols mode;
     1 (*  Title:      HOL/UNITY/UNITY_Main.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2003  University of Cambridge
     4 *)
     5 
     6 section{*Comprehensive UNITY Theory*}
     7 
     8 theory UNITY_Main
     9 imports Detects PPROD Follows ProgressSets
    10 begin
    11 
    12 ML_file "UNITY_tactics.ML"
    13 
    14 method_setup safety = {*
    15     Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    16     "for proving safety properties"
    17 
    18 method_setup ensures_tac = {*
    19   Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
    20   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
    21 *} "for proving progress properties"
    22 
    23 setup {*
    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 *}
    28 
    29 end