src/HOL/UNITY/Union.ML
author paulson
Mon, 16 Nov 1998 10:39:30 +0100
changeset 5867 1c4806b4bf43
parent 5804 8e0a4c4fd67b
child 5898 3e34e7aa7479
permissions -rw-r--r--
generalized JN_empty and added reachable_SKIP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Union.ML
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     5
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     6
Unions of programs
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     7
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     8
From Misra's Chapter 5: Asynchronous Compositions of Programs
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
     9
*)
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    10
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    11
5867
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    12
(** SKIP **)
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    13
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    14
Goal "Init SKIP = UNIV";
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    15
by (simp_tac (simpset() addsimps [SKIP_def]) 1);
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    16
qed "Init_SKIP";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    17
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    18
Goal "Acts SKIP = {Id}";
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    19
by (simp_tac (simpset() addsimps [SKIP_def]) 1);
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    20
qed "Acts_SKIP";
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    21
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    22
Addsimps [Init_SKIP, Acts_SKIP];
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    23
5867
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    24
Goal "reachable SKIP = UNIV";
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    25
by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    26
qed "reachable_SKIP";
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    27
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    28
Addsimps [reachable_SKIP];
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    29
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    30
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    31
(** Join and JN **)
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    32
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    33
Goal "Init (F Join G) = Init F Int Init G";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    34
by (simp_tac (simpset() addsimps [Join_def]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    35
qed "Init_Join";
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    36
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    37
Goal "Acts (F Join G) = Acts F Un Acts G";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    38
by (auto_tac (claset(), simpset() addsimps [Join_def]));
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    39
qed "Acts_Join";
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    40
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    41
Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    42
by (simp_tac (simpset() addsimps [JOIN_def]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    43
qed "Init_JN";
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    44
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    45
Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    46
by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    47
qed "Acts_JN";
5252
1b0f14d11142 Union primitives and examples
paulson
parents:
diff changeset
    48
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    49
Addsimps [Init_Join, Init_JN];
5259
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    50
5867
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    51
Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    52
by Auto_tac;
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    53
qed "JN_empty";
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    54
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    55
Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    56
by (rtac program_equalityI 1);
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    57
by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    58
qed "JN_insert";
5867
1c4806b4bf43 generalized JN_empty and added reachable_SKIP
paulson
parents: 5804
diff changeset
    59
Addsimps[JN_empty, JN_insert];
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    60
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    61
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    62
(** Algebraic laws **)
5259
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    63
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    64
Goal "F Join G = G Join F";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    65
by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
5259
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    66
qed "Join_commute";
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    67
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    68
Goal "(F Join G) Join H = F Join (G Join H)";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    69
by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
5259
86d80749453f Null program and a few new results
paulson
parents: 5252
diff changeset
    70
qed "Join_assoc";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    71
 
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    72
Goalw [Join_def, SKIP_def] "SKIP Join F = F";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    73
by (rtac program_equalityI 1);
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    74
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    75
qed "Join_SKIP_left";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    76
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    77
Goalw [Join_def, SKIP_def] "F Join SKIP = F";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    78
by (rtac program_equalityI 1);
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    79
by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    80
qed "Join_SKIP_right";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    81
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    82
Addsimps [Join_SKIP_left, Join_SKIP_right];
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    83
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    84
Goalw [Join_def] "F Join F = F";
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    85
by (rtac program_equalityI 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    86
by Auto_tac;
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    87
qed "Join_absorb";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    88
5611
6957f124ca97 Join now an infix operator
paulson
parents: 5608
diff changeset
    89
Addsimps [Join_absorb];
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    90
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    91
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    92
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    93
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    94
(*** Safety: constrains, stable, FP ***)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    95
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
    96
Goalw [constrains_def, JOIN_def]
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
    97
    "I ~= {} ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
    98
\    (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)";
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
    99
by (Simp_tac 1);
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
   100
by (Blast_tac 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   101
qed "constrains_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   102
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   103
Goal "F Join G : constrains A B =  \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   104
\     (F : constrains A B & G : constrains A B)";
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   105
by (auto_tac
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   106
    (claset(),
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   107
     simpset() addsimps [constrains_def, Join_def]));
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   108
qed "constrains_Join";
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   109
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   110
(**FAILS, I think; see 5.4.1, Substitution Axiom.
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   111
   The problem is to relate reachable (F Join G) with 
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   112
   reachable F and reachable G
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   113
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   114
Goalw [Constrains_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   115
    "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   116
by (simp_tac (simpset() addsimps [constrains_JN]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   117
by (Blast_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   118
qed "Constrains_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   119
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   120
Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   121
by (auto_tac
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   122
    (claset(),
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   123
     simpset() addsimps [Constrains_def, constrains_Join]));
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   124
qed "Constrains_Join";
3ac11c4af76a tidying and renaming
paulson
parents: 5611
diff changeset
   125
**)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   126
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   127
Goal "[| F : constrains A A';  G : constrains B B' |] \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   128
\     ==> F Join G : constrains (A Int B) (A' Un B')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   129
by (simp_tac (simpset() addsimps [constrains_Join]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   130
by (blast_tac (claset() addIs [constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   131
qed "constrains_Join_weaken";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   132
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   133
Goal "I ~= {} ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   134
\     (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   135
by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   136
qed "stable_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   137
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   138
Goal "F Join G : stable A = \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   139
\     (F : stable A & G : stable A)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   140
by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   141
qed "stable_Join";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   142
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   143
Goal "I ~= {} ==> FP (JN i:I. F i) = (INT i:I. FP (F i))";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   144
by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   145
qed "FP_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   146
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   147
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   148
(*** Progress: transient, ensures ***)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   149
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   150
Goal "I ~= {} ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   151
\   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   152
by (auto_tac (claset(),
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   153
	      simpset() addsimps [transient_def, JOIN_def]));
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   154
qed "transient_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   155
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   156
Goal "F Join G : transient A = \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   157
\     (F : transient A | G : transient A)";
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   158
by (auto_tac (claset(),
5596
b29d18d8c4d2 abstype of programs
paulson
parents: 5584
diff changeset
   159
	      simpset() addsimps [bex_Un, transient_def,
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   160
				  Join_def]));
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   161
qed "transient_Join";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   162
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   163
Goal "I ~= {} ==> \
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   164
\     (JN i:I. F i) : ensures A B = \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   165
\     ((ALL i:I. F i : constrains (A-B) (A Un B)) & \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   166
\      (EX i:I. F i : ensures A B))";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   167
by (auto_tac (claset(),
5584
aad639e56d4e Now id:(Acts prg) is implicit
paulson
parents: 5426
diff changeset
   168
	      simpset() addsimps [ensures_def, constrains_JN, transient_JN]));
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   169
qed "ensures_JN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   170
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   171
Goalw [ensures_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   172
     "F Join G : ensures A B =     \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   173
\     (F : constrains (A-B) (A Un B) & \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   174
\      G : constrains (A-B) (A Un B) & \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   175
\      (F : ensures A B | G : ensures A B))";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   176
by (auto_tac (claset(),
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   177
	      simpset() addsimps [constrains_Join, transient_Join]));
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   178
qed "ensures_Join";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   179
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   180
Goalw [stable_def, constrains_def, Join_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   181
    "[| F : stable A;  G : constrains A A' |] \
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   182
\    ==> F Join G : constrains A A'";
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   183
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   184
by (Blast_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   185
qed "stable_constrains_Join";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   186
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   187
(*Premise for G cannot use Invariant because  Stable F A  is weaker than
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   188
  G : stable A *)
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   189
Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Invariant A";
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   190
by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, 
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   191
				       Stable_eq_stable, stable_Join]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   192
by (force_tac(claset() addIs [stable_reachable, stable_Int],
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   193
	      simpset() addsimps [Acts_Join]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   194
qed "stable_Join_Invariant";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   195
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   196
Goal "[| F : stable A;  G : ensures A B |] ==> F Join G : ensures A B";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   197
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   198
by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   199
by (etac constrains_weaken 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   200
by Auto_tac;
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   201
qed "ensures_stable_Join1";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   202
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   203
(*As above, but exchanging the roles of F and G*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   204
Goal "[| F : ensures A B;  G : stable A |] ==> F Join G : ensures A B";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   205
by (stac Join_commute 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   206
by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   207
qed "ensures_stable_Join2";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5259
diff changeset
   208
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   209
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   210
(** Diff and localTo **)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   211
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   212
Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   213
by (rtac program_equalityI 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   214
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   215
qed "Join_Diff2";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   216
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   217
Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   218
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   219
qed "Diff_Disjoint";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   220
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   221
Goal "[| F Join G : v localTo F;  Disjoint F G |] \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   222
\     ==> G : (INT z. stable {s. v s = z})";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   223
by (asm_full_simp_tac 
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   224
    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   225
			 Acts_Join, stable_def, constrains_def]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   226
by (Blast_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   227
qed "localTo_imp_stable";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   228
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   229
Goal "[| F Join G : v localTo F;  (s,s') : act;  \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   230
\        act : Acts G;  Disjoint F G |] ==> v s' = v s";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   231
by (asm_full_simp_tac 
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   232
    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   233
			 Acts_Join, stable_def, constrains_def]) 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   234
by (Blast_tac 1);
fe887910e32e specifications as sets of programs
paulson
parents: 5639
diff changeset
   235
qed "localTo_imp_equals";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   236
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   237
Goalw [localTo_def, stable_def, constrains_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   238
     "v localTo F <= (f o v) localTo F";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   239
by (Clarify_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   240
by (auto_tac (claset() addSEs [allE, ballE], simpset()));
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   241
qed "localTo_imp_o_localTo";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   242
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   243
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   244
(*** Higher-level rules involving localTo and Join ***)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   245
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   246
Goal "[| F : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)};   \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   247
\        F Join G : v localTo F;       \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   248
\        F Join G : w localTo F;       \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   249
\        Disjoint F G |]               \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   250
\     ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   251
by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join]));
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   252
by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac));
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   253
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   254
qed "constrains_localTo_constrains2";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   255
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   256
Goalw [stable_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   257
     "[| F : stable {s. P (v s) (w s)};   \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   258
\        F Join G : v localTo F;       \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   259
\        F Join G : w localTo F;       \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   260
\        Disjoint F G |]               \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   261
\     ==> F Join G : stable {s. P (v s) (w s)}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   262
by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   263
qed "stable_localTo_stable2";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   264
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   265
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   266
Goal "(UN k. {s. f s = k}) = UNIV";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   267
by (Blast_tac 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   268
qed "UN_eq_UNIV";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   269
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   270
Goal "[| F : stable {s. v s <= w s};   \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   271
\        F Join G : v localTo F;       \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   272
\        F Join G : Increasing w;      \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   273
\        Disjoint F G |]               \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   274
\     ==> F Join G : Stable {s. v s <= w s}";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   275
by (safe_tac (claset() addSDs [localTo_imp_stable]));
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   276
by (rewrite_goals_tac [stable_def, Stable_def, Increasing_def]);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   277
by (subgoal_tac "ALL k: UNIV. ?H : Constrains ({s. v s = k} Int ?AA) ?AA" 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   278
by (dtac ball_Constrains_UN 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   279
by (full_simp_tac (simpset() addsimps [UN_eq_UNIV]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   280
by (rtac ballI 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   281
by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   282
\                                      ({s. v s = k} Un {s. v s <= w s})" 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   283
by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   284
by (blast_tac (claset() addIs [constrains_weaken]) 2);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   285
by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   286
by (etac Constrains_weaken 2);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   287
by Auto_tac;
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5785
diff changeset
   288
qed "Increasing_localTo_Stable";