src/HOL/UNITY/UNITY_Main.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 63146 f1ecba0272f9
child 69605 a96320074298
permissions -rw-r--r--
more robust sorted_entries;
     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\<open>Comprehensive UNITY Theory\<close>
     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 = \<open>
    15     Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
    16     "for proving safety properties"
    17 
    18 method_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 
    23 setup \<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 
    29 end