src/HOL/UNITY/Alloc.ML
author paulson
Sun Jun 13 13:57:31 1999 +0200 (1999-06-13)
changeset 6828 ea6832d74353
parent 6815 de4d358bf01e
child 6837 1bd850260747
permissions -rw-r--r--
not working but taking shape
paulson@6828
     1
(*  Title:      HOL/UNITY/Alloc
paulson@6828
     2
    ID:         $Id$
paulson@6828
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6828
     4
    Copyright   1998  University of Cambridge
paulson@6828
     5
paulson@6828
     6
Specification of Chandy and Charpentier's Allocator
paulson@6828
     7
*)
paulson@6828
     8
paulson@6815
     9
Addsimps [sub_def];
paulson@6828
    10
paulson@6828
    11
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    12
by (rtac injI 1);
paulson@6828
    13
by Auto_tac;
paulson@6828
    14
qed "inj_sysOfAlloc";
paulson@6828
    15
paulson@6828
    16
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    17
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    18
\                                allocAsk = allocAsk s,    \
paulson@6828
    19
\                                allocRel = allocRel s |), \
paulson@6828
    20
\                             client s)")] surjI 1);
paulson@6828
    21
by Auto_tac;
paulson@6828
    22
qed "surj_sysOfAlloc";
paulson@6828
    23
paulson@6828
    24
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    25
paulson@6828
    26
paulson@6828
    27
Open_locale "System";
paulson@6828
    28
paulson@6828
    29
val Alloc = thm "Alloc";
paulson@6828
    30
val Client = thm "Client";
paulson@6828
    31
val Network = thm "Network";
paulson@6828
    32
val System_def = thm "System_def";
paulson@6828
    33
paulson@6828
    34
AddIffs [finite_lessThan];
paulson@6828
    35
paulson@6828
    36
(*could move to PPROD.ML, but function "sub" is needed there*)
paulson@6828
    37
Goal "lift_set i {s. P (f s)} = {s. P (f (sub i s))}";
paulson@6828
    38
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@6828
    39
qed "lift_set_sub";
paulson@6828
    40
paulson@6828
    41
(*ONE OF THESE IS REDUNDANT!*)
paulson@6828
    42
Goal "lift_set i {s. P (f s)} = {s. P (f (s i))}";
paulson@6828
    43
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
paulson@6828
    44
qed "lift_set_sub2";
paulson@6828
    45
paulson@6828
    46
Goalw [Increasing_def]
paulson@6828
    47
     "[| i: I;  finite I |]  \
paulson@6828
    48
\     ==> ((PPI x:I. F) : Increasing (f o sub i)) = (F : Increasing f)";
paulson@6828
    49
by (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}" 1);
paulson@6828
    50
by (asm_simp_tac (simpset() addsimps [lift_set_sub]) 2);
paulson@6828
    51
by (asm_full_simp_tac (simpset() addsimps [PFUN_Stable]) 1);
paulson@6828
    52
qed "PFUN_Increasing";
paulson@6828
    53
paulson@6828
    54
(*FUN.ML*)
paulson@6828
    55
(*left-to-right inclusion holds even if I is empty*)
paulson@6828
    56
Goalw [inj_on_def]
paulson@6828
    57
   "[| inj_on f C;  ALL i:I. B i <= C;  j:I |] \
paulson@6828
    58
\   ==> f `` (INT i:I. B i) = (INT i:I. f `` B i)";
paulson@6828
    59
by (Blast_tac 1);
paulson@6828
    60
qed "inj_on_image_INT";
paulson@6828
    61
paulson@6828
    62
paulson@6828
    63
paulson@6828
    64
Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)";
paulson@6828
    65
by (asm_simp_tac 
paulson@6828
    66
    (simpset() addsimps [Increasing_def,
paulson@6828
    67
			 inj_lift_prog RS inj_on_image_INT]) 1);
paulson@6828
    68
auto();
paulson@6828
    69
by (dres_inst_tac [("x","z")] spec 1);
paulson@6828
    70
auto();
paulson@6828
    71
by (asm_simp_tac (simpset() addsimps [lift_set_sub2 RS sym,
paulson@6828
    72
				      lift_prog_Stable_eq]) 1);
paulson@6828
    73
qed "image_lift_prog_Increasing";
paulson@6828
    74
paulson@6828
    75
paulson@6828
    76
Goal "i < Nclients ==> \
paulson@6828
    77
\     lift_prog i Client : range (lift_prog i) guar Increasing (rel o sub i)";
paulson@6828
    78
paulson@6828
    79
paulson@6828
    80
paulson@6828
    81
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@6828
    82
by (cut_facts_tac [Client] 1);
paulson@6828
    83
by (full_simp_tac
paulson@6828
    84
    (simpset() addsimps [System_def,
paulson@6828
    85
			 client_spec_def, client_increasing_def,
paulson@6828
    86
			 guarantees_Int_right]) 1);
paulson@6828
    87
by Auto_tac;
paulson@6828
    88
by (dtac lift_prog_guarantees 1);
paulson@6828
    89
by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
paulson@6828
    90
back();
paulson@6828
    91
by (dtac (lessThan_iff RS iffD2 RS PFUN_Increasing RS iffD2) 1);
paulson@6828
    92
by Auto_tac;
paulson@6828
    93
paulson@6828
    94
paulson@6828
    95
by (full_simp_tac (simpset() addsimps [read_instantiate [("f1","rel"),("I1","lessThan Nclients")] (PFUN_Increasing RS sym)]) 1);
paulson@6828
    96
paulson@6828
    97
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
paulson@6828
    98
paulson@6828
    99
paulson@6828
   100
Goal "System : system_spec";
paulson@6828
   101
paulson@6828
   102
by (full_simp_tac
paulson@6828
   103
    (simpset() addsimps [alloc_spec_def, alloc_safety_def, System_def]) 1);
paulson@6828
   104
paulson@6828
   105
paulson@6828
   106
paulson@6828
   107
paulson@6828
   108
paulson@6828
   109
paulson@6828
   110
(*partial system...*)
paulson@6828
   111
Goal "[| Alloc : alloc_spec;  Network : network_spec |] \
paulson@6828
   112
\     ==> (extend sysOfAlloc Alloc) Join Network : system_spec";
paulson@6828
   113
paulson@6828
   114
(*partial system...*)
paulson@6828
   115
Goal "[| Client : client_spec;  Network : network_spec |] \
paulson@6828
   116
\     ==> (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
paulson@6828
   117
\         Join Network : system_spec";
paulson@6828
   118
paulson@6828
   119
paulson@6828
   120
paulson@6828
   121
Goal "[| Alloc : alloc_spec;  Client : client_spec;  \
paulson@6828
   122
\        Network : network_spec |] \
paulson@6828
   123
\     ==> (extend sysOfAlloc Alloc) \
paulson@6828
   124
\         Join (extend sysOfClient (PPI x: lessThan Nclients. Client)) \
paulson@6828
   125
\         Join Network : system_spec";
paulson@6828
   126
by (full_simp_tac
paulson@6828
   127
    (simpset() addsimps [system_spec_def, system_safety_def]) 1);
paulson@6828
   128
by Auto_tac;
paulson@6828
   129
by (full_simp_tac
paulson@6828
   130
    (simpset() addsimps [client_spec_def, client_increasing_def,
paulson@6828
   131
			 guarantees_Int_right]) 1);
paulson@6828
   132
by Auto_tac;
paulson@6828
   133
by (dtac (UNIV_I RSN (2, guaranteesD)) 1);
paulson@6828
   134
back();
paulson@6828
   135
by (full_simp_tac
paulson@6828
   136
    (simpset() addsimps [network_spec_def, network_rel_def]) 1);
paulson@6828
   137
paulson@6828
   138
by (subgoal_tac "" 1);
paulson@6828
   139
by (full_simp_tac
paulson@6828
   140
    (simpset() addsimps [alloc_spec_def, alloc_safety_def]) 1);
paulson@6828
   141
by Auto_tac;
paulson@6828
   142
paulson@6828
   143
by (Simp_tac 1);
paulson@6828
   144
paulson@6828
   145
paulson@6828
   146
paulson@6828
   147
paulson@6828
   148
(*Generalized version allowing different clients*)
paulson@6828
   149
Goal "[| Alloc : alloc_spec;  \
paulson@6828
   150
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6828
   151
\        Network : network_spec |] \
paulson@6828
   152
\     ==> (extend sysOfAlloc Alloc) \
paulson@6828
   153
\         Join (extend sysOfClient (PPROD (lessThan Nclients) Client)) \
paulson@6828
   154
\         Join Network : system_spec";
paulson@6828
   155