src/HOL/UNITY/UNITY.ML
author paulson
Mon, 24 May 1999 15:50:23 +0200
changeset 6712 d1bebb7f1c50
parent 6536 281d44905cab
child 7240 a509730e424b
permissions -rw-r--r--
generalized increasing_size to mono_increasing_o
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/UNITY
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
The basic UNITY theory (revised version, based upon the "co" operator)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming", 1994
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
set proof_timing;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
HOL_quantifiers := false;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    15
(*** General lemmas ***)
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    16
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    17
Goal "UNIV Times UNIV = UNIV";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    18
by Auto_tac;
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    19
qed "UNIV_Times_UNIV"; 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    20
Addsimps [UNIV_Times_UNIV];
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    21
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    22
Goal "- (UNIV Times A) = UNIV Times (-A)";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    23
by Auto_tac;
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    24
qed "Compl_Times_UNIV1"; 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    25
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    26
Goal "- (A Times UNIV) = (-A) Times UNIV";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    27
by Auto_tac;
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    28
qed "Compl_Times_UNIV2"; 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    29
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    30
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; 
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    31
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
    32
6535
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    33
(*** The abstract type of programs ***)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    34
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    35
val rep_ss = simpset() addsimps 
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    36
                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    37
		 Rep_Program_inverse, Abs_Program_inverse];
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    38
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    39
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    40
Goal "Id : Acts F";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    41
by (cut_inst_tac [("x", "F")] Rep_Program 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    42
by (auto_tac (claset(), rep_ss));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    43
qed "Id_in_Acts";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    44
AddIffs [Id_in_Acts];
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    45
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    46
Goal "insert Id (Acts F) = Acts F";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    47
by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    48
qed "insert_Id_Acts";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    49
AddIffs [insert_Id_Acts];
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    50
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    51
(** Inspectors for type "program" **)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    52
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    53
Goal "Init (mk_program (init,acts)) = init";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    54
by (auto_tac (claset(), rep_ss));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    55
qed "Init_eq";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    56
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    57
Goal "Acts (mk_program (init,acts)) = insert Id acts";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    58
by (auto_tac (claset(), rep_ss));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    59
qed "Acts_eq";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    60
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    61
Addsimps [Acts_eq, Init_eq];
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    62
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    63
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    64
(** The notation of equality for type "program" **)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    65
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    66
Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    67
by (subgoals_tac ["EX x. Rep_Program F = x",
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    68
		  "EX x. Rep_Program G = x"] 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    69
by (REPEAT (Blast_tac 2));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    70
by (Clarify_tac 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    71
by (auto_tac (claset(), rep_ss));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    72
by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    73
by (asm_full_simp_tac rep_ss 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    74
qed "program_equalityI";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    75
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    76
val [major,minor] =
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    77
Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    78
by (rtac minor 1);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    79
by (auto_tac (claset(), simpset() addsimps [major]));
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    80
qed "program_equalityE";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    81
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    82
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    83
(*** These rules allow "lazy" definition expansion 
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    84
     They avoid expanding the full program, which is a large expression
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    85
***)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    86
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    87
Goal "F == mk_program (init,acts) ==> Init F = init";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    88
by Auto_tac;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    89
qed "def_prg_Init";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    90
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    91
(*The program is not expanded, but its Init and Acts are*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    92
val [rew] = goal thy
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    93
    "[| F == mk_program (init,acts) |] \
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    94
\    ==> Init F = init & Acts F = insert Id acts";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    95
by (rewtac rew);
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    96
by Auto_tac;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    97
qed "def_prg_simps";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    98
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
    99
(*An action is expanded only if a pair of states is being tested against it*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   100
Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   101
by Auto_tac;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   102
qed "def_act_simp";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   103
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   104
fun simp_of_act def = def RS def_act_simp;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   105
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   106
(*A set is expanded only if an element is being tested against it*)
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   107
Goal "A == B ==> (x : A) = (x : B)";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   108
by Auto_tac;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   109
qed "def_set_simp";
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   110
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   111
fun simp_of_set def = def RS def_set_simp;
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   112
880f31a62784 eliminated theory UNITY/Traces
paulson
parents: 6295
diff changeset
   113
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   114
(*** co ***)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   115
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   116
overload_1st_set "UNITY.op co";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   117
overload_1st_set "UNITY.stable";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   118
overload_1st_set "UNITY.unless";
5340
d75c03cf77b5 Misc changes
paulson
parents: 5313
diff changeset
   119
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   120
val prems = Goalw [constrains_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   121
    "(!!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
   122
\    ==> F : A co A'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   123
by (blast_tac (claset() addIs prems) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   124
qed "constrainsI";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   125
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   126
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   127
    "[| F : A co A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   128
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   129
qed "constrainsD";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   130
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   131
Goalw [constrains_def] "F : {} co B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   132
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   133
qed "constrains_empty";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   134
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   135
Goalw [constrains_def] "F : A co UNIV";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   136
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   137
qed "constrains_UNIV";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   138
AddIffs [constrains_empty, constrains_UNIV];
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   139
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   140
(*monotonic in 2nd argument*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   141
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   142
    "[| F : A co A'; A'<=B' |] ==> F : A co B'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   143
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   144
qed "constrains_weaken_R";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   145
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   146
(*anti-monotonic in 1st argument*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   147
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   148
    "[| F : A co A'; B<=A |] ==> F : B co A'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   149
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   150
qed "constrains_weaken_L";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   151
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   152
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   153
   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   154
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   155
qed "constrains_weaken";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   156
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   157
(** Union **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   158
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   159
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   160
    "[| F : A co A'; F : B co B' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   161
\    ==> F : (A Un B) co (A' Un B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   162
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   163
qed "constrains_Un";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   164
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   165
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   166
    "ALL i:I. F : (A i) co (A' i) \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   167
\    ==> F : (UN i:I. A i) co (UN i:I. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   168
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   169
qed "ball_constrains_UN";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   170
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   171
(** Intersection **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   172
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   173
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   174
    "[| F : A co A'; F : B co B' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   175
\    ==> F : (A Int B) co (A' Int B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   176
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   177
qed "constrains_Int";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   178
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   179
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   180
    "ALL i:I. F : (A i) co (A' i) \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   181
\    ==> F : (INT i:I. A i) co (INT i:I. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   182
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   183
qed "ball_constrains_INT";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   184
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   185
Goalw [constrains_def] "F : A co A' ==> A <= A'";
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   186
by Auto_tac;
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   187
qed "constrains_imp_subset";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   188
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   189
(*The reasoning is by subsets since "co" refers to single actions
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
   190
  only.  So this rule isn't that useful.*)
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   191
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   192
    "[| F : A co B; F : B co C |] ==> F : A co C";
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   193
by (Blast_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   194
qed "constrains_trans";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   195
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   196
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   197
   "[| F : A co (A' Un B); F : B co B' |] \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   198
\   ==> F : A co (A' Un B')";
6295
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   199
by (Clarify_tac 1);
351b3c2b0d83 removed the infernal States, eqStates, compatible, etc.
paulson
parents: 6012
diff changeset
   200
by (Blast_tac 1);
6012
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
   201
qed "constrains_cancel";
1894bfc4aee9 Addition of the States component; parts of Comp not working
paulson
parents: 5804
diff changeset
   202
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   203
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   204
(*** stable ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   205
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   206
Goalw [stable_def] "F : A co A ==> F : stable A";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   207
by (assume_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   208
qed "stableI";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   209
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   210
Goalw [stable_def] "F : stable A ==> F : A co A";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   211
by (assume_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   212
qed "stableD";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   213
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   214
(** Union **)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   215
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   216
Goalw [stable_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   217
    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   218
by (blast_tac (claset() addIs [constrains_Un]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   219
qed "stable_Un";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   220
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   221
Goalw [stable_def]
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   222
    "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: 5669
diff changeset
   223
by (blast_tac (claset() addIs [ball_constrains_UN]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   224
qed "ball_stable_UN";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   225
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   226
(** Intersection **)
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   227
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   228
Goalw [stable_def]
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   229
    "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   230
by (blast_tac (claset() addIs [constrains_Int]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   231
qed "stable_Int";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   232
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   233
Goalw [stable_def]
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   234
    "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   235
by (blast_tac (claset() addIs [ball_constrains_INT]) 1);
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   236
qed "ball_stable_INT";
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   237
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   238
Goalw [stable_def, constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   239
    "[| F : stable C; F : A co (C Un A') |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   240
\    ==> F : (C Un A) co (C Un A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   241
by (Blast_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   242
qed "stable_constrains_Un";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   243
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   244
Goalw [stable_def, constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   245
    "[| F : stable C; F :  (C Int A) co  A' |]   \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   246
\    ==> F : (C Int A) co (C Int A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   247
by (Blast_tac 1);
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
   248
qed "stable_constrains_Int";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   249
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   250
(*[| F : stable C; F :  co (C Int A) A |] ==> F : stable (C Int A)*)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   251
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   252
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   253
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   254
(*** invariant ***)
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   255
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   256
Goal "[| Init F<=A;  F: stable A |] ==> F : invariant A";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   257
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   258
qed "invariantI";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   259
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   260
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   261
Goal "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   262
by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   263
qed "invariant_Int";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   264
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   265
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   266
(*** increasing ***)
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   267
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   268
Goalw [increasing_def, stable_def, constrains_def]
6712
d1bebb7f1c50 generalized increasing_size to mono_increasing_o
paulson
parents: 6536
diff changeset
   269
     "mono g ==> increasing f <= increasing (g o f)";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   270
by Auto_tac;
6712
d1bebb7f1c50 generalized increasing_size to mono_increasing_o
paulson
parents: 6536
diff changeset
   271
by (blast_tac (claset() addIs [monoD, order_trans]) 1);
d1bebb7f1c50 generalized increasing_size to mono_increasing_o
paulson
parents: 6536
diff changeset
   272
qed "mono_increasing_o";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   273
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   274
Goalw [increasing_def]
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   275
     "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}";
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   276
by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   277
by (Blast_tac 1);
5804
8e0a4c4fd67b Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents: 5669
diff changeset
   278
qed "increasing_stable_less";
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   279
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   280
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   281
(** The Elimination Theorem.  The "free" m has become universally quantified!
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   282
    Should the premise be !!m instead of ALL m ?  Would make it harder to use
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   283
    in forward proof. **)
fe887910e32e specifications as sets of programs
paulson
parents: 5608
diff changeset
   284
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   285
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   286
    "[| ALL m:M. F : {s. s x = m} co (B m) |] \
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   287
\    ==> F : {s. s x : M} co (UN m:M. B m)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   288
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   289
qed "elimination";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   290
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   291
(*As above, but for the trivial case of a one-variable state, in which the
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   292
  state is identified with its one variable.*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   293
Goalw [constrains_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   294
    "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   295
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   296
qed "elimination_sing";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   297
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   298
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   299
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   300
(*** Theoretical Results from Section 6 ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   301
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   302
Goalw [constrains_def, strongest_rhs_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   303
    "F : A co (strongest_rhs F A )";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   304
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   305
qed "constrains_strongest_rhs";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   306
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   307
Goalw [constrains_def, strongest_rhs_def]
6536
281d44905cab made many specification operators infix
paulson
parents: 6535
diff changeset
   308
    "F : A co B ==> strongest_rhs F A <= B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   309
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   310
qed "strongest_rhs_is_strongest";