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