src/HOL/UNITY/UNITY_Main.thy
author wenzelm
Thu, 12 May 2011 18:18:06 +0200
changeset 42767 e6d920bea7a6
parent 32689 860e1a2317bd
child 42795 66fcc9882784
permissions -rw-r--r--
prefer Proof.context over old-style clasimpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/UNITY_Main.thy
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     3
    Copyright   2003  University of Cambridge
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13786
diff changeset
     4
*)
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     5
13798
4c1a53627500 conversion to new-style theories and tidying
paulson
parents: 13786
diff changeset
     6
header{*Comprehensive UNITY Theory*}
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
     7
32689
860e1a2317bd tuned proof; tuned headers
haftmann
parents: 32149
diff changeset
     8
theory UNITY_Main
860e1a2317bd tuned proof; tuned headers
haftmann
parents: 32149
diff changeset
     9
imports Detects PPROD Follows ProgressSets
860e1a2317bd tuned proof; tuned headers
haftmann
parents: 32149
diff changeset
    10
uses "UNITY_tactics.ML"
860e1a2317bd tuned proof; tuned headers
haftmann
parents: 32149
diff changeset
    11
begin
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    12
16184
80617b8d33c5 renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15032
diff changeset
    13
method_setup safety = {*
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 32689
diff changeset
    14
    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    15
    "for proving safety properties"
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    16
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    17
method_setup ensures_tac = {*
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    18
  Args.goal_spec -- Scan.lift Args.name_source >>
42767
e6d920bea7a6 prefer Proof.context over old-style clasimpset;
wenzelm
parents: 32689
diff changeset
    19
  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    20
*} "for proving progress properties"
13786
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    21
ab8f39f48a6f More conversion of UNITY to Isar new-style theories
paulson
parents:
diff changeset
    22
end