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