src/ZF/UNITY/ClientImpl.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
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:
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/ClientImpl.thy
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     3
    Copyright   2002  University of Cambridge
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     4
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
     5
Distributed Resource Management System:  Client Implementation.
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     6
*)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16183
diff changeset
     8
theory ClientImpl imports AllocBase Guar begin
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
     9
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    10
abbreviation "ask == Var(Nil)" (* input history:  tokens requested *)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    11
abbreviation "giv == Var([0])" (* output history: tokens granted *)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    12
abbreviation "rel == Var([1])" (* input history: tokens released *)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 24051
diff changeset
    13
abbreviation "tok == Var([2])" (* the number of available tokens *)
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    14
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    15
axiomatization where
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    16
  type_assumes:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    17
  "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    18
   type_of(rel) = list(tokbag) & type_of(tok) = nat" and
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    19
  default_val_assumes:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    20
  "default_val(ask) = Nil & default_val(giv) = Nil &
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    21
   default_val(rel) = Nil & default_val(tok) = 0"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    22
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    23
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    24
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    25
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    26
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    27
 (** Release some client_tokens **)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    28
    "client_rel_act ==
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    29
     {<s,t> \<in> state*state.
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    30
      \<exists>nrel \<in> nat. nrel = length(s`rel) &
14057
57de6d68389e x-symbols (mostly)
paulson
parents: 14053
diff changeset
    31
                   t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
57de6d68389e x-symbols (mostly)
paulson
parents: 14053
diff changeset
    32
                   nrel < length(s`giv) &
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    33
                   nth(nrel, s`ask) \<le> nth(nrel, s`giv)}"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    34
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    35
  (** Choose a new token requirement **)
14057
57de6d68389e x-symbols (mostly)
paulson
parents: 14053
diff changeset
    36
  (** Including t=s suppresses fairness, allowing the non-trivial part
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    37
      of the action to be ignored **)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    38
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    39
  "client_tok_act == {<s,t> \<in> state*state. t=s |
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    40
                     t = s(tok:=succ(s`tok mod NbT))}"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    41
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    42
definition
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    43
  "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    44
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    45
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    46
  "client_prog ==
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    47
   mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil &
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    48
                       s`ask = Nil & s`rel = Nil},
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    49
                    {client_rel_act, client_tok_act, client_ask_act},
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    50
                   \<Union>G \<in> preserves(lift(rel)) Int
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    51
                         preserves(lift(ask)) Int
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 26289
diff changeset
    52
                         preserves(lift(tok)).  Acts(G))"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    53
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    54
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    55
declare type_assumes [simp] default_val_assumes [simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    56
(* This part should be automated *)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    57
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    58
lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    59
apply (unfold state_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    60
apply (drule_tac a = ask in apply_type, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    61
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    62
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    63
lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    64
apply (unfold state_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    65
apply (drule_tac a = giv in apply_type, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    66
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    67
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    68
lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    69
apply (unfold state_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    70
apply (drule_tac a = rel in apply_type, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    71
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    72
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    73
lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    74
apply (unfold state_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    75
apply (drule_tac a = tok in apply_type, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    76
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    77
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    78
(** The Client Program **)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    79
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    80
lemma client_type [simp,TC]: "client_prog \<in> program"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    81
apply (unfold client_prog_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    82
apply (simp (no_asm))
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    83
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    84
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    85
declare client_prog_def [THEN def_prg_Init, simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    86
declare client_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
    87
declare client_prog_def [program]
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    88
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    89
declare  client_rel_act_def [THEN def_act_simp, simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    90
declare  client_tok_act_def [THEN def_act_simp, simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    91
declare  client_ask_act_def [THEN def_act_simp, simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    92
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    93
lemma client_prog_ok_iff:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    94
  "\<forall>G \<in> program. (client_prog ok G) \<longleftrightarrow>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
    95
   (G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) &
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    96
    G \<in> preserves(lift(tok)) &  client_prog \<in> Allowed(G))"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    97
by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    98
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
    99
lemma client_prog_preserves:
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   100
    "client_prog:(\<Inter>x \<in> var-{ask, rel, tok}. preserves(lift(x)))"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   101
apply (rule Inter_var_DiffI, force)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   102
apply (rule ballI)
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   103
apply (rule preservesI, safety, auto)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   104
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   105
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   106
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   107
lemma preserves_lift_imp_stable:
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   108
     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   109
apply (drule preserves_imp_stable)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   110
apply (simp add: lift_def)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   111
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   112
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   113
lemma preserves_imp_prefix:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   114
     "G \<in> preserves(lift(ff))
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   115
      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   116
by (erule preserves_lift_imp_stable)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   117
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   118
(*Safety property 1 \<in> ask, rel are increasing: (24) *)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   119
lemma client_prog_Increasing_ask_rel:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   120
"client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   121
apply (unfold guar_def)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   122
apply (auto intro!: increasing_imp_Increasing
26289
9d2c375e242b avoid unclear fact references;
wenzelm
parents: 24893
diff changeset
   123
            simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   124
apply (safety, force, force)+
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   125
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   126
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   127
declare nth_append [simp] append_one_prefix [simp]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   128
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   129
lemma NbT_pos2: "0<NbT"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   130
apply (cut_tac NbT_pos)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   131
apply (rule Ord_0_lt, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   132
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   133
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   134
(*Safety property 2 \<in> the client never requests too many tokens.
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   135
With no Substitution Axiom, we must prove the two invariants simultaneously. *)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   136
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   137
lemma ask_Bounded_lemma:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   138
"[| client_prog ok G; G \<in> program |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   139
      ==> client_prog \<squnion> G \<in>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   140
              Always({s \<in> state. s`tok \<le> NbT}  \<inter>
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   141
                      {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   142
apply (rotate_tac -1)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   143
apply (auto simp add: client_prog_ok_iff)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   144
apply (rule invariantI [THEN stable_Join_Always2], force)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   145
 prefer 2
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   146
 apply (fast intro: stable_Int preserves_lift_imp_stable, safety)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   147
apply (auto dest: ActsD)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   148
apply (cut_tac NbT_pos)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   149
apply (rule NbT_pos2 [THEN mod_less_divisor])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   150
apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   151
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   152
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   153
(* Export version, with no mention of tok in the postcondition, but
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   154
  unfortunately tok must be declared local.*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   155
lemma client_prog_ask_Bounded:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   156
    "client_prog \<in> program guarantees
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   157
                   Always({s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   158
apply (rule guaranteesI)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   159
apply (erule ask_Bounded_lemma [THEN Always_weaken], auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   160
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   161
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   162
(*** Towards proving the liveness property ***)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   163
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   164
lemma client_prog_stable_rel_le_giv:
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   165
    "client_prog \<in> stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
16183
052d9aba392d renamed "constrains" to "safety" to avoid keyword clash
paulson
parents: 15634
diff changeset
   166
by (safety, auto)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   167
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   168
lemma client_prog_Join_Stable_rel_le_giv:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   169
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   170
    ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   171
apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   172
apply (auto simp add: lift_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   173
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   174
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   175
lemma client_prog_Join_Always_rel_le_giv:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   176
     "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   177
    ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   178
by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   179
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   180
lemma def_act_eq:
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   181
     "A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   182
by auto
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   183
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   184
lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   185
by auto
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   186
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   187
lemma transient_lemma:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   188
"client_prog \<in>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   189
  transient({s \<in> state. s`rel = k & <k, h> \<in> strict_prefix(nat)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   190
   & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask})"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   191
apply (rule_tac act = client_rel_act in transientI)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   192
apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   193
apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   194
apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   195
apply (rule ReplaceI)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   196
apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   197
apply (auto intro!: state_update_type app_type length_type nth_type, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   198
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   199
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   200
apply (simp (no_asm_use) add: gen_prefix_iff_nth)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   201
apply (subgoal_tac "h \<in> list(nat)")
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   202
 apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   203
apply (auto simp add: prefix_def Ge_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   204
apply (drule strict_prefix_length_lt)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   205
apply (drule_tac x = "length (x`rel) " in spec)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   206
apply auto
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   207
apply (simp (no_asm_use) add: gen_prefix_iff_nth)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   208
apply (auto simp add: id_def lam_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   209
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   210
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   211
lemma strict_prefix_is_prefix:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   212
    "<xs, ys> \<in> strict_prefix(A) \<longleftrightarrow>  <xs, ys> \<in> prefix(A) & xs\<noteq>ys"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   213
apply (unfold strict_prefix_def id_def lam_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   214
apply (auto dest: prefix_type [THEN subsetD])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   215
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   216
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   217
lemma induct_lemma:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   218
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   219
  ==> client_prog \<squnion> G \<in>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   220
  {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   221
   & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   222
        LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   223
                          & <s`rel, s`giv> \<in> prefix(nat) &
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   224
                                  <h, s`giv> \<in> prefix(nat) &
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   225
                h pfixGe s`ask}"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   226
apply (rule single_LeadsTo_I)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   227
 prefer 2 apply simp
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   228
apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   229
apply (rotate_tac [3] 2)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   230
apply (auto simp add: client_prog_ok_iff)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   231
apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   232
apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   233
apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   234
apply (simp (no_asm_simp))
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   235
apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   236
apply (simp (no_asm_simp))
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   237
apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   238
apply (simp (no_asm_simp))
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   239
apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   240
 prefer 2
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   241
 apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   242
apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1]
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   243
                   prefix_trans)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   244
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   245
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   246
lemma rel_progress_lemma:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   247
"[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   248
  ==> client_prog \<squnion> G  \<in>
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   249
     {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   250
           & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   251
                      LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   252
apply (rule_tac f = "\<lambda>x \<in> state. length(h) #- length(x`rel)"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   253
       in LessThan_induct)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   254
apply (auto simp add: vimage_def)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   255
 prefer 2 apply (force simp add: lam_def)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   256
apply (rule single_LeadsTo_I)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   257
 prefer 2 apply simp
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   258
apply (subgoal_tac "h \<in> list(nat)")
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   259
 prefer 2 apply (blast dest: prefix_type [THEN subsetD])
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   260
apply (rule induct_lemma [THEN LeadsTo_weaken])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   261
    apply (simp add: length_type lam_def)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   262
apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   263
            dest: common_prefix_linear  prefix_type [THEN subsetD])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   264
apply (erule swap)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   265
apply (rule imageI)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   266
 apply (force dest!: simp add: lam_def)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   267
apply (simp add: length_type lam_def, clarify)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   268
apply (drule strict_prefix_length_lt)+
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   269
apply (drule less_imp_succ_add, simp)+
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   270
apply clarify
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   271
apply simp
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   272
apply (erule diff_le_self [THEN ltD])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   273
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   274
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   275
lemma progress_lemma:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   276
"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   277
 ==> client_prog \<squnion> G
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   278
       \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   279
         LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   280
apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI],
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   281
       assumption)
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   282
apply (force simp add: client_prog_ok_iff)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   283
apply (rule LeadsTo_weaken_L)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   284
apply (rule LeadsTo_Un [OF rel_progress_lemma
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   285
                           subset_refl [THEN subset_imp_LeadsTo]])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   286
apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   287
            dest: common_prefix_linear prefix_type [THEN subsetD])
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   288
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   289
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   290
(*Progress property: all tokens that are given will be released*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   291
lemma client_prog_progress:
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   292
"client_prog \<in> Incr(lift(giv))  guarantees
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   293
      (\<Inter>h \<in> list(nat). {s \<in> state. <h, s`giv> \<in> prefix(nat) &
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   294
              h pfixGe s`ask} LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)})"
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   295
apply (rule guaranteesI)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   296
apply (blast intro: progress_lemma, auto)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   297
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   298
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   299
lemma client_prog_Allowed:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   300
     "Allowed(client_prog) =
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 41779
diff changeset
   301
      preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   302
apply (cut_tac v = "lift (ask)" in preserves_type)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46823
diff changeset
   303
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
14061
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   304
                      cons_Int_distrib safety_prop_Acts_iff)
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   305
done
abcb32a7b212 conversion of ClientImpl to Isar script
paulson
parents: 14057
diff changeset
   306
14072
f932be305381 Conversion of UNITY/Distributor to Isar script. General tidy-up.
paulson
parents: 14061
diff changeset
   307
end