src/ZF/UNITY/AllocImpl.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 58860 fee7cfa69c50
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
     1
(*  Title:      ZF/UNITY/AllocImpl.thy
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     3
    Copyright   2002  University of Cambridge
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
     5
Single-client allocator implementation.
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     6
Charpentier and Chandy, section 7 (page 17).
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     7
*)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16183
diff changeset
     9
theory AllocImpl imports ClientImpl begin
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    10
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    11
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    12
  NbR :: i            (*number of consumed messages*)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    13
  "NbR == Var([succ(2)])"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    14
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    15
abbreviation
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    16
  available_tok :: i  (*number of free tokens (T in paper)*)  where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    17
  "available_tok == Var([succ(succ(2))])"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    18
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    19
axiomatization where
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    20
  alloc_type_assumes [simp]:
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    21
  "type_of(NbR) = nat & type_of(available_tok)=nat" and
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    22
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    23
  alloc_default_val_assumes [simp]:
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    24
  "default_val(NbR)  = 0 & default_val(available_tok)=0"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    26
definition
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    27
  "alloc_giv_act ==
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
    28
       {<s, t> \<in> state*state.
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    29
        \<exists>k. k = length(s`giv) &
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    30
            t = s(giv := s`giv @ [nth(k, s`ask)],
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    31
                  available_tok := s`available_tok #- nth(k, s`ask)) &
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
    32
            k < length(s`ask) & nth(k, s`ask) \<le> s`available_tok}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    33
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    34
definition
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    35
  "alloc_rel_act ==
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
    36
       {<s, t> \<in> state*state.
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    37
        t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    38
              NbR := succ(s`NbR)) &
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    39
        s`NbR < length(s`rel)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    40
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    41
definition
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    42
  (*The initial condition s`giv=[] is missing from the
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
    43
    original definition: S. O. Ehmety *)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    44
  "alloc_prog ==
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    45
       mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    46
                  {alloc_giv_act, alloc_rel_act},
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    47
                  \<Union>G \<in> preserves(lift(available_tok)) \<inter>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    48
                        preserves(lift(NbR)) \<inter>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    49
                        preserves(lift(giv)). Acts(G))"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    50
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    51
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    52
lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    53
apply (unfold state_def)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    54
apply (drule_tac a = available_tok in apply_type, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    55
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    56
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    57
lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    58
apply (unfold state_def)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    59
apply (drule_tac a = NbR in apply_type, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    60
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    61
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    62
(** The Alloc Program **)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    63
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    64
lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    65
by (simp add: alloc_prog_def)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    66
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    67
declare alloc_prog_def [THEN def_prg_Init, simp]
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    68
declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
24051
896fb015079c replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents: 16417
diff changeset
    69
declare alloc_prog_def [program]
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    70
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    71
declare  alloc_giv_act_def [THEN def_act_simp, simp]
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    72
declare  alloc_rel_act_def [THEN def_act_simp, simp]
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    73
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    74
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    75
lemma alloc_prog_ok_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
    76
"\<forall>G \<in> program. (alloc_prog ok G) \<longleftrightarrow>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    77
     (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) &
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    78
       G \<in> preserves(lift(NbR)) &  alloc_prog \<in> Allowed(G))"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    79
by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    80
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    81
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    82
lemma alloc_prog_preserves:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    83
    "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    84
apply (rule Inter_var_DiffI, force)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    85
apply (rule ballI)
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15481
diff changeset
    86
apply (rule preservesI, safety)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    87
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    88
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    89
(* As a special case of the rule above *)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    90
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    91
lemma alloc_prog_preserves_rel_ask_tok:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    92
    "alloc_prog \<in>
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    93
       preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    94
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    95
apply (insert alloc_prog_preserves)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    96
apply (drule_tac [3] x = tok in Inter_var_DiffD)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    97
apply (drule_tac [2] x = ask in Inter_var_DiffD)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
    98
apply (drule_tac x = rel in Inter_var_DiffD, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
    99
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   100
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   101
lemma alloc_prog_Allowed:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   102
"Allowed(alloc_prog) =
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   103
  preserves(lift(giv)) \<inter> preserves(lift(available_tok)) \<inter> preserves(lift(NbR))"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   104
apply (cut_tac v="lift(giv)" in preserves_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   105
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   106
                      cons_Int_distrib safety_prop_Acts_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   107
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   108
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   109
(* In particular we have *)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   110
lemma alloc_prog_ok_client_prog: "alloc_prog ok client_prog"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   111
apply (auto simp add: ok_iff_Allowed)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   112
apply (cut_tac alloc_prog_preserves)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   113
apply (cut_tac [2] client_prog_preserves)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   114
apply (auto simp add: alloc_prog_Allowed client_prog_Allowed)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   115
apply (drule_tac [6] B = "preserves (lift (NbR))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   116
apply (drule_tac [5] B = "preserves (lift (available_tok))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   117
apply (drule_tac [4] B = "preserves (lift (giv))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   118
apply (drule_tac [3] B = "preserves (lift (tok))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   119
apply (drule_tac [2] B = "preserves (lift (ask))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   120
apply (drule_tac B = "preserves (lift (rel))" in InterD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   121
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   122
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   123
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   124
(** Safety property: (28) **)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   125
lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
26289
9d2c375e242b avoid unclear fact references;
wenzelm
parents: 24893
diff changeset
   126
apply (auto intro!: increasing_imp_Increasing simp add: guar_def
9d2c375e242b avoid unclear fact references;
wenzelm
parents: 24893
diff changeset
   127
  Increasing.increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   128
apply (auto dest: ActsD)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   129
apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   130
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   131
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   132
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   133
lemma giv_Bounded_lamma1:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   134
"alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   135
                     {s\<in>state. s`available_tok #+ tokens(s`giv) =
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   136
                                 NbT #+ tokens(take(s`NbR, s`rel))})"
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15481
diff changeset
   137
apply safety
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   138
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   139
apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   140
apply (simp (no_asm_simp) add: take_succ)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   141
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   142
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   143
lemma giv_Bounded_lemma2:
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   144
"[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   145
  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   146
   {s\<in>state. s`available_tok #+ tokens(s`giv) =
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   147
    NbT #+ tokens(take(s`NbR, s`rel))})"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   148
apply (cut_tac giv_Bounded_lamma1)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   149
apply (cut_tac alloc_prog_preserves_rel_ask_tok)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   150
apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   151
apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   152
apply (rotate_tac -1)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   153
apply (cut_tac A = "nat * nat * list(nat)"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   154
             and P = "%<m,n,l> y. n \<le> length(y) &
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   155
                                  m #+ tokens(l) = NbT #+ tokens(take(n,y))"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   156
             and g = "lift(rel)" and F = alloc_prog
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   157
       in stable_Join_Stable)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   158
prefer 3 apply assumption
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   159
apply (auto simp add: Collect_conj_eq)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   160
apply (frule_tac g = length in imp_Increasing_comp)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   161
apply (blast intro: mono_length)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   162
apply (auto simp add: refl_prefix)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   163
apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   164
apply assumption
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   165
apply (auto simp add: Le_def length_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   166
apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   167
apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   168
apply assumption+
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   169
apply (force dest: ActsD)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   170
apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   171
apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   172
apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   173
apply (auto simp add: Stable_def Constrains_def constrains_def)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   174
apply (drule bspec, force)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   175
apply (drule subsetD)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   176
apply (rule imageI, assumption)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   177
apply (auto simp add: prefix_take_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   178
apply (rotate_tac -1)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   179
apply (erule ssubst)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   180
apply (auto simp add: take_take min_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   181
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   182
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   183
(*Property (29), page 18:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   184
  the number of tokens in circulation never exceeds NbT*)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   185
lemma alloc_prog_giv_Bounded: "alloc_prog \<in> Incr(lift(rel))
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   186
      guarantees Always({s\<in>state. tokens(s`giv) \<le> NbT #+ tokens(s`rel)})"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   187
apply (cut_tac NbT_pos)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   188
apply (auto simp add: guar_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   189
apply (rule Always_weaken)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   190
apply (rule AlwaysI)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   191
apply (rule_tac [2] giv_Bounded_lemma2, auto)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   192
apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   193
apply (erule subst)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   194
apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   195
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   196
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   197
(*Property (30), page 18: the number of tokens given never exceeds the number
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   198
  asked for*)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   199
lemma alloc_prog_ask_prefix_giv:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   200
     "alloc_prog \<in> Incr(lift(ask)) guarantees
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   201
                   Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   202
apply (auto intro!: AlwaysI simp add: guar_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   203
apply (subgoal_tac "G \<in> preserves (lift (giv))")
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   204
 prefer 2 apply (simp add: alloc_prog_ok_iff)
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   205
apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   206
       in stable_Join_Stable)
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15481
diff changeset
   207
apply safety
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   208
 prefer 2 apply (simp add: lift_def, clarify)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   209
apply (drule_tac a = k in Increasing_imp_Stable, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   210
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   211
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   212
subsection{* Towards proving the liveness property, (31) *}
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   213
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   214
subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*}
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   215
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   216
lemma alloc_prog_transient_lemma:
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   217
     "[|G \<in> program; k\<in>nat|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   218
      ==> alloc_prog \<squnion> G \<in>
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   219
             transient({s\<in>state. k \<le> length(s`rel)} \<inter>
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   220
             {s\<in>state. succ(s`NbR) = k})"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   221
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   222
apply (erule_tac V = "G\<notin>?u" in thin_rl)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   223
apply (rule_tac act = alloc_rel_act in transientI)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   224
apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   225
apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   226
apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   227
apply (rule ReplaceI)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   228
apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   229
                        NbR:=succ (x`NbR))"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   230
       in exI)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   231
apply (auto intro!: state_update_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   232
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   233
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   234
lemma alloc_prog_rel_Stable_NbR_lemma:
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   235
    "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   236
     ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15481
diff changeset
   237
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   238
apply (blast intro: le_trans leI)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   239
apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   240
apply (drule_tac [2] g = succ in imp_increasing_comp)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   241
apply (rule_tac [2] mono_succ)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   242
apply (drule_tac [4] x = k in increasing_imp_stable)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   243
    prefer 5 apply (simp add: Le_def comp_def, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   244
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   245
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   246
lemma alloc_prog_NbR_LeadsTo_lemma:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   247
     "[| G \<in> program; alloc_prog ok G;
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   248
         alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   249
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   250
            {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   251
            LeadsTo {s\<in>state. k \<le> s`NbR}"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   252
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   253
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   254
apply (rule_tac [2] mono_length)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   255
    prefer 3 apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   256
apply (simp_all add: refl_prefix Le_def comp_def length_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   257
apply (rule LeadsTo_weaken)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   258
apply (rule PSP_Stable)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   259
prefer 2 apply assumption
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   260
apply (rule PSP_Stable)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   261
apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   262
apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   263
apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   264
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   265
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   266
lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   267
    "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   268
        k\<in>nat; n \<in> nat; n < k |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   269
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   270
            {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   271
               LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   272
                 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   273
apply (unfold greater_than_def)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   274
apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   275
       in LeadsTo_weaken_R)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   276
apply safe
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   277
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   278
apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   279
apply (rule_tac [2] mono_length)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   280
    prefer 3 apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   281
apply (simp_all add: refl_prefix Le_def comp_def length_type)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14095
diff changeset
   282
apply (subst Int_commute [of _ "{x \<in> state . n < x ` NbR}"])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14095
diff changeset
   283
apply (rule_tac A = "({s \<in> state . k \<le> length (s ` rel) } \<inter>
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14095
diff changeset
   284
                      {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length(s`rel)}"
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 14095
diff changeset
   285
       in LeadsTo_weaken_L)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   286
apply (rule PSP_Stable, safe)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   287
apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   288
apply (rule_tac [2] LeadsTo_weaken)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   289
apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   290
apply simp_all
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   291
apply (rule subset_imp_LeadsTo, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   292
apply (blast intro: lt_trans2)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   293
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   294
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   295
lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   296
by (force simp add: lt_def)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   297
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   298
(* Lemma 49, page 28 *)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   299
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   300
lemma alloc_prog_NbR_LeadsTo_lemma3:
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   301
  "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   302
     k\<in>nat|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   303
   ==> alloc_prog \<squnion> G \<in>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   304
           {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   305
(* Proof by induction over the difference between k and n *)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   306
apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   307
apply (simp_all add: lam_def, auto)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   308
apply (rule single_LeadsTo_I, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   309
apply (simp (no_asm_simp) add: Collect_vimage_eq)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   310
apply (rename_tac "s0")
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   311
apply (case_tac "s0`NbR < k")
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   312
apply (rule_tac [2] subset_imp_LeadsTo, safe)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   313
apply (auto dest!: not_lt_imp_le)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   314
apply (rule LeadsTo_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   315
apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   316
prefer 3 apply assumption
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   317
apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   318
apply (blast dest: lt_asym)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   319
apply (force dest: add_lt_elim2)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   320
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   321
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   322
subsubsection{*Towards proving lemma 50, page 29*}
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   323
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   324
lemma alloc_prog_giv_Ensures_lemma:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   325
"[| G \<in> program; k\<in>nat; alloc_prog ok G;
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   326
  alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   327
  alloc_prog \<squnion> G \<in>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   328
  {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   329
  {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   330
  Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   331
apply (rule EnsuresI, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   332
apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   333
apply (rule_tac [2] act = alloc_giv_act in transientI)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   334
 prefer 2
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   335
 apply (simp add: alloc_prog_def [THEN def_prg_Acts])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   336
 apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   337
apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   338
apply (erule_tac [2] swap)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   339
apply (rule_tac [2] ReplaceI)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   340
apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length(x`giv), x ` ask))" in exI)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   341
apply (auto intro!: state_update_type simp add: app_type)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   342
apply (rule_tac A = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length(s ` ask) } \<inter> {s\<in>state. length(s`giv) =k}" and A' = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<union> {s\<in>state. ~ k < length(s`ask) } \<union> {s\<in>state . length(s ` giv) \<noteq> k}" in Constrains_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   343
apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   344
apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1")
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   345
apply (rule_tac [2] trans)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   346
apply (rule_tac [2] length_app, auto)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   347
apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   348
apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   349
apply assumption+
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   350
apply auto
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   351
apply (drule_tac a = "xa ` ask" and r = "prefix(tokbag)" and A = "list(tokbag)"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   352
       in Increasing_imp_Stable)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   353
apply (auto simp add: prefix_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   354
apply (drule StableD)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   355
apply (auto simp add: Constrains_def constrains_def, force)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   356
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   357
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   358
lemma alloc_prog_giv_Stable_lemma:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   359
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   360
  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15481
diff changeset
   361
apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   362
apply (auto intro: leI)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   363
apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   364
apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   365
apply (drule_tac [2] x = k in increasing_imp_stable)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   366
 prefer 3 apply (simp add: Le_def comp_def)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   367
apply (auto simp add: length_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   368
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   369
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   370
(* Lemma 50, page 29 *)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   371
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   372
lemma alloc_prog_giv_LeadsTo_lemma:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   373
"[| G \<in> program; alloc_prog ok G;
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   374
    alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   375
 ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   376
        {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   377
        {s\<in>state.  k < length(s`ask)} \<inter>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   378
        {s\<in>state. length(s`giv) = k}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   379
        LeadsTo {s\<in>state. k < length(s`giv)}"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   380
apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } \<union> {s\<in>state. length(s`giv) \<noteq> k}")
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   381
prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   382
apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   383
apply (drule PSP_Stable, assumption)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   384
apply (rule LeadsTo_weaken)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   385
apply (rule PSP_Stable)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   386
apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   387
apply (auto simp add: le_iff)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   388
apply (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   389
apply (rule mono_length)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   390
 prefer 2 apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   391
apply (simp_all add: refl_prefix Le_def comp_def length_type)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   392
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   393
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   394
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   395
text{*Lemma 51, page 29.
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   396
  This theorem states as invariant that if the number of
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   397
  tokens given does not exceed the number returned, then the upper limit
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   398
  (@{term NbT}) does not exceed the number currently available.*}
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   399
lemma alloc_prog_Always_lemma:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   400
"[| G \<in> program; alloc_prog ok G;
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   401
    alloc_prog \<squnion> G \<in> Incr(lift(ask));
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   402
    alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   403
  ==> alloc_prog \<squnion> G \<in>
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   404
        Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   405
                NbT \<le> s`available_tok})"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   406
apply (subgoal_tac
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   407
       "alloc_prog \<squnion> G
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   408
          \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   409
                    {s\<in>state. s`available_tok #+ tokens(s`giv) = 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   410
                              NbT #+ tokens(take (s`NbR, s`rel))})")
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   411
apply (rule_tac [2] AlwaysI)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   412
apply (rule_tac [3] giv_Bounded_lemma2, auto)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   413
apply (rule Always_weaken, assumption, auto)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   414
apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   415
 prefer 2 apply (force)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   416
apply (subgoal_tac "x`available_tok =
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   417
                    NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   418
apply (simp add: );
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   419
apply (auto split add: nat_diff_split dest: lt_trans2)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   420
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   421
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   422
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14072
diff changeset
   423
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   424
subsubsection{* Main lemmas towards proving property (31)*}
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   425
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   426
lemma LeadsTo_strength_R:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   427
    "[|  F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo  B"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   428
by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   429
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   430
lemma PSP_StableI:
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   431
"[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   432
   F \<in> A \<inter> C LeadsTo B \<union> (state - C) |] ==> F \<in> A LeadsTo  B"
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   433
apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   434
 prefer 2 apply blast
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   435
apply (rule LeadsTo_Un, assumption)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   436
apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   437
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   438
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   439
lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   440
by auto
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   441
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   442
(*needed?*)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   443
lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   444
by auto
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   445
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   446
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   447
locale alloc_progress =
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   448
 fixes G
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   449
 assumes Gprog [intro,simp]: "G \<in> program"
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   450
     and okG [iff]:          "alloc_prog ok G"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   451
     and Incr_rel [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(rel))"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   452
     and Incr_ask [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(ask))"
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   453
     and safety:   "alloc_prog \<squnion> G
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   454
                      \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   455
     and progress: "alloc_prog \<squnion> G
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   456
                      \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   457
                        {s\<in>state. k \<le> tokens(s`rel)})"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   458
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   459
(*First step in proof of (31) -- the corrected version from Charpentier.
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   460
  This lemma implies that if a client releases some tokens then the Allocator
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   461
  will eventually recognize that they've been released.*)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   462
lemma (in alloc_progress) tokens_take_NbR_lemma:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   463
 "k \<in> tokbag
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   464
  ==> alloc_prog \<squnion> G \<in>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   465
        {s\<in>state. k \<le> tokens(s`rel)}
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   466
        LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   467
apply (rule single_LeadsTo_I, safe)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   468
apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   469
apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   470
apply (rule_tac [8] subset_imp_LeadsTo)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   471
apply (auto intro!: Incr_rel)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   472
apply (rule_tac j = "tokens(take (length(s`rel), x`rel))" in le_trans)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   473
apply (rule_tac j = "tokens(take (length(s`rel), s`rel))" in le_trans)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   474
apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   475
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   476
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   477
(*** Rest of proofs done by lcp ***)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   478
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   479
(*Second step in proof of (31): by LHS of the guarantee and transivity of
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   480
  LeadsTo *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   481
lemma (in alloc_progress) tokens_take_NbR_lemma2:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   482
     "k \<in> tokbag
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   483
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   484
            {s\<in>state. tokens(s`giv) = k}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   485
            LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   486
apply (rule LeadsTo_Trans)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   487
 apply (rule_tac [2] tokens_take_NbR_lemma)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   488
 prefer 2 apply assumption
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   489
apply (insert progress) 
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   490
apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   491
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   492
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   493
(*Third step in proof of (31): by PSP with the fact that giv increases *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   494
lemma (in alloc_progress) length_giv_disj:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   495
     "[| k \<in> tokbag; n \<in> nat |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   496
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   497
            {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   498
            LeadsTo
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   499
              {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   500
                         k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   501
apply (rule single_LeadsTo_I, safe)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   502
apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   503
apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   504
apply (simp_all add: Int_cons_left)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   505
apply (rule LeadsTo_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   506
apply (rule_tac k = "tokens(s`giv)" in tokens_take_NbR_lemma2)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   507
apply auto
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   508
apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) 
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   509
apply (simp add: not_lt_iff_le)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   510
apply (force dest: prefix_length_le_equal) 
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   511
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   512
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   513
(*Fourth step in proof of (31): we apply lemma (51) *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   514
lemma (in alloc_progress) length_giv_disj2:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   515
     "[|k \<in> tokbag; n \<in> nat|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   516
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   517
            {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   518
            LeadsTo
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   519
              {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   520
                        n < length(s`giv)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   521
apply (rule LeadsTo_weaken_R)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   522
apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   523
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   524
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   525
(*Fifth step in proof of (31): from the fourth step, taking the union over all
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   526
  k\<in>nat *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   527
lemma (in alloc_progress) length_giv_disj3:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   528
     "n \<in> nat
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   529
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   530
            {s\<in>state. length(s`giv) = n}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   531
            LeadsTo
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   532
              {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   533
                        n < length(s`giv)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   534
apply (rule LeadsTo_weaken_L)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   535
apply (rule_tac I = nat in LeadsTo_UN)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   536
apply (rule_tac k = i in length_giv_disj2)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   537
apply (simp_all add: UN_conj_eq)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   538
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   539
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   540
(*Sixth step in proof of (31): from the fifth step, by PSP with the
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   541
  assumption that ask increases *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   542
lemma (in alloc_progress) length_ask_giv:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   543
 "[|k \<in> nat;  n < k|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   544
  ==> alloc_prog \<squnion> G \<in>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   545
        {s\<in>state. length(s`ask) = k & length(s`giv) = n}
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   546
        LeadsTo
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   547
          {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   548
                     length(s`giv) = n) |
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   549
                    n < length(s`giv)}"
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   550
apply (rule single_LeadsTo_I, safe)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   551
apply (rule_tac a1 = "s`ask" and f1 = "lift(ask)" 
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   552
       in Increasing_imp_Stable [THEN PSP_StableI])
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   553
apply (rule Incr_ask, simp_all)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   554
apply (rule LeadsTo_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   555
apply (rule_tac n = "length(s ` giv)" in length_giv_disj3)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   556
apply simp_all
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   557
apply blast
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   558
apply clarify
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   559
apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   560
apply (blast dest!: prefix_length_le intro: lt_trans2)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   561
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   562
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   563
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   564
(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   565
lemma (in alloc_progress) length_ask_giv2:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   566
     "[|k \<in> nat;  n < k|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   567
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   568
            {s\<in>state. length(s`ask) = k & length(s`giv) = n}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   569
            LeadsTo
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   570
              {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   571
                         length(s`giv) < length(s`ask) & length(s`giv) = n) |
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   572
                        n < length(s`giv)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   573
apply (rule LeadsTo_weaken_R)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   574
apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14076
diff changeset
   575
apply (simp add: INT_iff)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   576
apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   577
apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   578
apply (blast intro: le_trans)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   579
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   580
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   581
(*Eighth step in proof of (31): by 50, we get |giv| > n. *)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   582
lemma (in alloc_progress) extend_giv:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   583
     "[| k \<in> nat;  n < k|]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   584
      ==> alloc_prog \<squnion> G \<in>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   585
            {s\<in>state. length(s`ask) = k & length(s`giv) = n}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   586
            LeadsTo {s\<in>state. n < length(s`giv)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   587
apply (rule LeadsTo_Un_duplicate)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   588
apply (rule LeadsTo_cancel1)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   589
apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   590
apply (simp_all add: Incr_ask lt_nat_in_nat)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   591
apply (rule LeadsTo_weaken_R)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   592
apply (rule length_ask_giv2, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   593
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   594
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   595
(*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n.
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   596
  The report has an error: putting |ask|=k for the precondition fails because
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   597
  we can't expect |ask| to remain fixed until |giv| increases.*)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   598
lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   599
 "k \<in> nat
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   600
  ==> alloc_prog \<squnion> G \<in>
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   601
        {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   602
(* Proof by induction over the difference between k and n *)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   603
apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   604
apply (auto simp add: lam_def Collect_vimage_eq)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   605
apply (rule single_LeadsTo_I, auto)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   606
apply (rename_tac "s0")
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   607
apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ")
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   608
 apply (rule_tac [2] subset_imp_LeadsTo)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   609
  apply (auto simp add: not_lt_iff_le)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   610
 prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   611
apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   612
       in Increasing_imp_Stable [THEN PSP_StableI])
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   613
apply (rule Incr_ask, simp)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   614
apply (force)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   615
apply (rule LeadsTo_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   616
apply (rule_tac n = "length(s0 ` giv)" and k = "length(s0 ` ask)"
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   617
       in extend_giv) 
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   618
apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) 
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   619
apply (blast dest!: prefix_length_le intro: lt_trans2)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   620
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   621
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   622
(*Final lemma: combine previous result with lemma (30)*)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   623
lemma (in alloc_progress) final:
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   624
     "h \<in> list(tokbag)
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   625
      ==> alloc_prog \<squnion> G
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14071
diff changeset
   626
            \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
   627
              {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   628
apply (rule single_LeadsTo_I)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   629
 prefer 2 apply simp
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   630
apply (rename_tac s0)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   631
apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   632
       in Increasing_imp_Stable [THEN PSP_StableI])
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   633
   apply (rule Incr_ask)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   634
  apply (simp_all add: Int_cons_left)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   635
apply (rule LeadsTo_weaken)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   636
apply (rule_tac k1 = "length(s0 ` ask)"
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   637
       in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   638
                              alloc_prog_ask_LeadsTo_giv])
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   639
apply (auto simp add: Incr_ask)
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   640
apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le 
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   641
                    lt_trans2)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   642
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   643
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   644
(** alloc_prog liveness property (31), page 18 **)
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   645
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   646
theorem alloc_prog_progress:
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   647
"alloc_prog \<in>
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   648
    Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   649
    Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   650
    (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   651
              {s\<in>state. k \<le> tokens(s`rel)})
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   652
  guarantees (\<Inter>h \<in> list(tokbag).
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   653
              {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   654
              {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   655
apply (rule guaranteesI)
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14076
diff changeset
   656
apply (rule INT_I)
14071
373806545656 Converting ZF/UNITY to Isar
paulson
parents: 14061
diff changeset
   657
apply (rule alloc_progress.final)
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14076
diff changeset
   658
apply (auto simp add: alloc_progress_def)
14060
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   659
done
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   660
c0c4af41fa3b Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
diff changeset
   661
end