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