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