src/HOL/UNITY/Project.ML
author paulson
Wed, 13 Oct 1999 12:05:25 +0200
changeset 7841 65d91d13fc13
parent 7826 c6a8b73b6c2a
child 7878 43b03d412b82
permissions -rw-r--r--
working snapshot; more steps in Alloc
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
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
     9
*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    10
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    11
Open_locale "Extend";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    12
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    13
(** projection: monotonicity for safety **)
7630
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
Goal "D <= C ==> project_act D h act <= project_act C h act";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    16
by (auto_tac (claset(), simpset() addsimps [project_act_def]));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    17
qed "project_act_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    18
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    19
Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    20
by (auto_tac (claset(), simpset() addsimps [constrains_def]));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
    21
by (dtac project_act_mono 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    22
by (Blast_tac 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    23
qed "project_constrains_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    24
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    25
Goal "[| D <= C;  project C h F : stable A |] ==> project D h F : stable A";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    26
by (asm_full_simp_tac
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    27
    (simpset() addsimps [stable_def, project_constrains_mono]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    28
qed "project_stable_mono";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    29
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    30
Goal "F : A co B ==> project C h (extend h F) : A co B";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    31
by (auto_tac (claset(), 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    32
      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
    33
qed "project_extend_constrains_I";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    34
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    35
Goal "UNIV <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    36
\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    37
by (rtac program_equalityI 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    38
by (asm_simp_tac (simpset() addsimps [image_Un, image_image,
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    39
			subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    40
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    41
qed "project_extend_Join";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    42
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    43
Goal "UNIV <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    44
\     ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    45
by (dres_inst_tac [("f", "project C h")] arg_cong 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    46
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    47
qed "extend_Join_eq_extend_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    48
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    49
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    50
(** Safety **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    51
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    52
Goalw [constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    53
     "(project C h F : A co B)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    54
\     (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
    55
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    56
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    57
(*the <== direction*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    58
by (rewtac project_act_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    59
by (force_tac (claset() addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    60
qed "project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    61
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    62
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    63
     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    64
by (simp_tac (simpset() addsimps [project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    65
qed "project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    66
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    67
Goal "F : stable (extend_set h A) ==> project C h F : stable A";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
    68
by (dtac (project_stable RS iffD2) 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    69
by (blast_tac (claset() addIs [project_stable_mono]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    70
qed "project_stable_I";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    71
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    72
(*used below to prove Join_project_ensures*)
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    73
Goal "[| G : stable C;  project C h G : A unless B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    74
\     ==> 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
    75
by (asm_full_simp_tac
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    76
    (simpset() addsimps [unless_def, project_constrains]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    77
by (blast_tac (claset() addDs [stable_constrains_Int]
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    78
			addIs [constrains_weaken]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    79
qed_spec_mp "project_unless";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
    80
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    81
(*This form's useful with guarantees reasoning*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    82
Goal "(F Join project C h G : A co B)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    83
\       (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
    84
\        F : A co B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    85
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    86
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    87
                        addDs [constrains_imp_subset]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    88
qed "Join_project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    89
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    90
(*The condition is required to prove the left-to-right direction;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    91
  could weaken it to G : (C Int extend_set h A) co C*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    92
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    93
     "extend h F Join G : stable C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    94
\     ==> (F Join project C h G : stable A)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    95
\         (extend h F Join G : stable (C Int extend_set h A) &  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    96
\          F : stable A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    97
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    98
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    99
qed "Join_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   100
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   101
Goal "(F Join project UNIV h G : increasing func)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   102
\     (extend h F Join G : increasing (func o f))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   103
by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   104
by (auto_tac (claset(),
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   105
	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   106
				  extend_stable RS iffD1]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   107
qed "Join_project_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   108
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   109
(*For using project_guarantees in particular cases*)
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   110
Goal "extend h F Join G : extend_set h A co extend_set h B \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   111
\     ==> F Join project C h G : A co B";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   112
by (asm_full_simp_tac
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   113
    (simpset() addsimps [project_constrains, Join_constrains, 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   114
			 extend_constrains]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   115
by (blast_tac (claset() addIs [constrains_weaken]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   116
			addDs [constrains_imp_subset]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   117
qed "project_constrains_I";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   118
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   119
(*The UNIV argument is essential*)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   120
Goal "F Join project UNIV h G : A co B \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   121
\     ==> 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
   122
by (asm_full_simp_tac
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   123
    (simpset() addsimps [project_constrains, Join_constrains, 
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   124
			 extend_constrains]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   125
qed "project_constrains_D";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   126
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   127
(** "projecting" and union/intersection **)
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   128
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   129
Goalw [projecting_def]
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   130
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   131
\     ==> projecting C h F (XA' Int XB') (XA Int XB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   132
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   133
qed "projecting_Int";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   134
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   135
Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   136
     "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   137
\     ==> projecting C h F (XA' Un XB') (XA Un XB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   138
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   139
qed "projecting_Un";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   140
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   141
val [prem] = Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   142
     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   143
\     ==> 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
   144
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   145
qed "projecting_INT";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   146
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   147
val [prem] = Goalw [projecting_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   148
     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   149
\     ==> 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
   150
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   151
qed "projecting_UN";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   152
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   153
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   154
     "[| 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
   155
by Auto_tac;
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   156
qed "projecting_weaken";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   157
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   158
Goalw [extending_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   159
     "[| extending C h F X' YA' YA;  extending C h F X' YB' YB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   160
\     ==> extending C h F X' (YA' Int YB') (YA Int YB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   161
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   162
qed "extending_Int";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   163
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   164
Goalw [extending_def]
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   165
     "[| extending C h F X' YA' YA;  extending C h F X' YB' YB |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   166
\     ==> extending C h F X' (YA' Un YB') (YA Un YB)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   167
by (Blast_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   168
qed "extending_Un";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   169
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   170
(*This is the right way to handle the X' argument.  Having (INT i:I. X' i)
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   171
  would strengthen the premise.*)
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   172
val [prem] = Goalw [extending_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   173
     "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   174
\     ==> extending C h F X' (INT i:I. Y' i) (INT i:I. Y i)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   175
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   176
qed "extending_INT";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   177
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   178
val [prem] = Goalw [extending_def]
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   179
     "[| !!i. i:I ==> extending C h F X' (Y' i) (Y i) |] \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   180
\     ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   181
by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   182
qed "extending_UN";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   183
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   184
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   185
     "[| extending C h F X' Y' Y;  U'<= X';  Y'<=V';  V<=Y |] \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   186
\     ==> extending C h F U' V' V";
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
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   209
Goal "extending C h F X' UNIV Y";
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]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   214
     "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
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]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   219
     "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
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]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   224
     "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
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
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   228
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   229
(*** Diff, needed for localTo ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   230
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   231
(*Opposite direction fails because Diff in the extended state may remove
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   232
  fewer actions, i.e. those that affect other state variables.*)
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   233
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   234
Goal "Diff (project C h G) (project_act C h `` acts) <= \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   235
\         project C h (Diff G acts)";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   236
by (auto_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def,
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   237
					    UN_subset_iff]));
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   238
qed "Diff_project_project_component_project_Diff";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   239
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   240
Goal "(UN act:acts. Domain act) <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   241
\     ==> Diff (project C h G) acts <= \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   242
\         project C h (Diff G (extend_act h `` acts))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   243
by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   244
					   UN_subset_iff]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   245
by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   246
	       simpset() addsimps [image_image_eq_UN]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   247
qed "Diff_project_component_project_Diff";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   248
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   249
Goal
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   250
   "[| (UN act:acts. Domain act) <= project_set h C; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   251
\      Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   252
\   ==> Diff (project C h G) acts : A co B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   253
by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   254
by (rtac (project_constrains RS iffD2) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   255
by (ftac constrains_imp_subset 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   256
by (Asm_full_simp_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   257
by (blast_tac (claset() addIs [constrains_weaken]) 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   258
qed "Diff_project_constrains";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   259
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   260
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   261
     "[| (UN act:acts. Domain act) <= project_set h C; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   262
\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   263
\     ==> Diff (project C h G) acts : stable A";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   264
by (etac Diff_project_constrains 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   265
by (assume_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   266
qed "Diff_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   267
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   268
(*Converse fails: even if the conclusion holds, H could modify (v o f) 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   269
  simultaneously with other variables, and this action would not be 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   270
  superseded by anything in (extend h G) *)
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   271
Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   272
\     ==> project C h H : func localTo G";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   273
by (asm_full_simp_tac 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   274
    (simpset() addsimps [localTo_def, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   275
			 project_extend_Join RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   276
			 subset_UNIV RS subset_trans RS Diff_project_stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   277
			 Collect_eq_extend_set RS sym]) 1);
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   278
qed "project_localTo_lemma";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   279
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   280
Goal "extend h F Join G : (v o f) localTo extend h H \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   281
\     ==> F Join project UNIV h G : v localTo H";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   282
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   283
by (asm_simp_tac 
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   284
    (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   285
qed "project_localTo_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   286
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   287
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   288
     "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   289
by (blast_tac (claset() addIs [project_localTo_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   290
qed "projecting_localTo";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   291
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   292
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   293
(** Reachability and project **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   294
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   295
Goal "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   296
\        z : reachable (extend h F Join G) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   297
\     ==> f z : reachable (F Join project C h G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   298
by (etac reachable.induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   299
by (force_tac (claset() addIs [reachable.Init, project_set_I],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   300
	       simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   301
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   302
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   303
	       simpset()) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   304
by (res_inst_tac [("act","x")] reachable.Acts 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   305
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   306
by (etac extend_act_D 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   307
qed "reachable_imp_reachable_project";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   308
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   309
(*The extra generality in the first premise allows guarantees with STRONG
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   310
  preconditions (localTo) and WEAK postconditions.*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   311
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   312
     "[| reachable (extend h F Join G) <= C;    \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   313
\        F Join project C h G : A Co B |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   314
\     ==> 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
   315
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   316
by (Clarify_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   317
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   318
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   319
qed "project_Constrains_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   320
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   321
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   322
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   323
\        F Join project C h G : Stable A |]   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   324
\     ==> extend h F Join G : Stable (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   325
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   326
qed "project_Stable_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   327
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   328
Goalw [Always_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   329
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   330
\        F Join project C h G : Always A |]   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   331
\     ==> extend h F Join G : Always (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   332
by (force_tac (claset() addIs [reachable.Init, project_set_I],
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   333
               simpset() addsimps [project_Stable_D]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   334
qed "project_Always_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   335
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   336
Goalw [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   337
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   338
\        F Join project C h G : Increasing func |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   339
\     ==> extend h F Join G : Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   340
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   341
by (stac Collect_eq_extend_set 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   342
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   343
qed "project_Increasing_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   344
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   345
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   346
(** Converse results for weak safety: benefits of the argument C *)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   347
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   348
Goal "[| C <= reachable(extend h F Join G);   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   349
\        x : reachable (F Join project C h G) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   350
\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   351
by (etac reachable.induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   352
by (ALLGOALS Asm_full_simp_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   353
(*SLOW: 6.7s*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   354
by (force_tac (claset() delrules [Id_in_Acts]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   355
		        addIs [reachable.Acts, extend_act_D],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   356
	       simpset() addsimps [project_act_def]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   357
by (force_tac (claset() addIs [reachable.Init],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   358
	       simpset() addsimps [project_set_def]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   359
qed "reachable_project_imp_reachable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   360
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   361
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   362
Goal "project_set h (reachable (extend h F Join G)) = \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   363
\     reachable (F Join project (reachable (extend h F Join G)) h G)";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   364
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
   365
			      subset_refl RS reachable_project_imp_reachable], 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   366
	      simpset() addsimps [project_set_def]));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   367
qed "project_set_reachable_extend_eq";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   368
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   369
(*Perhaps should replace C by reachable...*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   370
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   371
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   372
\        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
   373
\     ==> F Join project C h G : A Co B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   374
by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   375
				       extend_set_Int_distrib]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   376
by (rtac conjI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   377
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   378
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   379
by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   380
(*Some generalization of constrains_weaken_L would be better, but what is it?*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   381
by (rewtac constrains_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   382
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   383
by (thin_tac "ALL act : Acts G. ?P act" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   384
by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   385
	       simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   386
qed "project_Constrains_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   387
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   388
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   389
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   390
\        extend h F Join G : Stable (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   391
\     ==> F Join project C h G : Stable A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   392
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   393
qed "project_Stable_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   394
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   395
Goalw [Always_def]
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   396
     "[| C <= reachable (extend h F Join G);  \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   397
\        extend h F Join G : Always (extend_set h A) |]   \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   398
\     ==> F Join project C h G : Always A";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   399
by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   400
by (rewrite_goals_tac [project_set_def, extend_set_def]);
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   401
by (Blast_tac 1);
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   402
qed "project_Always_I";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   403
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   404
Goalw [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   405
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   406
\        extend h F Join G : Increasing (func o f) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   407
\     ==> F Join project C h G : Increasing func";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   408
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   409
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   410
				      project_Stable_I]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   411
qed "project_Increasing_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   412
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   413
Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   414
\     (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
   415
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   416
qed "project_Constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   417
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   418
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   419
     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   420
\     (extend h F Join G : Stable (extend_set h A))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   421
by (rtac project_Constrains 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   422
qed "project_Stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   423
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   424
Goal
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   425
   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   426
\   (extend h F Join G : Increasing (func o f))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   427
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   428
				      Collect_eq_extend_set RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   429
qed "project_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   430
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   431
(** A lot of redundant theorems: all are proved to facilitate reasoning
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   432
    about guarantees. **)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   433
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   434
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   435
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   436
\                (extend_set h A Co extend_set h B) (A Co B)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   437
by (blast_tac (claset() addIs [project_Constrains_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   438
qed "projecting_Constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   439
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   440
Goalw [Stable_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   441
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   442
\                (Stable (extend_set h A)) (Stable A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   443
by (rtac projecting_Constrains 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   444
qed "projecting_Stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   445
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   446
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   447
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   448
\                (Always (extend_set h A)) (Always A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   449
by (blast_tac (claset() addIs [project_Always_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   450
qed "projecting_Always";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   451
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   452
Goalw [projecting_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   453
     "projecting (%G. reachable (extend h F Join G)) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   454
\                (Increasing (func o f)) (Increasing func)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   455
by (blast_tac (claset() addIs [project_Increasing_I]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   456
qed "projecting_Increasing";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   457
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   458
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   459
     "extending (%G. reachable (extend h F Join G)) h F X' \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   460
\               (extend_set h A Co extend_set h B) (A Co B)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   461
by (blast_tac (claset() addIs [project_Constrains_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   462
qed "extending_Constrains";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   463
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   464
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   465
     "extending (%G. reachable (extend h F Join G)) h F X' \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   466
\               (Stable (extend_set h A)) (Stable A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   467
by (blast_tac (claset() addIs [project_Stable_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   468
qed "extending_Stable";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   469
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   470
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   471
     "extending (%G. reachable (extend h F Join G)) h F X' \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   472
\               (Always (extend_set h A)) (Always A)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   473
by (blast_tac (claset() addIs [project_Always_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   474
qed "extending_Always";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   475
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   476
val [prem] = 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   477
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   478
     "(!!G. reachable (extend h F Join G) <= C G)  \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   479
\     ==> extending C h F X' \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   480
\                   (Increasing (func o f)) (Increasing func)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   481
by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   482
qed "extending_Increasing";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   483
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   484
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   485
(** Progress includes safety in the definition of ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   486
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   487
(*** Progress for (project C h F) ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   488
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   489
(** transient **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   490
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   491
(*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
   492
  transient one.  Could have C=UNIV of course*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   493
Goalw [transient_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   494
     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   495
\                      Domain act <= C;    \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   496
\        F : transient (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   497
\     ==> project C h F : transient A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   498
by (auto_tac (claset() delrules [ballE],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   499
              simpset() addsimps [Domain_project_act, Int_absorb2]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   500
by (REPEAT (ball_tac 1));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   501
by (auto_tac (claset(),
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   502
              simpset() addsimps [extend_set_def, project_set_def, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   503
				  project_act_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   504
by (ALLGOALS Blast_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   505
qed "transient_extend_set_imp_project_transient";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   506
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   507
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   508
(*UNUSED.  WHY??
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   509
  Converse of the above...it requires a strong assumption about actions
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   510
  being enabled for all possible values of the new variables.*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   511
Goalw [transient_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   512
     "[| project C h F : transient A;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   513
\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   514
\                         Domain act <= C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   515
\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   516
\     ==> F : transient (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   517
by (auto_tac (claset() delrules [ballE],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   518
	      simpset() addsimps [Domain_project_act]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   519
by (ball_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   520
by (rtac bexI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   521
by (assume_tac 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   522
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   523
by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   524
by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   525
(*The Domain requirement's proved; must prove the Image requirement*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   526
by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   527
by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   528
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   529
by (thin_tac "A <= ?B" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   530
by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   531
qed "project_transient_imp_transient_extend_set";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   532
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   533
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   534
(** ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   535
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   536
(*For simplicity, the complicated condition on C is eliminated
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   537
  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   538
Goal "F : (extend_set h A) ensures (extend_set h B) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   539
\     ==> project UNIV h F : A ensures B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   540
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   541
    (simpset() addsimps [ensures_def, project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   542
			 transient_extend_set_imp_project_transient,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   543
			 extend_set_Un_distrib RS sym, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   544
			 extend_set_Diff_distrib RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   545
by (Blast_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   546
qed "ensures_extend_set_imp_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   547
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   548
(*A strong condition: F can do anything that project G can.*)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   549
Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   550
\        extend h F Join G : stable C;  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   551
\        F Join project C h G : A ensures B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   552
\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   553
by (case_tac "A <= B" 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   554
by (blast_tac (claset() addIs [subset_imp_ensures] addDs [extend_set_mono]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   555
by (full_simp_tac (simpset() addsimps [ensures_def, Join_constrains,
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   556
				       Join_stable, Join_transient]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   557
by (REPEAT_FIRST (rtac conjI));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   558
by (blast_tac (claset() addDs [extend_transient RS iffD2] 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   559
                        addIs [transient_strengthen]) 3);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   560
by (REPEAT (force_tac (claset() addIs [project_unless RS unlessD, unlessI, 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   561
				       project_extend_constrains_I], 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   562
		       simpset()) 1));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   563
qed_spec_mp "Join_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   564
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   565
Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   566
\        extend h F Join G : stable C;  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   567
\        F Join project C h G : A leadsTo B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   568
\     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   569
by (etac leadsTo_induct 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   570
by (asm_simp_tac (simpset() delsimps UN_simps
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   571
		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   572
by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   573
			       leadsTo_Trans]) 2);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   574
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   575
qed "project_leadsTo_lemma";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   576
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   577
(*Instance of the previous theorem for STRONG progress*)
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   578
Goal "[| ALL D. project UNIV h G : transient D --> F : transient D;  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   579
\        F Join project UNIV h G : A leadsTo B |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   580
\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   581
by (dtac project_leadsTo_lemma 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   582
by Auto_tac;
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   583
qed "project_UNIV_leadsTo_lemma";
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   584
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   585
(** Towards the analogous theorem for WEAK progress*)
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   586
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   587
Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   588
\        extend h F Join G : stable C;  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   589
\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   590
\     ==> extend h F Join G : 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
   591
by (etac leadsTo_induct 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   592
by (asm_simp_tac (simpset() delsimps UN_simps
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   593
		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   594
by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   595
			       leadsTo_Trans]) 2);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   596
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
   597
val lemma = result();
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   598
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   599
Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   600
\        extend h F Join G : stable C;  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   601
\        F Join project C h G : (project_set h C Int A) leadsTo B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   602
\     ==> 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
   603
by (rtac (lemma RS leadsTo_weaken) 1);
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   604
by (auto_tac (claset() addIs [project_set_I], simpset()));
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   605
val lemma2 = result();
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   606
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   607
Goal "[| C = (reachable (extend h F Join G)); \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   608
\        ALL D. project C h G : transient D --> F : transient D;  \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   609
\        F Join project C h G : A LeadsTo B |] \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   610
\     ==> 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
   611
by (asm_full_simp_tac 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   612
    (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, 
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   613
			 project_set_reachable_extend_eq]) 1);
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   614
qed "Join_project_LeadsTo";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   615
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   616
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   617
(*** GUARANTEES and EXTEND ***)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   618
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   619
(** Strong precondition and postcondition; doesn't seem very useful. **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   620
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   621
Goal "F : X guarantees Y ==> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   622
\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   623
by (rtac guaranteesI 1);
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
by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   626
			       guaranteesD]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   627
qed "guarantees_imp_extend_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   628
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   629
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   630
\    ==> F : X guarantees Y";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   631
by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   632
by (dres_inst_tac [("x", "extend h G")] spec 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   633
by (asm_full_simp_tac 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   634
    (simpset() delsimps [extend_Join] 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   635
           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   636
qed "extend_guarantees_imp_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   637
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   638
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   639
\    (F : X guarantees Y)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   640
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   641
			       extend_guarantees_imp_guarantees]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   642
qed "extend_guarantees_eq";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   643
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   644
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   645
(*Weak precondition and postcondition; this is the good one!
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   646
  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
   647
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   648
(*The raw version*)
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   649
val [xguary,project,extend] =
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   650
Goal "[| F : X guarantees Y;  \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   651
\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   652
\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   653
\                Disjoint (extend h F) G |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   654
\             ==> extend h F Join G : Y' |] \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   655
\     ==> extend h F : X' guarantees Y'";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   656
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   657
by (etac project 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   658
by (assume_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   659
by (assume_tac 1);
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   660
qed "project_guarantees_lemma";
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   661
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   662
Goal "[| F : X guarantees Y;  \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   663
\        projecting C h F X' X;  extending C h F X' Y' Y |] \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   664
\     ==> extend h F : X' guarantees Y'";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   665
by (rtac guaranteesI 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   666
by (auto_tac (claset(), 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   667
        simpset() addsimps [guaranteesD, projecting_def, extending_def]));
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   668
qed "project_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   669
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   670
(*It seems that neither "guarantees" law can be proved from the other.*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   671
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   672
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   673
(*** guarantees corollaries ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   674
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   675
(** Most could be deleted: the required versions are easy to prove **)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   676
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   677
Goal "F : UNIV guarantees increasing func \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   678
\     ==> extend h F : X' guarantees increasing (func o f)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   679
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   680
by (rtac extending_increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   681
by (rtac projecting_UNIV 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   682
qed "extend_guar_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   683
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   684
Goal "F : UNIV guarantees Increasing func \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   685
\     ==> extend h F : X' guarantees Increasing (func o f)";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   686
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   687
by (rtac extending_Increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   688
by (rtac projecting_UNIV 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   689
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   690
qed "extend_guar_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   691
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   692
Goal "F : (v localTo G) guarantees increasing func  \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   693
\     ==> extend h F : (v o f) localTo (extend h G)  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   694
\                      guarantees increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   695
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   696
by (rtac extending_increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   697
by (rtac projecting_localTo 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   698
qed "extend_localTo_guar_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   699
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   700
Goal "F : (v localTo G) guarantees Increasing func  \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   701
\     ==> extend h F : (v o f) localTo (extend h G)  \
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   702
\                      guarantees Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   703
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   704
by (rtac extending_Increasing 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   705
by (rtac projecting_localTo 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   706
by Auto_tac;
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   707
qed "extend_localTo_guar_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   708
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   709
Goal "F : Always A guarantees Always B \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   710
\ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   711
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   712
by (rtac extending_Always 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   713
by (rtac projecting_Always 1);
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   714
qed "extend_guar_Always";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   715
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   716
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   717
(** Guarantees with a leadsTo postcondition **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   718
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   719
(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   720
Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   721
\     ==> F : transient D";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   722
by (case_tac "D={}" 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   723
by (auto_tac (claset() addIs [transient_strengthen], simpset()));
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   724
qed "transient_lemma";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   725
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   726
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   727
(*Previously tried to prove
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   728
[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   729
but it can fail if C removes some parts of an action of G.*)
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   730
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   731
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   732
Goal "[| G : f localTo extend h F; \
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   733
\        Disjoint (extend h F) G |] ==> project C h G : stable {x}";
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   734
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   735
    (simpset() addsimps [localTo_imp_stable,
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   736
			 extend_set_sing, project_stable_I]) 1);
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   737
qed "localTo_imp_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   738
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   739
Goal "F : stable{s} ==> F ~: transient {s}";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   740
by (auto_tac (claset(), 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   741
	      simpset() addsimps [FP_def, transient_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   742
				  stable_def, constrains_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   743
qed "stable_sing_imp_not_transient";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   744
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   745
by (auto_tac (claset(), 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   746
	      simpset() addsimps [FP_def, transient_def,
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   747
				  stable_def, constrains_def]));
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   748
qed "stable_sing_imp_not_transient";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   749
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   750
Goal "[| F Join project UNIV h G : A leadsTo B;    \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   751
\        G : f localTo extend h F; \
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   752
\        Disjoint (extend h F) G |]  \
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   753
\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   754
by (rtac project_UNIV_leadsTo_lemma 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   755
by (Clarify_tac 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   756
by (rtac transient_lemma 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   757
by (auto_tac (claset(), 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   758
	      simpset() addsimps [localTo_imp_project_stable, 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   759
				  stable_sing_imp_not_transient]));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   760
qed "project_leadsTo_D";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   761
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   762
Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   763
\         G : f localTo extend h F; \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   764
\         Disjoint (extend h F) G |]  \
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   765
\      ==> 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
   766
by (rtac (refl RS Join_project_LeadsTo) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   767
by (Clarify_tac 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   768
by (rtac transient_lemma 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   769
by (auto_tac (claset(), 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   770
	      simpset() addsimps [localTo_imp_project_stable, 
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   771
				  stable_sing_imp_not_transient]));
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   772
qed "project_LeadsTo_D";
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   773
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   774
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   775
     "extending (%G. UNIV) h F \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   776
\                (f localTo extend h F) \
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   777
\                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   778
by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   779
			addIs [project_leadsTo_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   780
qed "extending_leadsTo";
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   781
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   782
Goalw [extending_def]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   783
     "extending (%G. reachable (extend h F Join G)) h F \
7841
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   784
\               (f localTo extend h F) \
65d91d13fc13 working snapshot; more steps in Alloc
paulson
parents: 7826
diff changeset
   785
\               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   786
by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   787
			addIs [project_LeadsTo_D]) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   788
qed "extending_LeadsTo";
7689
affe0c2fdfbf working snapshot (even Alloc)
paulson
parents: 7660
diff changeset
   789
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   790
(*STRONG precondition and postcondition*)
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   791
Goal "F : (A co A') guarantees (B leadsTo B')  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   792
\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   793
\                   Int (f localTo (extend h F)) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   794
\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   795
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   796
by (rtac (extending_leadsTo RS extending_weaken) 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   797
by (rtac (projecting_constrains RS projecting_weaken) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   798
by Auto_tac;
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   799
qed "extend_co_guar_leadsTo";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   800
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   801
(*WEAK precondition and postcondition*)
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   802
Goal "F : (A Co A') guarantees (B LeadsTo B')  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   803
\ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   804
\                   Int (f localTo (extend h F)) \
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   805
\                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   806
by (etac project_guarantees 1);
7826
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   807
by (rtac (extending_LeadsTo RS extending_weaken) 2);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   808
by (rtac (projecting_Constrains RS projecting_weaken) 1);
c6a8b73b6c2a working shapshot with "projecting" and "extending"
paulson
parents: 7689
diff changeset
   809
by Auto_tac;
7660
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   810
qed "extend_Co_guar_LeadsTo";
7e38237edfcb now with (weak safety) guarantees (weak progress) with Extend
paulson
parents: 7630
diff changeset
   811
7630
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   812
Close_locale "Extend";