src/HOL/UNITY/UNITY_Main.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42795 66fcc9882784
child 48891 c0eafbd55de3
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 uses "UNITY_tactics.ML"
    11 begin
    12 
    13 method_setup safety = {*
    14     Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    15     "for proving safety properties"
    16 
    17 method_setup ensures_tac = {*
    18   Args.goal_spec -- Scan.lift Args.name_source >>
    19   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
    20 *} "for proving progress properties"
    21 
    22 setup {*
    23   Simplifier.map_simpset_global (fn ss => ss
    24     addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair})
    25     addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map}))
    26 *}
    27 
    28 end