src/HOL/UNITY/UNITY.ML
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5340 d75c03cf77b5
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     1 (*  Title:      HOL/UNITY/UNITY
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The basic UNITY theory (revised version, based upon the "co" operator)
     7 
     8 From Misra, "A Logic for Concurrent Programming", 1994
     9 *)
    10 
    11 set proof_timing;
    12 HOL_quantifiers := false;
    13 
    14 
    15 (*** constrains ***)
    16 
    17 val prems = Goalw [constrains_def]
    18     "(!!act s s'. [| act: acts;  (s,s') : act;  s: A |] ==> s': A') \
    19 \    ==> constrains acts A A'";
    20 by (blast_tac (claset() addIs prems) 1);
    21 qed "constrainsI";
    22 
    23 Goalw [constrains_def]
    24     "[| constrains acts A A'; act: acts;  (s,s'): act;  s: A |] ==> s': A'";
    25 by (Blast_tac 1);
    26 qed "constrainsD";
    27 
    28 Goalw [constrains_def] "constrains acts {} B";
    29 by (Blast_tac 1);
    30 qed "constrains_empty";
    31 
    32 Goalw [constrains_def] "constrains acts A UNIV";
    33 by (Blast_tac 1);
    34 qed "constrains_UNIV";
    35 AddIffs [constrains_empty, constrains_UNIV];
    36 
    37 Goalw [constrains_def]
    38     "[| constrains acts A A'; A'<=B' |] ==> constrains acts A B'";
    39 by (Blast_tac 1);
    40 qed "constrains_weaken_R";
    41 
    42 Goalw [constrains_def]
    43     "[| constrains acts A A'; B<=A |] ==> constrains acts B A'";
    44 by (Blast_tac 1);
    45 qed "constrains_weaken_L";
    46 
    47 Goalw [constrains_def]
    48    "[| constrains acts A A'; B<=A; A'<=B' |] ==> constrains acts B B'";
    49 by (Blast_tac 1);
    50 qed "constrains_weaken";
    51 
    52 (** Union **)
    53 
    54 Goalw [constrains_def]
    55     "[| constrains acts A A'; constrains acts B B' |]   \
    56 \    ==> constrains acts (A Un B) (A' Un B')";
    57 by (Blast_tac 1);
    58 qed "constrains_Un";
    59 
    60 Goalw [constrains_def]
    61     "ALL i:I. constrains acts (A i) (A' i) \
    62 \    ==> constrains acts (UN i:I. A i) (UN i:I. A' i)";
    63 by (Blast_tac 1);
    64 qed "ball_constrains_UN";
    65 
    66 Goalw [constrains_def]
    67     "[| ALL i. constrains acts (A i) (A' i) |] \
    68 \    ==> constrains acts (UN i. A i) (UN i. A' i)";
    69 by (Blast_tac 1);
    70 qed "all_constrains_UN";
    71 
    72 (** Intersection **)
    73 
    74 Goalw [constrains_def]
    75     "[| constrains acts A A'; constrains acts B B' |]   \
    76 \    ==> constrains acts (A Int B) (A' Int B')";
    77 by (Blast_tac 1);
    78 qed "constrains_Int";
    79 
    80 Goalw [constrains_def]
    81     "ALL i:I. constrains acts (A i) (A' i) \
    82 \    ==> constrains acts (INT i:I. A i) (INT i:I. A' i)";
    83 by (Blast_tac 1);
    84 qed "ball_constrains_INT";
    85 
    86 Goalw [constrains_def]
    87     "[| ALL i. constrains acts (A i) (A' i) |] \
    88 \    ==> constrains acts (INT i. A i) (INT i. A' i)";
    89 by (Blast_tac 1);
    90 qed "all_constrains_INT";
    91 
    92 Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
    93 by (Blast_tac 1);
    94 qed "constrains_imp_subset";
    95 
    96 Goalw [constrains_def]
    97     "[| id: acts; constrains acts A B; constrains acts B C |]   \
    98 \    ==> constrains acts A C";
    99 by (Blast_tac 1);
   100 qed "constrains_trans";
   101 
   102 
   103 (*** stable ***)
   104 
   105 Goalw [stable_def] "constrains acts A A ==> stable acts A";
   106 by (assume_tac 1);
   107 qed "stableI";
   108 
   109 Goalw [stable_def] "stable acts A ==> constrains acts A A";
   110 by (assume_tac 1);
   111 qed "stableD";
   112 
   113 Goalw [stable_def]
   114     "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
   115 by (blast_tac (claset() addIs [constrains_Un]) 1);
   116 qed "stable_Un";
   117 
   118 Goalw [stable_def]
   119     "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
   120 by (blast_tac (claset() addIs [constrains_Int]) 1);
   121 qed "stable_Int";
   122 
   123 Goalw [stable_def, constrains_def]
   124     "[| stable acts C; constrains acts A (C Un A') |]   \
   125 \    ==> constrains acts (C Un A) (C Un A')";
   126 by (Blast_tac 1);
   127 qed "stable_constrains_Un";
   128 
   129 Goalw [stable_def, constrains_def]
   130     "[| stable acts C; constrains acts (C Int A) A' |]   \
   131 \    ==> constrains acts (C Int A) (C Int A')";
   132 by (Blast_tac 1);
   133 qed "stable_constrains_Int";
   134 
   135 
   136 (*The Elimination Theorem.  The "free" m has become universally quantified!
   137   Should the premise be !!m instead of ALL m ?  Would make it harder to use
   138   in forward proof.*)
   139 Goalw [constrains_def]
   140     "[| ALL m. constrains acts {s. s x = m} (B m) |] \
   141 \    ==> constrains acts {s. s x : M} (UN m:M. B m)";
   142 by (Blast_tac 1);
   143 qed "elimination";
   144 
   145 
   146 (*As above, but for the trivial case of a one-variable state, in which the
   147   state is identified with its one variable.*)
   148 Goalw [constrains_def]
   149     "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
   150 by (Blast_tac 1);
   151 qed "elimination_sing";
   152 
   153 
   154 Goalw [constrains_def]
   155    "[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
   156 \   ==> constrains acts A (A' Un B')";
   157 by (Blast_tac 1);
   158 qed "constrains_cancel";
   159 
   160 
   161 
   162 (*** Theoretical Results from Section 6 ***)
   163 
   164 Goalw [constrains_def, strongest_rhs_def]
   165     "constrains acts A (strongest_rhs acts A )";
   166 by (Blast_tac 1);
   167 qed "constrains_strongest_rhs";
   168 
   169 Goalw [constrains_def, strongest_rhs_def]
   170     "constrains acts A B ==> strongest_rhs acts A <= B";
   171 by (Blast_tac 1);
   172 qed "strongest_rhs_is_strongest";