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";
```