src/HOL/UNITY/UNITY_Main.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 55111 5792f5106c40
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 header{*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