src/HOL/UNITY/WFair.ML
author paulson
Wed, 05 Aug 1998 18:20:25 +0200
changeset 5257 c03e3ba9cbcc
parent 5253 82a5ca6290aa
child 5277 e4297d03e5d2
permissions -rw-r--r--
Indentation, comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/WFair
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
Weak Fairness versions of transient, ensures, leadsTo.
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
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
(*** transient ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    14
Goalw [stable_def, constrains_def, transient_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    15
    "[| stable acts A; transient acts A |] ==> A = {}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
qed "stable_transient_empty";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    18
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    19
Goalw [transient_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    20
    "[| transient acts A; B<=A |] ==> transient acts B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
by (rtac bexI 1 THEN assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    24
qed "transient_strengthen";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    26
Goalw [transient_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    27
    "[| act:acts;  A <= Domain act;  act^^A <= Compl A |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    28
\         ==> transient acts A";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    29
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    30
qed "transient_mem";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    33
(*** ensures ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    35
Goalw [ensures_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    36
    "[| constrains acts (A-B) (A Un B); transient acts (A-B) |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    37
\    ==> ensures acts A B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    39
qed "ensuresI";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    40
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    41
Goalw [ensures_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    42
    "ensures acts A B  \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    43
\    ==> constrains acts (A-B) (A Un B) & transient acts (A-B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
qed "ensuresD";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    46
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    47
(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    48
Goalw [ensures_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    49
    "[| ensures acts A A'; A'<=B' |] ==> ensures acts A B'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    50
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
qed "ensures_weaken_R";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    53
Goalw [ensures_def, constrains_def, transient_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    54
    "acts ~= {} ==> ensures acts A UNIV";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    55
by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    56
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    57
qed "ensures_UNIV";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    58
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
    59
Goalw [ensures_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    60
    "[| stable acts C; \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    61
\       constrains acts (C Int (A - A')) (A Un A'); \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    62
\       transient  acts (C Int (A-A')) |]   \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    63
\   ==> ensures acts (C Int A) (C Int A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    64
by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    65
				      Diff_Int_distrib RS sym,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    66
				      stable_constrains_Int]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    67
qed "stable_ensures_Int";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    68
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    69
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    70
(*** leadsTo ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    71
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    72
(*Synonyms for the theorems produced by the inductive defn package*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    73
bind_thm ("leadsTo_Basis", leadsto.Basis);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    74
bind_thm ("leadsTo_Trans", leadsto.Trans);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    75
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    76
Goal "act: acts ==> leadsTo acts A UNIV";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    77
by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    78
qed "leadsTo_UNIV";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    79
Addsimps [leadsTo_UNIV];
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    80
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    81
(*Useful with cancellation, disjunction*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    82
Goal "leadsTo acts A (A' Un A') ==> leadsTo acts A A'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    83
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    84
qed "leadsTo_Un_duplicate";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    85
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    86
Goal "leadsTo acts A (A' Un C Un C) ==> leadsTo acts A (A' Un C)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    87
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    88
qed "leadsTo_Un_duplicate2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    89
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    90
(*The Union introduction rule as we should have liked to state it*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    91
val prems = goal thy
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    92
    "(!!A. A : S ==> leadsTo acts A B) ==> leadsTo acts (Union S) B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    93
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    94
qed "leadsTo_Union";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    95
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    96
val prems = goal thy
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
    97
    "(!!i. i : I ==> leadsTo acts (A i) B) ==> leadsTo acts (UN i:I. A i) B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    98
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    99
by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   100
qed "leadsTo_UN";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   101
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   102
(*Binary union introduction rule*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   103
Goal "[| leadsTo acts A C; leadsTo acts B C |] ==> leadsTo acts (A Un B) C";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   104
by (stac Un_eq_Union 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   105
by (blast_tac (claset() addIs [leadsTo_Union]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   106
qed "leadsTo_Un";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   107
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   108
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   109
(*The INDUCTION rule as we should have liked to state it*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   110
val major::prems = goal thy
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   111
  "[| leadsTo acts za zb;  \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   112
\     !!A B. ensures acts A B ==> P A B; \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   113
\     !!A B C. [| leadsTo acts A B; P A B; leadsTo acts B C; P B C |] \
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   114
\              ==> P A C; \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   115
\     !!B S. ALL A:S. leadsTo acts A B & P A B ==> P (Union S) B \
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   116
\  |] ==> P za zb";
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 5111
diff changeset
   117
by (rtac (major RS leadsto.induct) 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   118
by (REPEAT (blast_tac (claset() addIs prems) 1));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   119
qed "leadsTo_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   120
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   121
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   122
Goal "[| A<=B;  id: acts |] ==> leadsTo acts A B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   123
by (rtac leadsTo_Basis 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   124
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   125
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   126
qed "subset_imp_leadsTo";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   127
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   128
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   129
Addsimps [empty_leadsTo];
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   130
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   131
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   132
(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   133
  needs the extra premise id:acts*)
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   134
Goal "leadsTo acts A A' ==> A'<=B' --> leadsTo acts A B'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   135
by (etac leadsTo_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   136
by (Clarify_tac 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   137
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   138
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   139
by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   140
qed_spec_mp "leadsTo_weaken_R";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   141
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   142
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   143
Goal "[| leadsTo acts A A'; B<=A; id: acts |] ==>  \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   144
\         leadsTo acts B A'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   145
by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   146
			       subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   147
qed_spec_mp "leadsTo_weaken_L";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   148
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   149
(*Distributes over binary unions*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   150
Goal "id: acts ==> \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   151
\       leadsTo acts (A Un B) C  =  (leadsTo acts A C & leadsTo acts B C)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   152
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   153
qed "leadsTo_Un_distrib";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   154
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   155
Goal "id: acts ==> \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   156
\       leadsTo acts (UN i:I. A i) B  =  (ALL i : I. leadsTo acts (A i) B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   157
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   158
qed "leadsTo_UN_distrib";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   159
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   160
Goal "id: acts ==> \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   161
\       leadsTo acts (Union S) B  =  (ALL A : S. leadsTo acts A B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   162
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   163
qed "leadsTo_Union_distrib";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   164
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   165
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   166
Goal "[| leadsTo acts A A'; id: acts; B<=A; A'<=B' |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   167
\   ==> leadsTo acts B B'";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   168
(*PROOF FAILED: why?*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   169
by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   170
			       leadsTo_weaken_L]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   171
qed "leadsTo_weaken";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   172
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   173
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   174
(*Set difference: maybe combine with leadsTo_weaken_L??*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   175
Goal "[| leadsTo acts (A-B) C; leadsTo acts B C; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   176
\       ==> leadsTo acts A C";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   177
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   178
qed "leadsTo_Diff";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   179
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   180
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   181
(** Meta or object quantifier ???
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   182
    see ball_constrains_UN in UNITY.ML***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   183
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   184
val prems = goal thy
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   185
   "(!! i. i:I ==> leadsTo acts (A i) (A' i)) \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   186
\   ==> leadsTo acts (UN i:I. A i) (UN i:I. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   187
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   188
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   189
                        addIs prems) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   190
qed "leadsTo_UN_UN";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   191
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   192
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   193
(*Version with no index set*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   194
val prems = goal thy
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   195
   "(!! i. leadsTo acts (A i) (A' i)) \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   196
\   ==> leadsTo acts (UN i. A i) (UN i. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   197
by (blast_tac (claset() addIs [leadsTo_UN_UN] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   198
                        addIs prems) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   199
qed "leadsTo_UN_UN_noindex";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   200
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   201
(*Version with no index set*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   202
Goal "ALL i. leadsTo acts (A i) (A' i) \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   203
\   ==> leadsTo acts (UN i. A i) (UN i. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   204
by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   205
qed "all_leadsTo_UN_UN";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   206
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   207
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   208
(*Binary union version*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   209
Goal "[| leadsTo acts A A'; leadsTo acts B B' |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   210
\         ==> leadsTo acts (A Un B) (A' Un B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   211
by (blast_tac (claset() addIs [leadsTo_Un, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   212
			       leadsTo_weaken_R]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   213
qed "leadsTo_Un_Un";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   214
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   215
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   216
(** The cancellation law **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   217
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   218
Goal "[| leadsTo acts A (A' Un B); leadsTo acts B B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   219
\   ==> leadsTo acts A (A' Un B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   220
by (blast_tac (claset() addIs [leadsTo_Un_Un, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   221
			       subset_imp_leadsTo, leadsTo_Trans]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   222
qed "leadsTo_cancel2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   223
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   224
Goal "[| leadsTo acts A (A' Un B); leadsTo acts (B-A') B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   225
\   ==> leadsTo acts A (A' Un B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   226
by (rtac leadsTo_cancel2 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   227
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   228
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   229
qed "leadsTo_cancel_Diff2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   230
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   231
Goal "[| leadsTo acts A (B Un A'); leadsTo acts B B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   232
\   ==> leadsTo acts A (B' Un A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   233
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   234
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   235
qed "leadsTo_cancel1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   236
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   237
Goal "[| leadsTo acts A (B Un A'); leadsTo acts (B-A') B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   238
\   ==> leadsTo acts A (B' Un A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   239
by (rtac leadsTo_cancel1 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   240
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   241
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   242
qed "leadsTo_cancel_Diff1";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   243
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   244
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   245
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   246
(** The impossibility law **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   247
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   248
Goal "leadsTo acts A B ==> B={} --> A={}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   249
by (etac leadsTo_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   250
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   251
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   252
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   253
val lemma = result() RS mp;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   254
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   255
Goal "leadsTo acts A {} ==> A={}";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   256
by (blast_tac (claset() addSIs [lemma]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   257
qed "leadsTo_empty";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   258
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   259
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   260
(** PSP: Progress-Safety-Progress **)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   261
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   262
(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:acts. *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   263
Goalw [stable_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   264
   "[| leadsTo acts A A'; stable acts B |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   265
\   ==> leadsTo acts (A Int B) (A' Int B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   266
by (etac leadsTo_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   267
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   268
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   269
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   270
by (rtac leadsTo_Basis 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   271
by (asm_full_simp_tac
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   272
    (simpset() addsimps [ensures_def, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   273
			 Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   274
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   275
qed "PSP_stable";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   276
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   277
Goal "[| leadsTo acts A A'; stable acts B |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   278
\   ==> leadsTo acts (B Int A) (B Int A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   279
by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   280
qed "PSP_stable2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   281
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   282
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   283
Goalw [ensures_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   284
   "[| ensures acts A A'; constrains acts B B' |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   285
\   ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   286
by Safe_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   287
by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   288
by (etac transient_strengthen 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   289
by (Blast_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   290
qed "PSP_ensures";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   291
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   292
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   293
Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   294
\           ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   295
by (etac leadsTo_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   296
by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   297
by (blast_tac (claset() addIs [leadsTo_Union]) 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   298
(*Transitivity case has a delicate argument involving "cancellation"*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   299
by (rtac leadsTo_Un_duplicate2 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   300
by (etac leadsTo_cancel_Diff1 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   301
by (assume_tac 3);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   302
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   303
(*Basis case*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   304
by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   305
qed "PSP";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   306
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   307
Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   308
\   ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   309
by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   310
qed "PSP2";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   311
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   312
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   313
Goalw [unless_def]
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   314
   "[| leadsTo acts A A'; unless acts B B'; id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   315
\   ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   316
by (dtac PSP 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   317
by (assume_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   318
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   319
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   320
by (etac leadsTo_Diff 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   321
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   322
by Auto_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   323
qed "PSP_unless";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   324
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   325
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   326
(*** Proving the induction rules ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   327
5257
c03e3ba9cbcc Indentation, comments
paulson
parents: 5253
diff changeset
   328
(** The most general rule: r is any wf relation; f is any variant function **)
c03e3ba9cbcc Indentation, comments
paulson
parents: 5253
diff changeset
   329
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   330
Goal "[| wf r;     \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   331
\        ALL m. leadsTo acts (A Int f-``{m})                     \
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   332
\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   333
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   334
\     ==> leadsTo acts (A Int f-``{m}) B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   335
by (eres_inst_tac [("a","m")] wf_induct 1);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   336
by (subgoal_tac "leadsTo acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   337
by (stac vimage_eq_UN 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   338
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   339
by (blast_tac (claset() addIs [leadsTo_UN]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   340
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   341
val lemma = result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   342
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   343
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   344
(** Meta or object quantifier ????? **)
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   345
Goal "[| wf r;     \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   346
\        ALL m. leadsTo acts (A Int f-``{m})                     \
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   347
\                            ((A Int f-``(r^-1 ^^ {m})) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   348
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   349
\     ==> leadsTo acts A B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   350
by (res_inst_tac [("t", "A")] subst 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   351
by (rtac leadsTo_UN 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   352
by (etac lemma 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   353
by (REPEAT (assume_tac 2));
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   354
by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   355
qed "leadsTo_wf_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   356
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   357
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   358
Goal "[| wf r;     \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   359
\        ALL m:I. leadsTo acts (A Int f-``{m})                   \
5257
c03e3ba9cbcc Indentation, comments
paulson
parents: 5253
diff changeset
   360
\                              ((A Int f-``(r^-1 ^^ {m})) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   361
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   362
\     ==> leadsTo acts A ((A - (f-``I)) Un B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   363
by (etac leadsTo_wf_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   364
by Safe_tac;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   365
by (case_tac "m:I" 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   366
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   367
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   368
qed "bounded_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   369
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   370
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   371
(*Alternative proof is via the lemma leadsTo acts (A Int f-``(lessThan m)) B*)
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   372
Goal "[| ALL m. leadsTo acts (A Int f-``{m})                     \
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   373
\                            ((A Int f-``(lessThan m)) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   374
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   375
\     ==> leadsTo acts A B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   376
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   377
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   378
by (Asm_simp_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   379
qed "lessThan_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   380
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   381
Goal "[| ALL m:(greaterThan l). leadsTo acts (A Int f-``{m})   \
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   382
\                                  ((A Int f-``(lessThan m)) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   383
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   384
\     ==> leadsTo acts A ((A Int (f-``(atMost l))) Un B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   385
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   386
by (rtac (wf_less_than RS bounded_induct) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   387
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   388
by (Asm_simp_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   389
qed "lessThan_bounded_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   390
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   391
Goal "[| ALL m:(lessThan l). leadsTo acts (A Int f-``{m})   \
5239
2fd94efb9d64 Tidying
paulson
parents: 5232
diff changeset
   392
\                              ((A Int f-``(greaterThan m)) Un B);   \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   393
\        id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   394
\     ==> leadsTo acts A ((A Int (f-``(atLeast l))) Un B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   395
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   396
    (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   397
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   398
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   399
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   400
by (case_tac "m<l" 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   401
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   402
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   403
qed "greaterThan_bounded_induct";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   404
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   405
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   406
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   407
(*** wlt ****)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   408
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   409
(*Misra's property W3*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   410
Goalw [wlt_def] "leadsTo acts (wlt acts B) B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   411
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   412
qed "wlt_leadsTo";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   413
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   414
Goalw [wlt_def] "leadsTo acts A B ==> A <= wlt acts B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   415
by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   416
qed "leadsTo_subset";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   417
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   418
(*Misra's property W2*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   419
Goal "id: acts ==> leadsTo acts A B = (A <= wlt acts B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   420
by (blast_tac (claset() addSIs [leadsTo_subset, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   421
				wlt_leadsTo RS leadsTo_weaken_L]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   422
qed "leadsTo_eq_subset_wlt";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   423
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   424
(*Misra's property W4*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   425
Goal "id: acts ==> B <= wlt acts B";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   426
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   427
				      subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   428
qed "wlt_increasing";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   429
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   430
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   431
(*Used in the Trans case below*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4776
diff changeset
   432
Goalw [constrains_def]
5111
8f4b72f0c15d Uncurried functions LeadsTo and reach
paulson
parents: 5069
diff changeset
   433
   "[| B <= A2;  \
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   434
\      constrains acts (A1 - B) (A1 Un B); \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   435
\      constrains acts (A2 - C) (A2 Un C) |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   436
\   ==> constrains acts (A1 Un A2 - C) (A1 Un A2 Un C)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   437
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   438
by (blast_tac (claset() addSDs [bspec]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   439
val lemma1 = result();
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   440
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   441
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   442
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   443
Goal "[| leadsTo acts A A';  id: acts |] ==> \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   444
\      EX B. A<=B & leadsTo acts B A' & constrains acts (B-A') (B Un A')";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   445
by (etac leadsTo_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   446
(*Basis*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   447
by (blast_tac (claset() addIs [leadsTo_Basis]
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   448
                        addDs [ensuresD]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   449
(*Trans*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   450
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   451
by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   452
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   453
			       leadsTo_Un_duplicate]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   454
(*Union*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   455
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   456
				  bchoice, ball_constrains_UN]) 1);;
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   457
by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   458
by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   459
qed "leadsTo_123";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   460
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   461
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   462
(*Misra's property W5*)
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   463
Goal "id: acts ==> constrains acts (wlt acts B - B) (wlt acts B)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   464
by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   465
by (Clarify_tac 1);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   466
by (subgoal_tac "Ba = wlt acts B" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   467
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   468
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   469
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   470
qed "wlt_constrains_wlt";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   471
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   472
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   473
(*** Completion: Binary and General Finite versions ***)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   474
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   475
Goal "[| leadsTo acts A A';  stable acts A';   \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   476
\      leadsTo acts B B';  stable acts B';  id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   477
\   ==> leadsTo acts (A Int B) (A' Int B')";
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   478
by (subgoal_tac "stable acts (wlt acts B')" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   479
by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   480
by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   481
	   etac wlt_constrains_wlt 2,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   482
	   fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   483
	   Blast_tac 2]);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   484
by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   485
by (blast_tac (claset() addIs [PSP_stable]) 2);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   486
by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   487
by (blast_tac (claset() addIs [wlt_leadsTo, PSP_stable2]) 2);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   488
by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   489
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   490
			       subset_imp_leadsTo]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   491
(*Blast_tac gives PROOF FAILED*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   492
by (best_tac (claset() addIs [leadsTo_Trans]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   493
qed "stable_completion";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   494
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   495
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   496
Goal "[| finite I;  id: acts |]                     \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   497
\   ==> (ALL i:I. leadsTo acts (A i) (A' i)) -->  \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   498
\       (ALL i:I. stable acts (A' i)) -->         \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   499
\       leadsTo acts (INT i:I. A i) (INT i:I. A' i)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   500
by (etac finite_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   501
by (Asm_simp_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   502
by (asm_simp_tac 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   503
    (simpset() addsimps [stable_completion, stable_def, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   504
			 ball_constrains_INT]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   505
qed_spec_mp "finite_stable_completion";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   506
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   507
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   508
Goal "[| W = wlt acts (B' Un C);     \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   509
\      leadsTo acts A (A' Un C);  constrains acts A' (A' Un C);   \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   510
\      leadsTo acts B (B' Un C);  constrains acts B' (B' Un C);   \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   511
\      id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   512
\   ==> leadsTo acts (A Int B) ((A' Int B') Un C)";
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   513
by (subgoal_tac "constrains acts (W-C) (W Un B' Un C)" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   514
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   515
			       MRS constrains_Un RS constrains_weaken]) 2);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   516
by (subgoal_tac "constrains acts (W-C) W" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   517
by (asm_full_simp_tac 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   518
    (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   519
by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   520
by (simp_tac (simpset() addsimps [Int_Diff]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   521
by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   522
by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   523
by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   524
                               PSP2 RS leadsTo_weaken_R, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   525
			       subset_refl RS subset_imp_leadsTo, 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   526
			       leadsTo_Un_duplicate2]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   527
by (dtac leadsTo_Diff 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   528
by (assume_tac 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   529
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   530
by (subgoal_tac "A Int B <= A Int W" 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   531
by (blast_tac (claset() addIs [leadsTo_subset, Int_mono] 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   532
	                delrules [subsetI]) 2);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   533
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   534
bind_thm("completion", refl RS result());
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   535
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   536
5253
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   537
Goal "[| finite I;  id: acts |] \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   538
\   ==> (ALL i:I. leadsTo acts (A i) (A' i Un C)) -->  \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   539
\       (ALL i:I. constrains acts (A' i) (A' i Un C)) --> \
82a5ca6290aa New record type of programs
paulson
parents: 5239
diff changeset
   540
\       leadsTo acts (INT i:I. A i) ((INT i:I. A' i) Un C)";
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   541
by (etac finite_induct 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   542
by (ALLGOALS Asm_simp_tac);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   543
by (Clarify_tac 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   544
by (dtac ball_constrains_INT 1);
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   545
by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   546
qed "finite_completion";
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
   547