src/HOL/UNITY/Constrains.ML
author paulson
Mon, 20 Sep 1999 10:42:09 +0200
changeset 7541 1a7a38d8f5bd
parent 7403 c318acb88251
child 7689 affe0c2fdfbf
permissions -rw-r--r--
new theorem Always_INT_distrib; therefore renamed Always_Int to Always_Int_I
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Constrains
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     2
    ID:         $Id$
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     5
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     6
Safety relations: restricted to the set of reachable states.
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     7
*)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     8
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
     9
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    10
(*** traces and reachable ***)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    11
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    12
Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    13
by Safe_tac;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    14
by (etac traces.induct 2);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    15
by (etac reachable.induct 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    16
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    17
qed "reachable_equiv_traces";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    18
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    19
Goal "Init F <= reachable F";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    20
by (blast_tac (claset() addIs reachable.intrs) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    21
qed "Init_subset_reachable";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    22
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    23
Goal "Acts G <= Acts F ==> G : stable (reachable F)";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    24
by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    25
qed "stable_reachable";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    26
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    27
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    28
(*The set of all reachable states is an invariant...*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    29
Goal "F : invariant (reachable F)";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    30
by (simp_tac (simpset() addsimps [invariant_def]) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    31
by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    32
qed "invariant_reachable";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    33
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    34
(*...in fact the strongest invariant!*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    35
Goal "F : invariant A ==> reachable F <= A";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    36
by (full_simp_tac 
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    37
    (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    38
by (rtac subsetI 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    39
by (etac reachable.induct 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    40
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    41
qed "invariant_includes_reachable";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    42
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    43
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    44
(*** Co ***)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    45
7403
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
    46
(*Needed because its operands are sets*)
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
    47
overload_1st_set "Constrains.Constrains";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5319
diff changeset
    48
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    49
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    50
bind_thm ("constrains_reachable_Int",
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    51
	  subset_refl RS
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    52
	  rewrite_rule [stable_def] stable_reachable RS 
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    53
	  constrains_Int);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    54
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    55
(*Resembles the previous definition of Constrains*)
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    56
Goalw [Constrains_def]
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    57
     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}";
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    58
by (blast_tac (claset() addDs [constrains_reachable_Int]
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    59
			addIs [constrains_weaken]) 1);
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    60
qed "Constrains_eq_constrains";
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    61
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    62
Goalw [Constrains_def] "F : A co A' ==> F : A Co A'";
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
    63
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    64
qed "constrains_imp_Constrains";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    65
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
    66
Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A";
5631
707f30bc7fe7 new theorems
paulson
parents: 5620
diff changeset
    67
by (etac constrains_imp_Constrains 1);
707f30bc7fe7 new theorems
paulson
parents: 5620
diff changeset
    68
qed "stable_imp_Stable";
707f30bc7fe7 new theorems
paulson
parents: 5620
diff changeset
    69
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    70
val prems = Goal
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5584
diff changeset
    71
    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    72
\    ==> F : A Co A'";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    73
by (rtac constrains_imp_Constrains 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    74
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    75
qed "ConstrainsI";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    76
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    77
Goalw [Constrains_def, constrains_def] "F : {} Co B";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    78
by (Blast_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    79
qed "Constrains_empty";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    80
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    81
Goal "F : A Co UNIV";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    82
by (blast_tac (claset() addIs [ConstrainsI]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    83
qed "Constrains_UNIV";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    84
AddIffs [Constrains_empty, Constrains_UNIV];
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    85
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    86
Goalw [Constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    87
    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    88
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    89
qed "Constrains_weaken_R";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    90
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    91
Goalw [Constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    92
    "[| F : A Co A'; B<=A |] ==> F : B Co A'";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    93
by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    94
qed "Constrains_weaken_L";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    95
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    96
Goalw [Constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
    97
   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    98
by (blast_tac (claset() addIs [constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
    99
qed "Constrains_weaken";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   100
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   101
(** Union **)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   102
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   103
Goalw [Constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   104
    "[| F : A Co A'; F : B Co B' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   105
\    ==> F : (A Un B) Co (A' Un B')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   106
by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   107
qed "Constrains_Un";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   108
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   109
Goal "ALL i:I. F : (A i) Co (A' i) \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   110
\     ==> F : (UN i:I. A i) Co (UN i:I. A' i)";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   111
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   112
by (dtac ball_constrains_UN 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   113
by (blast_tac (claset() addIs [constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   114
qed "ball_Constrains_UN";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   115
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   116
(** Intersection **)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   117
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   118
Goalw [Constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   119
    "[| F : A Co A'; F : B Co B' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   120
\    ==> F : (A Int B) Co (A' Int B')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   121
by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   122
qed "Constrains_Int";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   123
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   124
Goal "ALL i:I. F : (A i) Co (A' i)   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   125
\     ==> F : (INT i:I. A i) Co (INT i:I. A' i)";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   126
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   127
by (dtac ball_constrains_INT 1);
5340
d75c03cf77b5 Misc changes
paulson
parents: 5319
diff changeset
   128
by (dtac constrains_reachable_Int 1);
d75c03cf77b5 Misc changes
paulson
parents: 5319
diff changeset
   129
by (blast_tac (claset() addIs [constrains_weaken]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   130
qed "ball_Constrains_INT";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   131
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   132
Goal "F : A Co A' ==> reachable F Int A <= A'";
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   133
by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset, 
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   134
					   Constrains_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   135
qed "Constrains_imp_subset";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   136
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   137
Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   138
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   139
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   140
qed "Constrains_trans";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   141
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   142
Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   143
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains, 
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   144
				       constrains_def]) 1);
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   145
by (Blast_tac 1);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
   146
qed "Constrains_cancel";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
   147
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   148
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   149
(*** Stable ***)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   150
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   151
Goal "(F : Stable A) = (F : stable (reachable F Int A))";
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   152
by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, 
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   153
				  stable_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   154
qed "Stable_eq_stable";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   155
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   156
Goalw [Stable_def] "F : A Co A ==> F : Stable A";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   157
by (assume_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   158
qed "StableI";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   159
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   160
Goalw [Stable_def] "F : Stable A ==> F : A Co A";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   161
by (assume_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   162
qed "StableD";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   163
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   164
Goalw [Stable_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   165
    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   166
by (blast_tac (claset() addIs [Constrains_Un]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   167
qed "Stable_Un";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   168
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   169
Goalw [Stable_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   170
    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   171
by (blast_tac (claset() addIs [Constrains_Int]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   172
qed "Stable_Int";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   173
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   174
Goalw [Stable_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   175
    "[| F : Stable C; F : A Co (C Un A') |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   176
\    ==> F : (C Un A) Co (C Un A')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   177
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   178
qed "Stable_Constrains_Un";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   179
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   180
Goalw [Stable_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   181
    "[| F : Stable C; F : (C Int A) Co A' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   182
\    ==> F : (C Int A) Co (C Int A')";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   183
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   184
qed "Stable_Constrains_Int";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   185
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   186
Goalw [Stable_def]
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   187
    "(ALL i:I. F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   188
by (etac ball_Constrains_UN 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   189
qed "ball_Stable_UN";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   190
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   191
Goalw [Stable_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   192
    "(ALL i:I. F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   193
by (etac ball_Constrains_INT 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   194
qed "ball_Stable_INT";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   195
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   196
Goal "F : Stable (reachable F)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   197
by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   198
qed "Stable_reachable";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   199
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   200
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   201
5784
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   202
(*** Increasing ***)
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   203
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   204
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
6704
5febcf428342 generalized Increasing_size to mono_Increasing_o
paulson
parents: 6672
diff changeset
   205
     "mono g ==> Increasing f <= Increasing (g o f)";
5784
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   206
by Auto_tac;
6704
5febcf428342 generalized Increasing_size to mono_Increasing_o
paulson
parents: 6672
diff changeset
   207
by (blast_tac (claset() addIs [monoD, order_trans]) 1);
5febcf428342 generalized Increasing_size to mono_Increasing_o
paulson
parents: 6672
diff changeset
   208
qed "mono_Increasing_o";
5784
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   209
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   210
Goalw [Increasing_def]
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   211
     "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}";
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   212
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   213
by (Blast_tac 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   214
qed "Increasing_Stable_less";
5784
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   215
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   216
Goalw [increasing_def, Increasing_def]
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   217
     "F : increasing f ==> F : Increasing f";
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   218
by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   219
qed "increasing_imp_Increasing";
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   220
54276fba8420 the Increasing operator
paulson
parents: 5669
diff changeset
   221
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   222
(*** The Elimination Theorem.  The "free" m has become universally quantified!
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   223
     Should the premise be !!m instead of ALL m ?  Would make it harder to use
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   224
     in forward proof. ***)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   225
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   226
Goalw [Constrains_def, constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   227
    "[| ALL m. F : {s. s x = m} Co (B m) |] \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   228
\    ==> F : {s. s x : M} Co (UN m:M. B m)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   229
by (Blast_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   230
qed "Elimination";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   231
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   232
(*As above, but for the trivial case of a one-variable state, in which the
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   233
  state is identified with its one variable.*)
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   234
Goalw [Constrains_def, constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   235
    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   236
by (Blast_tac 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   237
qed "Elimination_sing";
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   238
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   239
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   240
(*** Specialized laws for handling Always ***)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   241
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   242
(** Natural deduction rules for "Always A" **)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   243
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   244
Goal "[| Init F<=A;  F : Stable A |] ==> F : Always A";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   245
by (asm_simp_tac (simpset() addsimps [Always_def]) 1);
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   246
qed "AlwaysI";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   247
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   248
Goal "F : Always A ==> Init F<=A & F : Stable A";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   249
by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   250
qed "AlwaysD";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   251
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   252
bind_thm ("AlwaysE", AlwaysD RS conjE);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   253
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   254
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   255
(*The set of all reachable states is Always*)
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   256
Goal "F : Always A ==> reachable F <= A";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   257
by (full_simp_tac 
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   258
    (simpset() addsimps [Stable_def, Constrains_def, constrains_def, 
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   259
			 Always_def]) 1);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   260
by (rtac subsetI 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   261
by (etac reachable.induct 1);
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   262
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   263
qed "Always_includes_reachable";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   264
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   265
Goalw [Always_def, invariant_def, Stable_def, stable_def]
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   266
     "F : invariant A ==> F : Always A";
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   267
by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   268
qed "invariant_imp_Always";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   269
6672
8542c6dda828 new theorem Always_reachable
paulson
parents: 6575
diff changeset
   270
bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
8542c6dda828 new theorem Always_reachable
paulson
parents: 6575
diff changeset
   271
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   272
Goal "Always A = {F. F : invariant (reachable F Int A)}";
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   273
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   274
				  Constrains_eq_constrains, stable_def]) 1);
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   275
by (blast_tac (claset() addIs reachable.intrs) 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   276
qed "Always_eq_invariant_reachable";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   277
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   278
(*the RHS is the traditional definition of the "always" operator*)
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   279
Goal "Always A = {F. reachable F <= A}";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   280
by (auto_tac (claset() addDs [invariant_includes_reachable],
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   281
	      simpset() addsimps [Int_absorb2, invariant_reachable,
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   282
				  Always_eq_invariant_reachable]));
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   283
qed "Always_eq_includes_reachable";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   284
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   285
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   286
Goal "Always A = (UN I: Pow A. invariant I)";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   287
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   288
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   289
                               stable_reachable,
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   290
			       impOfSubs invariant_includes_reachable]) 1);
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   291
qed "Always_eq_UN_invariant";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   292
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   293
Goal "[| F : Always A; A <= B |] ==> F : Always B";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   294
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   295
qed "Always_weaken";
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   296
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   297
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   298
(*** "Co" rules involving Always ***)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   299
6739
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   300
Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')";
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   301
by (asm_simp_tac
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   302
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5784
diff changeset
   303
			 Constrains_def, Int_assoc RS sym]) 1);
6739
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   304
qed "Always_Constrains_pre";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   305
6739
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   306
Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')";
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   307
by (asm_simp_tac
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   308
    (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
6575
70d758762c50 new definitions of Co and LeadsTo
paulson
parents: 6570
diff changeset
   309
			 Constrains_eq_constrains, Int_assoc RS sym]) 1);
6739
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   310
qed "Always_Constrains_post";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   311
6739
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   312
(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   313
bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   314
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   315
(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
66e4118eead9 replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
paulson
parents: 6704
diff changeset
   316
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   317
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   318
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   319
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   320
(** Conjoining Always properties **)
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   321
7541
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   322
Goal "Always (A Int B) = Always A Int Always B";
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   323
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   324
qed "Always_Int_distrib";
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   325
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   326
Goal "Always (INTER I A) = (INT i:I. Always (A i))";
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   327
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   328
qed "Always_INT_distrib";
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   329
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   330
Goal "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)";
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   331
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
7541
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   332
qed "Always_Int_I";
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   333
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   334
(*Delete the nearest invariance assumption (which will be the second one
7541
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   335
  used by Always_Int_I) *)
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   336
val Always_thin =
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   337
    read_instantiate_sg (sign_of thy)
6570
a7d7985050a9 Invariant -> Always and other tidying
paulson
parents: 6536
diff changeset
   338
                [("V", "?F : Always ?A")] thin_rl;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   339
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   340
(*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
7541
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   341
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   342
5319
7356d0c88b1b Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
paulson
parents: 5313
diff changeset
   343
(*Combines a list of invariance THEOREMS into one.*)
7541
1a7a38d8f5bd new theorem Always_INT_distrib; therefore renamed Always_Int
paulson
parents: 7403
diff changeset
   344
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   345
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff changeset
   346
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   347
(*To allow expansion of the program's definition when appropriate*)
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   348
val program_defs_ref = ref ([] : thm list);
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   349
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   350
(*proves "co" properties when the program is specified*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   351
fun constrains_tac i = 
5422
578dc167453f Moved constrains_tac from SubstAx to Constrains.
paulson
parents: 5340
diff changeset
   352
   SELECT_GOAL
7403
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   353
      (EVERY [REPEAT (Always_Int_tac 1),
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   354
	      REPEAT (etac Always_ConstrainsI 1
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   355
		      ORELSE
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   356
		      resolve_tac [StableI, stableI,
5422
578dc167453f Moved constrains_tac from SubstAx to Constrains.
paulson
parents: 5340
diff changeset
   357
				   constrains_imp_Constrains] 1),
578dc167453f Moved constrains_tac from SubstAx to Constrains.
paulson
parents: 5340
diff changeset
   358
	      rtac constrainsI 1,
7403
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   359
	      full_simp_tac (simpset() addsimps !program_defs_ref) 1,
5620
3ac11c4af76a tidying and renaming
paulson
parents: 5584
diff changeset
   360
	      REPEAT (FIRSTGOAL (etac disjE)),
5422
578dc167453f Moved constrains_tac from SubstAx to Constrains.
paulson
parents: 5340
diff changeset
   361
	      ALLGOALS Clarify_tac,
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5631
diff changeset
   362
	      ALLGOALS Asm_full_simp_tac]) i;
7403
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   363
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   364
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   365
(*For proving invariants*)
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   366
fun always_tac i = 
c318acb88251 tidied some proofs
paulson
parents: 6741
diff changeset
   367
    rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;