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
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
paulson@13798
     6
header{*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