src/HOL/UNITY/Project.ML
author paulson
Tue, 21 Dec 1999 15:03:02 +0100
changeset 8069 19b9f92ca503
parent 8065 658e0d4e4ed9
child 8073 6c99b44b333e
permissions -rw-r--r--
working with weak LeadsTo in guarantees precondition\!
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Project.ML
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     2
    ID:         $Id$
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     5
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     6
Projections of state sets (also of actions and programs)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     7
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     8
Inheritance of GUARANTEES properties under extension
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
     9
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
    10
POSSIBLY CAN DELETE Restrict_image_Diff
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    11
*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    12
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    13
Open_locale "Extend";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    14
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    15
(** projection: monotonicity for safety **)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    16
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 8002
diff changeset
    17
Goal "D <= C ==> \
e3237d8c18d6 working version with new theory ELT
paulson
parents: 8002
diff changeset
    18
\     project_act h (Restrict D act) <= project_act h (Restrict C act)";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    19
by (auto_tac (claset(), simpset() addsimps [project_act_def]));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    20
qed "project_act_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    21
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    22
Goal "[| D <= C; project h C F : A co B |] ==> project h D F : A co B";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    23
by (auto_tac (claset(), simpset() addsimps [constrains_def]));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
    24
by (dtac project_act_mono 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    25
by (Blast_tac 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    26
qed "project_constrains_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    27
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    28
Goal "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    29
by (asm_full_simp_tac
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    30
    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    31
qed "project_stable_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    32
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    33
Goal "F : A co B ==> project h C (extend h F) : A co B";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    34
by (auto_tac (claset(), 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    35
      simpset() addsimps [extend_act_def, project_act_def, constrains_def]));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    36
qed "project_extend_constrains_I";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    37
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    38
Goal "UNIV <= project_set h C \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    39
\     ==> project h C ((extend h F) Join G) = F Join (project h C G)";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    40
by (rtac program_equalityI 1);
7915
c7fd7eb3b0ef ALMOST working version: LocalTo results commented out
paulson
parents: 7880
diff changeset
    41
by (asm_simp_tac (simpset() addsimps [image_eq_UN, UN_Un,
7878
43b03d412b82 working version with localTo[C] instead of localTo
paulson
parents: 7841
diff changeset
    42
			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    43
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    44
qed "project_extend_Join";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    45
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    46
Goal "UNIV <= project_set h C \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    47
\     ==> (extend h F) Join G = extend h H ==> H = F Join (project h C G)";
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    48
by (dres_inst_tac [("f", "project h C")] arg_cong 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    49
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    50
qed "extend_Join_eq_extend_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    51
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    52
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    53
(** Safety **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    54
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    55
Goalw [constrains_def]
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    56
     "(project h C F : A co B)  =  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    57
\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    58
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    59
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    60
(*the <== direction*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    61
by (rewtac project_act_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    62
by (force_tac (claset() addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    63
qed "project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    64
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    65
Goalw [stable_def]
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    66
     "(project h UNIV F : stable A) = (F : stable (extend_set h A))";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    67
by (simp_tac (simpset() addsimps [project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    68
qed "project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    69
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    70
Goal "F : stable (extend_set h A) ==> project h C F : stable A";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
    71
by (dtac (project_stable RS iffD2) 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    72
by (blast_tac (claset() addIs [project_stable_mono]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    73
qed "project_stable_I";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    74
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    75
(*used below to prove Join_project_ensures*)
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    76
Goal "[| G : stable C;  project h C G : A unless B |] \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    77
\     ==> G : (C Int extend_set h A) unless (extend_set h B)";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    78
by (asm_full_simp_tac
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    79
    (simpset() addsimps [unless_def, project_constrains]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    80
by (blast_tac (claset() addDs [stable_constrains_Int]
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    81
			addIs [constrains_weaken]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    82
qed_spec_mp "project_unless";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    83
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    84
(*This form's useful with guarantees reasoning*)
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    85
Goal "(F Join project h C G : A co B)  =  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    86
\       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    87
\        F : A co B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    88
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    89
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    90
                        addDs [constrains_imp_subset]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    91
qed "Join_project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    92
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    93
(*The condition is required to prove the left-to-right direction;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    94
  could weaken it to G : (C Int extend_set h A) co C*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    95
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    96
     "extend h F Join G : stable C \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
    97
\     ==> (F Join project h C G : stable A)  =  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    98
\         (extend h F Join G : stable (C Int extend_set h A) &  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    99
\          F : stable A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   100
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   101
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   102
qed "Join_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   103
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   104
(*For using project_guarantees in particular cases*)
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   105
Goal "extend h F Join G : extend_set h A co extend_set h B \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   106
\     ==> F Join project h C G : A co B";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   107
by (asm_full_simp_tac
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   108
    (simpset() addsimps [project_constrains, Join_constrains, 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   109
			 extend_constrains]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   110
by (blast_tac (claset() addIs [constrains_weaken]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   111
			addDs [constrains_imp_subset]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   112
qed "project_constrains_I";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   113
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   114
Goalw [increasing_def, stable_def]
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   115
     "extend h F Join G : increasing (func o f) \
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   116
\     ==> F Join project h C G : increasing func";
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   117
by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   118
					   Collect_eq_extend_set RS sym]) 1);
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   119
qed "project_increasing_I";
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   120
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   121
Goal "(F Join project h UNIV G : increasing func)  =  \
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   122
\     (extend h F Join G : increasing (func o f))";
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   123
by (rtac iffI 1);
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   124
by (etac project_increasing_I 2);
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   125
by (asm_full_simp_tac 
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   126
    (simpset() addsimps [increasing_def, Join_project_stable]) 1);
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   127
by (auto_tac (claset(),
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   128
	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   129
				  extend_stable RS iffD1]));
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   130
qed "Join_project_increasing";
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   131
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   132
(*The UNIV argument is essential*)
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   133
Goal "F Join project h UNIV G : A co B \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   134
\     ==> extend h F Join G : extend_set h A co extend_set h B";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   135
by (asm_full_simp_tac
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   136
    (simpset() addsimps [project_constrains, Join_constrains, 
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   137
			 extend_constrains]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   138
qed "project_constrains_D";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   139
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   140
(** "projecting" and union/intersection (no converses) **)
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   141
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   142
Goalw [projecting_def]
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   143
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   144
\     ==> projecting C h F (XA' Int XB') (XA Int XB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   145
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   146
qed "projecting_Int";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   147
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   148
Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   149
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   150
\     ==> projecting C h F (XA' Un XB') (XA Un XB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   151
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   152
qed "projecting_Un";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   153
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   154
val [prem] = Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   155
     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   156
\     ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   157
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   158
qed "projecting_INT";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   159
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   160
val [prem] = Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   161
     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   162
\     ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   163
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   164
qed "projecting_UN";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   165
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   166
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   167
     "[| projecting C h F X' X;  U'<=X';  X<=U |] ==> projecting C h F U' U";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   168
by Auto_tac;
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   169
qed "projecting_weaken";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   170
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   171
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   172
     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   173
\     ==> extending v C h F (YA' Int YB') (YA Int YB)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   174
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   175
qed "extending_Int";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   176
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   177
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   178
     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   179
\     ==> extending v C h F (YA' Un YB') (YA Un YB)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   180
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   181
qed "extending_Un";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   182
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   183
val [prem] = Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   184
     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   185
\     ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   186
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   187
qed "extending_INT";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   188
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   189
val [prem] = Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   190
     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   191
\     ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   192
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   193
qed "extending_UN";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   194
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   195
Goalw [extending_def]
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   196
     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y; \
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   197
\        preserves w <= preserves v |] \
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   198
\     ==> extending w C h F V' V";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   199
by Auto_tac;
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   200
qed "extending_weaken";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   201
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   202
Goal "projecting C h F X' UNIV";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   203
by (simp_tac (simpset() addsimps [projecting_def]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   204
qed "projecting_UNIV";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   205
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   206
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   207
     "projecting C h F (extend_set h A co extend_set h B) (A co B)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   208
by (blast_tac (claset() addIs [project_constrains_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   209
qed "projecting_constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   210
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   211
Goalw [stable_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   212
     "projecting C h F (stable (extend_set h A)) (stable A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   213
by (rtac projecting_constrains 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   214
qed "projecting_stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   215
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   216
Goalw [projecting_def]
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   217
     "projecting C h F (increasing (func o f)) (increasing func)";
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   218
by (blast_tac (claset() addIs [project_increasing_I]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   219
qed "projecting_increasing";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   220
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   221
Goal "extending v C h F UNIV Y";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   222
by (simp_tac (simpset() addsimps [extending_def]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   223
qed "extending_UNIV";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   224
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   225
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   226
     "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   227
by (blast_tac (claset() addIs [project_constrains_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   228
qed "extending_constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   229
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   230
Goalw [stable_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   231
     "extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   232
by (rtac extending_constrains 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   233
qed "extending_stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   234
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   235
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   236
     "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   237
by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   238
qed "extending_increasing";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   239
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   240
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   241
(** Reachability and project **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   242
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   243
Goal "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   244
\        z : reachable (extend h F Join G) |] \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   245
\     ==> f z : reachable (F Join project h C G)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   246
by (etac reachable.induct 1);
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   247
by (force_tac (claset() addSIs [reachable.Init],
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   248
	       simpset() addsimps [split_extended_all]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   249
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   250
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   251
	       simpset()) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   252
by (res_inst_tac [("act","x")] reachable.Acts 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   253
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   254
by (etac extend_act_D 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   255
qed "reachable_imp_reachable_project";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   256
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   257
(*The extra generality in the first premise allows guarantees with STRONG
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   258
  preconditions (localT) and WEAK postconditions.*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   259
(*LOCALTO NO LONGER EXISTS: replace C by reachable...??*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   260
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   261
     "[| reachable (extend h F Join G) <= C;    \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   262
\        F Join project h C G : A Co B |] \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   263
\     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   264
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   265
by (Clarify_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   266
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   267
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   268
qed "project_Constrains_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   269
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   270
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   271
     "[| reachable (extend h F Join G) <= C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   272
\        F Join project h C G : Stable A |]   \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   273
\     ==> extend h F Join G : Stable (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   274
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   275
qed "project_Stable_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   276
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   277
Goalw [Always_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   278
     "[| reachable (extend h F Join G) <= C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   279
\        F Join project h C G : Always A |]   \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   280
\     ==> extend h F Join G : Always (extend_set h A)";
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   281
by (force_tac (claset() addIs [reachable.Init],
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   282
               simpset() addsimps [project_Stable_D, split_extended_all]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   283
qed "project_Always_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   284
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   285
Goalw [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   286
     "[| reachable (extend h F Join G) <= C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   287
\        F Join project h C G : Increasing func |] \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   288
\     ==> extend h F Join G : Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   289
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   290
by (stac Collect_eq_extend_set 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   291
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   292
qed "project_Increasing_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   293
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   294
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   295
(** Converse results for weak safety: benefits of the argument C *)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   296
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   297
Goal "[| C <= reachable(extend h F Join G);   \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   298
\        x : reachable (F Join project h C G) |] \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   299
\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   300
by (etac reachable.induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   301
by (ALLGOALS Asm_full_simp_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   302
(*SLOW: 6.7s*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   303
by (force_tac (claset() delrules [Id_in_Acts]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   304
		        addIs [reachable.Acts, extend_act_D],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   305
	       simpset() addsimps [project_act_def]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   306
by (force_tac (claset() addIs [reachable.Init],
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   307
	       simpset()) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   308
qed "reachable_project_imp_reachable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   309
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   310
Goal "project_set h (reachable (extend h F Join G)) = \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   311
\     reachable (F Join project h (reachable (extend h F Join G)) G)";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   312
by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   313
			      subset_refl RS reachable_project_imp_reachable], 
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   314
	      simpset()));
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   315
qed "project_set_reachable_extend_eq";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   316
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   317
Goal "reachable (extend h F Join G) <= C  \
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   318
\     ==> reachable (extend h F Join G) <= \
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   319
\         extend_set h (reachable (F Join project h C G))";
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   320
by (auto_tac (claset() addDs [reachable_imp_reachable_project], 
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   321
	      simpset()));
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   322
qed "reachable_extend_Join_subset";
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   323
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   324
(*Perhaps should replace C by reachable...*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   325
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   326
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   327
\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   328
\     ==> F Join project h C G : A Co B";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   329
by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   330
				       extend_set_Int_distrib]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   331
by (rtac conjI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   332
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   333
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   334
by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   335
(*Some generalization of constrains_weaken_L would be better, but what is it?*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   336
by (rewtac constrains_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   337
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   338
by (thin_tac "ALL act : Acts G. ?P act" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   339
by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   340
	       simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   341
qed "project_Constrains_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   342
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   343
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   344
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   345
\        extend h F Join G : Stable (extend_set h A) |] \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   346
\     ==> F Join project h C G : Stable A";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   347
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   348
qed "project_Stable_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   349
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   350
Goalw [Always_def]
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   351
     "[| C <= reachable (extend h F Join G);  \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   352
\        extend h F Join G : Always (extend_set h A) |]   \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   353
\     ==> F Join project h C G : Always A";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   354
by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   355
by (rewtac extend_set_def);
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   356
by (Blast_tac 1);
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   357
qed "project_Always_I";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   358
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   359
Goalw [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   360
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   361
\        extend h F Join G : Increasing (func o f) |] \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   362
\     ==> F Join project h C G : Increasing func";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   363
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   364
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   365
				      project_Stable_I]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   366
qed "project_Increasing_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   367
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   368
Goal "(F Join project h (reachable (extend h F Join G)) G : A Co B)  =  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   369
\     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   370
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   371
qed "project_Constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   372
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   373
Goalw [Stable_def]
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   374
     "(F Join project h (reachable (extend h F Join G)) G : Stable A)  =  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   375
\     (extend h F Join G : Stable (extend_set h A))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   376
by (rtac project_Constrains 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   377
qed "project_Stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   378
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   379
Goal
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   380
   "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  = \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   381
\   (extend h F Join G : Increasing (func o f))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   382
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   383
				      Collect_eq_extend_set RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   384
qed "project_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   385
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   386
(** A lot of redundant theorems: all are proved to facilitate reasoning
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   387
    about guarantees. **)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   388
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   389
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   390
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   391
\                (extend_set h A Co extend_set h B) (A Co B)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   392
by (blast_tac (claset() addIs [project_Constrains_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   393
qed "projecting_Constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   394
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   395
Goalw [Stable_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   396
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   397
\                (Stable (extend_set h A)) (Stable A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   398
by (rtac projecting_Constrains 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   399
qed "projecting_Stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   400
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   401
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   402
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   403
\                (Always (extend_set h A)) (Always A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   404
by (blast_tac (claset() addIs [project_Always_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   405
qed "projecting_Always";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   406
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   407
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   408
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   409
\                (Increasing (func o f)) (Increasing func)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   410
by (blast_tac (claset() addIs [project_Increasing_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   411
qed "projecting_Increasing";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   412
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   413
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   414
     "extending v (%G. reachable (extend h F Join G)) h F \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   415
\                 (extend_set h A Co extend_set h B) (A Co B)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   416
by (blast_tac (claset() addIs [project_Constrains_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   417
qed "extending_Constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   418
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   419
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   420
     "extending v (%G. reachable (extend h F Join G)) h F \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   421
\                 (Stable (extend_set h A)) (Stable A)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   422
by (blast_tac (claset() addIs [project_Stable_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   423
qed "extending_Stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   424
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   425
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   426
     "extending v (%G. reachable (extend h F Join G)) h F \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   427
\                 (Always (extend_set h A)) (Always A)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   428
by (blast_tac (claset() addIs [project_Always_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   429
qed "extending_Always";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   430
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   431
val [prem] = 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   432
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   433
     "(!!G. reachable (extend h F Join G) <= C G)  \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   434
\     ==> extending v C h F (Increasing (func o f)) (Increasing func)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   435
by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   436
qed "extending_Increasing";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   437
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   438
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   439
(** Progress includes safety in the definition of ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   440
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   441
(*** Progress for (project h C F) ***)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   442
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   443
(** transient **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   444
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   445
(*Premise is that C includes the domains of all actions that could be the
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   446
  transient one.  Could have C=UNIV of course*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   447
Goalw [transient_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   448
     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   449
\                      Domain act <= C;    \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   450
\        F : transient (extend_set h A) |] \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   451
\     ==> project h C F : transient A";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   452
by (auto_tac (claset() delrules [ballE],
7915
c7fd7eb3b0ef ALMOST working version: LocalTo results commented out
paulson
parents: 7880
diff changeset
   453
              simpset() addsimps [Domain_project_act, Int_absorb1]));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   454
by (REPEAT (ball_tac 1));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   455
by (auto_tac (claset(),
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   456
              simpset() addsimps [extend_set_def, project_act_def]));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   457
by (ALLGOALS Blast_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   458
qed "transient_extend_set_imp_project_transient";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   459
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   460
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   461
(** ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   462
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   463
(*For simplicity, the complicated condition on C is eliminated
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   464
  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   465
Goal "F : (extend_set h A) ensures (extend_set h B) \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   466
\     ==> project h UNIV F : A ensures B";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   467
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   468
    (simpset() addsimps [ensures_def, project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   469
			 transient_extend_set_imp_project_transient,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   470
			 extend_set_Un_distrib RS sym, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   471
			 extend_set_Diff_distrib RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   472
by (Blast_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   473
qed "ensures_extend_set_imp_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   474
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   475
Goal "[| project h C G ~: transient (A-B) | A<=B;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   476
\        extend h F Join G : stable C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   477
\        F Join project h C G : A ensures B |] \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   478
\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   479
by (etac disjE 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   480
by (blast_tac (claset() addIs [subset_imp_ensures]) 2);
8002
paulson
parents: 7947
diff changeset
   481
by (auto_tac (claset() addDs [extend_transient RS iffD2] 
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 8002
diff changeset
   482
                       addIs [transient_strengthen, project_set_I,
8002
paulson
parents: 7947
diff changeset
   483
			      project_unless RS unlessD, unlessI, 
paulson
parents: 7947
diff changeset
   484
			      project_extend_constrains_I], 
paulson
parents: 7947
diff changeset
   485
	      simpset() addsimps [ensures_def, Join_constrains,
paulson
parents: 7947
diff changeset
   486
				  Join_stable, Join_transient]));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   487
qed_spec_mp "Join_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   488
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   489
(** Lemma useful for both STRONG and WEAK progress*)
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   490
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   491
(*The strange induction formula allows induction over the leadsTo
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   492
  assumption's non-atomic precondition*)
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   493
Goal "[| ALL D. project h C G : transient D --> D={};  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   494
\        extend h F Join G : stable C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   495
\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   496
\     ==> extend h F Join G : \
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   497
\         C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   498
by (etac leadsTo_induct 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   499
by (asm_simp_tac (simpset() delsimps UN_simps
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   500
		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 8002
diff changeset
   501
by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L, 
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   502
			       leadsTo_Trans]) 2);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   503
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   504
val lemma = result();
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   505
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   506
Goal "[| ALL D. project h C G : transient D --> D={};  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   507
\        extend h F Join G : stable C;  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   508
\        F Join project h C G : (project_set h C Int A) leadsTo B |] \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   509
\     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   510
by (rtac (lemma RS leadsTo_weaken) 1);
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   511
by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   512
qed "project_leadsTo_lemma";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   513
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   514
Goal "[| C = (reachable (extend h F Join G)); \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   515
\        ALL D. project h C G : transient D --> D={};  \
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   516
\        F Join project h C G : A LeadsTo B |] \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   517
\     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   518
by (asm_full_simp_tac 
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   519
    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, 
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   520
			 project_set_reachable_extend_eq]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   521
qed "Join_project_LeadsTo";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   522
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   523
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   524
(*** GUARANTEES and EXTEND ***)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   525
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   526
(** preserves **)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   527
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   528
Goal "G : preserves (v o f) ==> project h C G : preserves v";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   529
by (auto_tac (claset(),
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   530
	      simpset() addsimps [preserves_def, project_stable_I,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   531
				  Collect_eq_extend_set RS sym]));
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   532
qed "project_preserves_I";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   533
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   534
(*to preserve f is to preserve the whole original state*)
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   535
Goal "G : preserves f ==> project h C G : preserves id";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   536
by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   537
qed "project_preserves_id_I";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   538
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   539
Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   540
by (auto_tac (claset(),
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   541
	      simpset() addsimps [preserves_def, extend_stable RS sym,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   542
				  Collect_eq_extend_set RS sym]));
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   543
qed "extend_preserves";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   544
8065
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   545
Goal "inj h ==> (extend h G : preserves g)";
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   546
by (auto_tac (claset(),
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   547
	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   548
				  stable_def, constrains_def, g_def]));
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   549
qed "inj_extend_preserves";
658e0d4e4ed9 first working version to Alloc/System_Client_Progress;
paulson
parents: 8055
diff changeset
   550
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   551
(** Strong precondition and postcondition; doesn't seem very useful. **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   552
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   553
Goal "F : X guarantees[v] Y ==> \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   554
\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   555
by (rtac guaranteesI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   556
by Auto_tac;
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   557
by (blast_tac (claset() addIs [project_preserves_I]
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   558
			addDs [project_set_UNIV RS equalityD2 RS 
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   559
			       extend_Join_eq_extend_D, 
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   560
			       guaranteesD]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   561
qed "guarantees_imp_extend_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   562
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   563
Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   564
\     ==> F : X guarantees[v] Y";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   565
by (auto_tac (claset(), simpset() addsimps [guar_def]));
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   566
by (dres_inst_tac [("x", "extend h G")] spec 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   567
by (asm_full_simp_tac 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   568
    (simpset() delsimps [extend_Join] 
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   569
           addsimps [extend_Join RS sym, extend_preserves,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   570
		     inj_extend RS inj_image_mem_iff]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   571
qed "extend_guarantees_imp_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   572
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   573
Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   574
\    (F : X guarantees[v] Y)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   575
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   576
			       extend_guarantees_imp_guarantees]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   577
qed "extend_guarantees_eq";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   578
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   579
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   580
(*Weak precondition and postcondition; this is the good one!
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   581
  Not clear that it has a converse [or that we want one!]*)
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   582
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   583
(*The raw version*)
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   584
val [xguary,project,extend] =
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   585
Goal "[| F : X guarantees[v] Y;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   586
\        !!G. extend h F Join G : X' ==> F Join project h C G : X;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   587
\        !!G. [| F Join project h C G : Y; extend h F Join G : X' |] \
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   588
\             ==> extend h F Join G : Y' |] \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   589
\     ==> extend h F : X' guarantees[v o f] Y'";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   590
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   591
by (etac project_preserves_I 1);
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   592
by (etac project 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   593
by (assume_tac 1);
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 8002
diff changeset
   594
qed "project_guarantees_raw";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   595
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   596
Goal "[| F : X guarantees[v] Y;  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   597
\        projecting C h F X' X;  extending w C h F Y' Y; \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   598
\        preserves w <= preserves (v o f) |] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   599
\     ==> extend h F : X' guarantees[w] Y'";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   600
by (rtac guaranteesI 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   601
by (auto_tac (claset(), 
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   602
        simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   603
			    extending_def]));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   604
qed "project_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   605
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   606
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   607
(*It seems that neither "guarantees" law can be proved from the other.*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   608
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   609
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   610
(*** guarantees corollaries ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   611
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   612
(** Some could be deleted: the required versions are easy to prove **)
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   613
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   614
Goal "F : UNIV guarantees[v] increasing func \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   615
\     ==> extend h F : X' guarantees[v o f] increasing (func o f)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   616
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   617
by (rtac extending_increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   618
by (rtac projecting_UNIV 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   619
by Auto_tac;
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   620
qed "extend_guar_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   621
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   622
Goal "F : UNIV guarantees[v] Increasing func \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   623
\     ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   624
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   625
by (rtac extending_Increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   626
by (rtac projecting_UNIV 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   627
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   628
qed "extend_guar_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   629
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   630
Goal "F : Always A guarantees[v] Always B \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   631
\     ==> extend h F : Always(extend_set h A) guarantees[v o f] \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   632
\                      Always(extend_set h B)";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   633
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   634
by (rtac extending_Always 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   635
by (rtac projecting_Always 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   636
by Auto_tac;
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   637
qed "extend_guar_Always";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   638
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   639
Goal "[| G : preserves f;  project h C G : transient D |] ==> D={}";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   640
by (rtac stable_transient_empty 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   641
by (assume_tac 2);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   642
by (blast_tac (claset() addIs [project_preserves_id_I,
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   643
			 impOfSubs preserves_id_subset_stable]) 1);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   644
qed "preserves_project_transient_empty";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   645
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   646
8069
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   647
(** Guarantees with a leadsTo postcondition 
19b9f92ca503 working with weak LeadsTo in guarantees precondition\!
paulson
parents: 8065
diff changeset
   648
    THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   649
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   650
Goal "[| F Join project h UNIV G : A leadsTo B;    \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   651
\        G : preserves f |]  \
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   652
\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
7947
b999c1ab9327 working again; new treatment of LocalTo
paulson
parents: 7915
diff changeset
   653
by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   654
by (auto_tac (claset() addDs [preserves_project_transient_empty], 
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   655
	      simpset()));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   656
qed "project_leadsTo_D";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   657
7880
62fb24e28e5e exchanged the first two args of "project" and "drop_prog"
paulson
parents: 7878
diff changeset
   658
Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   659
\         G : preserves f |]  \
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   660
\      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   661
by (rtac (refl RS Join_project_LeadsTo) 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   662
by (auto_tac (claset() addDs [preserves_project_transient_empty], 
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   663
	      simpset()));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   664
qed "project_LeadsTo_D";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   665
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   666
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   667
     "extending f (%G. UNIV) h F \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   668
\                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   669
by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   670
qed "extending_leadsTo";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   671
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   672
Goalw [extending_def]
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   673
     "extending f (%G. reachable (extend h F Join G)) h F \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   674
\                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   675
by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   676
qed "extending_LeadsTo";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   677
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   678
(*STRONG precondition and postcondition*)
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   679
Goal "F : (A co A') guarantees[v] (B leadsTo B')  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   680
\ ==> extend h F : (extend_set h A co extend_set h A') \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   681
\                  guarantees[f] (extend_set h B leadsTo extend_set h B')";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   682
by (etac project_guarantees 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   683
by (rtac subset_preserves_o 3);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   684
by (rtac extending_leadsTo 2);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   685
by (rtac projecting_constrains 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   686
qed "extend_co_guar_leadsTo";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   687
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   688
(*WEAK precondition and postcondition*)
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   689
Goal "F : (A Co A') guarantees[v] (B LeadsTo B')  \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   690
\ ==> extend h F : (extend_set h A Co extend_set h A') \
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   691
\                  guarantees[f] (extend_set h B LeadsTo extend_set h B')";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   692
by (etac project_guarantees 1);
8055
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   693
by (rtac subset_preserves_o 3);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   694
by (rtac extending_LeadsTo 2);
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents: 8041
diff changeset
   695
by (rtac projecting_Constrains 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   696
qed "extend_Co_guar_LeadsTo";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   697
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   698
Close_locale "Extend";