src/HOL/UNITY/Project.ML
author paulson
Wed, 29 Sep 1999 13:13:06 +0200
changeset 7630 d0e4a6f1f05c
child 7660 7e38237edfcb
permissions -rw-r--r--
working snapshot with new theory "Project"
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
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    13
Goalw [restr_def] "Init (restr C h F) = Init F";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    14
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    15
qed "Init_restr";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    16
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    17
Goalw [restr_act_def, extend_act_def, project_act_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    18
     "((x,x') : restr_act C h act) = ((x,x') : act & (EX y. h(x,y) : C))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    19
by (Blast_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    20
qed "restr_act_iff";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    21
Addsimps [restr_act_iff];
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    22
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    23
Goal "Acts (restr C h F) = insert Id (restr_act C h `` Acts F)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    24
by (auto_tac (claset(), 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    25
	      simpset() addsimps [restr_def, symmetric restr_act_def, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    26
				  image_image_eq_UN]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    27
qed "Acts_restr";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    28
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    29
Addsimps [Init_restr, Acts_restr];
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    30
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    31
(*The definitions are RE-ORIENTED*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    32
Addsimps [symmetric restr_act_def, symmetric restr_def];
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    33
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    34
Goal "project C h ((extend h F) Join G) = (restr C h F) Join (project C h G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    35
by (rtac program_equalityI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    36
by (asm_simp_tac (simpset() addsimps [symmetric restr_act_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    37
				      image_Un, image_image]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    38
by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    39
qed "project_extend_Join_restr";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    40
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    41
Goalw [project_set_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    42
 "Domain act <= project_set h C ==> restr_act C h act = act";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    43
by (Force_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    44
qed "restr_act_ident";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    45
Addsimps [restr_act_ident];
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    46
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    47
Goal "F : A co B ==> restr C h F : A co B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    48
by (auto_tac (claset(), simpset() addsimps [constrains_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    49
by (Blast_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    50
qed "restr_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    51
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    52
Goal "F : stable A ==> restr C h F : stable A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    53
by (asm_full_simp_tac (simpset() addsimps [stable_def, restr_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    54
qed "restr_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    55
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    56
Goal "UNIV <= project_set h C ==> restr C h F = F";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    57
by (rtac program_equalityI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    58
by (force_tac (claset(),
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    59
	       simpset() addsimps [image_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    60
                   subset_UNIV RS subset_trans RS restr_act_ident]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    61
by (Simp_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    62
qed "restr_ident";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    63
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    64
(*Ideally, uses of this should be eliminated.  But often we see it re-oriented
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    65
  as project_extend_Join RS sym*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    66
Goal "UNIV <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    67
\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    68
by (asm_simp_tac (simpset() addsimps [project_extend_Join_restr, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    69
				      restr_ident]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    70
qed "project_extend_Join";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    71
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    72
Goal "UNIV <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    73
\     ==> (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
    74
by (dres_inst_tac [("f", "project C h")] arg_cong 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    75
by (asm_full_simp_tac (simpset() addsimps [project_extend_Join_restr, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    76
					   restr_ident]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    77
qed "extend_Join_eq_extend_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    78
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    79
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    80
(** Safety **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    81
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    82
Goalw [constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    83
     "(project C h F : A co B)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    84
\     (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
    85
by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    86
by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    87
(*the <== direction*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    88
by (rewtac project_act_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    89
by (force_tac (claset() addSDs [subsetD], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    90
qed "project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    91
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
     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    94
by (simp_tac (simpset() addsimps [project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    95
qed "project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    96
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    97
(*This form's useful with guarantees reasoning*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    98
Goal "(F Join project C h G : A co B)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
    99
\       (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
   100
\        F : A co B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   101
by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   102
by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   103
                        addDs [constrains_imp_subset]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   104
qed "Join_project_constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   105
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   106
(*The condition is required to prove the left-to-right direction;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   107
  could weaken it to G : (C Int extend_set h A) co C*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   108
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   109
     "extend h F Join G : stable C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   110
\     ==> (F Join project C h G : stable A)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   111
\         (extend h F Join G : stable (C Int extend_set h A) &  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   112
\          F : stable A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   113
by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   114
by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   115
qed "Join_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   116
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   117
Goal "(F Join project UNIV h G : increasing func)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   118
\     (extend h F Join G : increasing (func o f))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   119
by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   120
by (auto_tac (claset(),
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   121
	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   122
				  extend_stable RS iffD1]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   123
qed "Join_project_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   124
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   125
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   126
(*** Diff, needed for localTo ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   127
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   128
(*Opposite direction fails because Diff in the extended state may remove
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   129
  fewer actions, i.e. those that affect other state variables.*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   130
Goal "(UN act:acts. Domain act) <= project_set h C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   131
\     ==> Diff (project C h G) acts <= \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   132
\         project C h (Diff G (extend_act h `` acts))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   133
by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   134
					   UN_subset_iff]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   135
by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   136
	       simpset() addsimps [image_image_eq_UN]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   137
qed "Diff_project_component_project_Diff";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   138
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   139
Goal
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   140
   "[| (UN act:acts. Domain act) <= project_set h C; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   141
\      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
   142
\   ==> Diff (project C h G) acts : A co B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   143
by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   144
by (rtac (project_constrains RS iffD2) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   145
by (ftac constrains_imp_subset 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   146
by (Asm_full_simp_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   147
by (blast_tac (claset() addIs [constrains_weaken]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   148
qed "Diff_project_co";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   149
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   150
Goalw [stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   151
     "[| (UN act:acts. Domain act) <= project_set h C; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   152
\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   153
\     ==> Diff (project C h G) acts : stable A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   154
by (etac Diff_project_co 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   155
by (assume_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   156
qed "Diff_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   157
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   158
(*Converse appears to fail*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   159
Goal "[| UNIV <= project_set h C;  (H : (func o f) localTo extend h G) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   160
\     ==> (project C h H : func localTo G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   161
by (asm_full_simp_tac 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   162
    (simpset() addsimps [localTo_def, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   163
			 project_extend_Join RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   164
			 subset_UNIV RS subset_trans RS Diff_project_stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   165
			 Collect_eq_extend_set RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   166
qed "project_localTo_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   167
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   168
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   169
(** Reachability and project **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   170
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   171
Goal "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   172
\        z : reachable (extend h F Join G) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   173
\     ==> f z : reachable (F Join project C h G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   174
by (etac reachable.induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   175
by (force_tac (claset() addIs [reachable.Init, project_set_I],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   176
	       simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   177
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   178
by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   179
	       simpset()) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   180
by (res_inst_tac [("act","x")] reachable.Acts 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   181
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   182
by (etac extend_act_D 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   183
qed "reachable_imp_reachable_project";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   184
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   185
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   186
     "[| reachable (extend h F Join G) <= C;    \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   187
\        F Join project C h G : A Co B |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   188
\     ==> 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
   189
by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   190
by (Clarify_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   191
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   192
by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   193
qed "project_Constrains_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   194
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   195
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   196
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   197
\        F Join project C h G : Stable A |]   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   198
\     ==> extend h F Join G : Stable (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   199
by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   200
qed "project_Stable_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   201
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   202
Goalw [Always_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   203
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   204
\        F Join project C h G : Always A |]   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   205
\     ==> extend h F Join G : Always (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   206
by (force_tac (claset() addIs [reachable.Init, project_set_I],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   207
	       simpset() addsimps [project_Stable_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   208
qed "project_Always_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   209
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   210
Goalw [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   211
     "[| reachable (extend h F Join G) <= C;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   212
\        F Join project C h G : Increasing func |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   213
\     ==> extend h F Join G : Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   214
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   215
by (stac Collect_eq_extend_set 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   216
by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   217
qed "project_Increasing_D";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   218
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   219
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   220
(** Converse results for weak safety: benefits of the argument C *)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   221
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   222
Goal "[| C <= reachable(extend h F Join G);   \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   223
\        x : reachable (F Join project C h G) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   224
\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   225
by (etac reachable.induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   226
by (ALLGOALS Asm_full_simp_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   227
(*SLOW: 6.7s*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   228
by (force_tac (claset() delrules [Id_in_Acts]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   229
		        addIs [reachable.Acts, extend_act_D],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   230
	       simpset() addsimps [project_act_def]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   231
by (force_tac (claset() addIs [reachable.Init],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   232
	       simpset() addsimps [project_set_def]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   233
qed "reachable_project_imp_reachable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   234
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   235
Goalw [Constrains_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   236
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   237
\        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
   238
\     ==> F Join project C h G : A Co B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   239
by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   240
				       extend_set_Int_distrib]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   241
by (rtac conjI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   242
by (etac constrains_weaken 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   243
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   244
by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   245
(*Some generalization of constrains_weaken_L would be better, but what is it?*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   246
by (rewtac constrains_def);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   247
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   248
by (thin_tac "ALL act : Acts G. ?P act" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   249
by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   250
	       simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   251
qed "project_Constrains_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   252
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   253
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   254
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   255
\        extend h F Join G : Stable (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   256
\     ==> F Join project C h G : Stable A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   257
by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   258
qed "project_Stable_I";
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 [Increasing_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   261
     "[| C <= reachable (extend h F Join G);  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   262
\        extend h F Join G : Increasing (func o f) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   263
\     ==> F Join project C h G : Increasing func";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   264
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   265
by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   266
				      project_Stable_I]) 1); 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   267
qed "project_Increasing_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   268
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   269
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
   270
\     (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
   271
by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   272
qed "project_Constrains";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   273
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   274
Goalw [Stable_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   275
     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   276
\     (extend h F Join G : Stable (extend_set h A))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   277
by (rtac project_Constrains 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   278
qed "project_Stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   279
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   280
Goal
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   281
   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   282
\   (extend h F Join G : Increasing (func o f))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   283
by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   284
				      Collect_eq_extend_set RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   285
qed "project_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   286
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   287
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   288
(** Progress includes safety in the definition of ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   289
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   290
(*** Progress for (project C h F) ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   291
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   292
(** transient **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   293
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   294
(*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
   295
  transient one.  Could have C=UNIV of course*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   296
Goalw [transient_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   297
     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   298
\                      Domain act <= C;    \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   299
\        F : transient (extend_set h A) |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   300
\     ==> project C h F : transient A";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   301
by (auto_tac (claset() delrules [ballE],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   302
              simpset() addsimps [Domain_project_act, Int_absorb2]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   303
by (REPEAT (ball_tac 1));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   304
by (auto_tac (claset(),
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   305
              simpset() addsimps [extend_set_def, project_set_def, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   306
				  project_act_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   307
by (ALLGOALS Blast_tac);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   308
qed "transient_extend_set_imp_project_transient";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   309
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   310
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   311
(*UNUSED.  WHY??
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   312
  Converse of the above...it requires a strong assumption about actions
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   313
  being enabled for all possible values of the new variables.*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   314
Goalw [transient_def]
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   315
     "[| project C h F : transient A;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   316
\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   317
\                         Domain act <= C \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   318
\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   319
\     ==> F : transient (extend_set h A)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   320
by (auto_tac (claset() delrules [ballE],
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   321
	      simpset() addsimps [Domain_project_act]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   322
by (ball_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   323
by (rtac bexI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   324
by (assume_tac 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   325
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   326
by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   327
by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   328
(*The Domain requirement's proved; must prove the Image requirement*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   329
by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   330
by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   331
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   332
by (thin_tac "A <= ?B" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   333
by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   334
qed "project_transient_imp_transient_extend_set";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   335
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   336
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   337
(** ensures **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   338
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   339
(*For simplicity, the complicated condition on C is eliminated
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   340
  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   341
Goal "F : (extend_set h A) ensures (extend_set h B) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   342
\     ==> project UNIV h F : A ensures B";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   343
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   344
    (simpset() addsimps [ensures_def, project_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   345
			 transient_extend_set_imp_project_transient,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   346
			 extend_set_Un_distrib RS sym, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   347
			 extend_set_Diff_distrib RS sym]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   348
by (Blast_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   349
qed "ensures_extend_set_imp_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   350
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   351
(*A super-strong condition: G is not allowed to affect the
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   352
  shared variables at all.*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   353
Goal "[| ALL x. project UNIV h G ~: transient {x};  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   354
\        F Join project UNIV h G : A ensures B |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   355
\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   356
by (case_tac "A <= B" 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   357
by (etac (extend_set_mono RS subset_imp_ensures) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   358
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   359
    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   360
			 extend_set_Un_distrib RS sym, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   361
			 extend_set_Diff_distrib RS sym,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   362
			 Join_transient, Join_constrains,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   363
			 project_constrains, Int_absorb1]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   364
by (blast_tac (claset() addIs [transient_strengthen]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   365
qed_spec_mp "Join_project_ensures";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   366
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   367
Goal "[| ALL x. project UNIV h G ~: transient {x};  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   368
\        F Join project UNIV h G : A leadsTo B |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   369
\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   370
by (etac leadsTo_induct 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   371
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   372
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   373
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   374
qed "Join_project_leadsTo_I";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   375
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   376
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   377
(** Strong precondition and postcondition; doesn't seem very useful. **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   378
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   379
Goal "F : X guarantees Y ==> \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   380
\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   381
by (rtac guaranteesI 1);
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 (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   384
			       guaranteesD]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   385
qed "guarantees_imp_extend_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   386
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   387
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   388
\    ==> F : X guarantees Y";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   389
by (rtac guaranteesI 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   390
by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   391
by (dtac spec 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   392
by (dtac (mp RS mp) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   393
by (Blast_tac 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   394
by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   395
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   396
qed "extend_guarantees_imp_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   397
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   398
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   399
\    (F : X guarantees Y)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   400
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   401
			       extend_guarantees_imp_guarantees]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   402
qed "extend_guarantees_eq";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   403
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   404
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   405
(*Weak precondition and postcondition; this is the good one!
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   406
  Not clear that it has a converse [or that we want one!]*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   407
val [xguary,project,extend] =
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   408
Goal "[| F : X guarantees Y;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   409
\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   410
\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   411
\                Disjoint (extend h F) G |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   412
\             ==> extend h F Join G : Y' |] \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   413
\     ==> extend h F : X' guarantees Y'";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   414
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   415
by (etac project 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   416
by (assume_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   417
by (assume_tac 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   418
qed "project_guarantees";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   419
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   420
(** It seems that neither "guarantees" law can be proved from the other. **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   421
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   422
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   423
(*** guarantees corollaries ***)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   424
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   425
Goal "F : UNIV guarantees increasing func \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   426
\     ==> extend h F : UNIV guarantees increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   427
by (etac project_guarantees 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   428
by (ALLGOALS
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   429
    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   430
qed "extend_guar_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   431
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   432
Goal "F : UNIV guarantees Increasing func \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   433
\     ==> extend h F : UNIV guarantees Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   434
by (etac project_guarantees 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   435
by (rtac (subset_UNIV RS project_Increasing_D) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   436
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   437
qed "extend_guar_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   438
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   439
Goal "F : (func localTo G) guarantees increasing func  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   440
\     ==> extend h F : (func o f) localTo (extend h G)  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   441
\                      guarantees increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   442
by (etac project_guarantees 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   443
(*the "increasing" guarantee*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   444
by (asm_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   445
    (simpset() addsimps [Join_project_increasing RS sym]) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   446
(*the "localTo" requirement*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   447
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   448
by (asm_simp_tac 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   449
    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   450
qed "extend_localTo_guar_increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   451
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   452
Goal "F : (func localTo G) guarantees Increasing func  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   453
\     ==> extend h F : (func o f) localTo (extend h G)  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   454
\                      guarantees Increasing (func o f)";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   455
by (etac project_guarantees 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   456
(*the "Increasing" guarantee*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   457
by (etac (subset_UNIV RS project_Increasing_D) 2);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   458
(*the "localTo" requirement*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   459
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   460
by (asm_simp_tac 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   461
    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   462
qed "extend_localTo_guar_Increasing";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   463
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   464
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   465
(** Guarantees with a leadsTo postcondition **)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   466
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   467
Goal "[| G : f localTo extend h F; \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   468
\        Disjoint (extend h F) G |] ==> project UNIV h G : stable {x}";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   469
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   470
    (simpset() addsimps [localTo_imp_stable,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   471
			 extend_set_sing, project_stable]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   472
qed "localTo_imp_project_stable";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   473
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   474
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   475
Goal "F : stable{s} ==> F ~: transient {s}";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   476
by (auto_tac (claset(), 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   477
	      simpset() addsimps [FP_def, transient_def,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   478
				  stable_def, constrains_def]));
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   479
qed "stable_sing_imp_not_transient";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   480
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   481
Goal "F : (A co A') guarantees (B leadsTo B')  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   482
\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   483
\                   Int (f localTo (extend h F)) \
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   484
\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   485
by (etac project_guarantees 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   486
(*the safety precondition*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   487
by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   488
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   489
    (simpset() addsimps [project_constrains, Join_constrains, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   490
			 extend_constrains]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   491
by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   492
(*the liveness postcondition*)
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   493
by (rtac Join_project_leadsTo_I 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   494
by Auto_tac;
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   495
by (asm_full_simp_tac
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   496
    (simpset() addsimps [Join_localTo, self_localTo,
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   497
			 localTo_imp_project_stable, 
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   498
			 stable_sing_imp_not_transient]) 1);
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   499
qed "extend_co_guar_leadsTo";
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   500
d0e4a6f1f05c working snapshot with new theory "Project"
paulson
parents:
diff changeset
   501
Close_locale "Extend";