src/ZF/UNITY/Merge.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46823 57bf0cecb366
child 59788 6f7b6adac439
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: 24893
diff changeset
     1
(*  Title:      ZF/UNITY/Merge.thy
14053
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: 24893
diff changeset
     5
A multiple-client allocator from a single-client allocator: Merge
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
     6
specification.
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     7
*)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14077
diff changeset
     9
theory Merge imports AllocBase Follows  Guar GenPrefix begin
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    10
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    11
(** Merge specification (the number of inputs is Nclients) ***)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    12
(** Parameter A represents the type of items to Merge **)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    15
  (*spec (10)*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    16
  merge_increasing :: "[i, i, i] =>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    17
    "merge_increasing(A, Out, iOut) == program guarantees
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    18
         (lift(Out) IncreasingWrt  prefix(A)/list(A)) Int
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    19
         (lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    20
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    21
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    22
  (*spec (11)*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
  merge_eq_Out :: "[i, i] =>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    24
  "merge_eq_Out(Out, iOut) == program guarantees
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    25
         Always({s \<in> state. length(s`Out) = length(s`iOut)})"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    26
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    27
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    28
  (*spec (12)*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    29
  merge_bounded :: "i=>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    30
  "merge_bounded(iOut) == program guarantees
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    31
         Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    32
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    33
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    34
  (*spec (13)*)
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    35
  (* Parameter A represents the type of tokens *)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    36
  merge_follows :: "[i, i=>i, i, i] =>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    37
    "merge_follows(A, In, Out, iOut) ==
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    38
     (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    39
                   guarantees
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    40
     (\<Inter>n \<in> Nclients. 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    41
        (%s. sublist(s`Out, {k \<in> nat. k < length(s`iOut) &
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    42
                      nth(k, s`iOut) = n})) Fols lift(In(n))
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    43
         Wrt prefix(A)/list(A))"
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    44
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    45
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    46
  (*spec: preserves part*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    47
  merge_preserves :: "[i=>i] =>i"  where
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    48
    "merge_preserves(In) == \<Inter>n \<in> nat. preserves(lift(In(n)))"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    49
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    50
definition
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    51
(* environmental constraints*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    52
  merge_allowed_acts :: "[i, i] =>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    53
  "merge_allowed_acts(Out, iOut) ==
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    54
         {F \<in> program. AllowedActs(F) =
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    55
            cons(id(state), (\<Union>G \<in> preserves(lift(Out)) \<inter>
14057
57de6d68389e x-symbols (mostly)
paulson
parents: 14053
diff changeset
    56
                                   preserves(lift(iOut)). Acts(G)))}"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    57
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    58
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    59
  merge_spec :: "[i, i =>i, i, i]=>i"  where
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    60
  "merge_spec(A, In, Out, iOut) ==
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    61
   merge_increasing(A, Out, iOut) \<inter> merge_eq_Out(Out, iOut) \<inter>
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    62
   merge_bounded(iOut) \<inter>  merge_follows(A, In, Out, iOut)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    63
   \<inter> merge_allowed_acts(Out, iOut) \<inter> merge_preserves(In)"
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    64
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
    65
(** State definitions.  OUTPUT variables are locals **)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    66
locale merge =
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    67
  fixes In   --{*merge's INPUT histories: streams to merge*}
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    68
    and Out  --{*merge's OUTPUT history: merged items*}
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    69
    and iOut --{*merge's OUTPUT history: origins of merged items*}
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    70
    and A    --{*the type of items being merged *}
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    71
    and M
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    72
 assumes var_assumes [simp]:
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    73
           "(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    74
     and all_distinct_vars:
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    75
           "\<forall>n. all_distinct([In(n), Out, iOut])"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    76
     and type_assumes [simp]:
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    77
           "(\<forall>n. type_of(In(n))=list(A)) &
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    78
            type_of(Out)=list(A) &
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    79
            type_of(iOut)=list(nat)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    80
     and default_val_assumes [simp]: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    81
           "(\<forall>n. default_val(In(n))=Nil) &
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    82
            default_val(Out)=Nil &
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    83
            default_val(iOut)=Nil"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    84
     and merge_spec:  "M \<in> merge_spec(A, In, Out, iOut)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    85
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    86
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    87
lemma (in merge) In_value_type [TC,simp]: "s \<in> state ==> s`In(n) \<in> list(A)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    88
apply (unfold state_def)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    89
apply (drule_tac a = "In (n)" in apply_type)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    90
apply auto
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    91
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    92
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    93
lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    94
apply (unfold state_def)
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
    95
apply (drule_tac a = Out in apply_type, auto)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    96
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    97
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    98
lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
    99
apply (unfold state_def)
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   100
apply (drule_tac a = iOut in apply_type, auto)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   101
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   102
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   103
lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   104
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   105
apply (auto dest: guarantees_type [THEN subsetD]
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   106
            simp add: merge_spec_def merge_increasing_def)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   107
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   108
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   109
lemma (in merge) merge_Allowed: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   110
     "Allowed(M) = (preserves(lift(Out)) \<inter> preserves(lift(iOut)))"
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   111
apply (insert merge_spec preserves_type [of "lift (Out)"])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   112
apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   113
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   114
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   115
lemma (in merge) M_ok_iff: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   116
     "G \<in> program ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   117
       M ok G \<longleftrightarrow> (G \<in> preserves(lift(Out)) &   
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   118
                   G \<in> preserves(lift(iOut)) & M \<in> Allowed(G))"
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   119
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   120
apply (auto simp add: merge_Allowed ok_iff_Allowed)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   121
done
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
   122
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   123
lemma (in merge) merge_Always_Out_eq_iOut: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   124
     "[| G \<in> preserves(lift(Out)); G \<in> preserves(lift(iOut));  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   125
         M \<in> Allowed(G) |]
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   126
      ==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   127
apply (frule preserves_type [THEN subsetD])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   128
apply (subgoal_tac "G \<in> program")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   129
 prefer 2 apply assumption
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   130
apply (frule M_ok_iff)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   131
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   132
apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   133
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   134
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   135
lemma (in merge) merge_Bounded: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   136
     "[| G \<in> preserves(lift(iOut)); G \<in> preserves(lift(Out));  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   137
         M \<in> Allowed(G) |] ==>  
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   138
       M \<squnion> G: Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   139
apply (frule preserves_type [THEN subsetD])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   140
apply (frule M_ok_iff)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   141
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   142
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   143
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   144
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   145
lemma (in merge) merge_bag_Follows_lemma: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   146
"[| G \<in> preserves(lift(iOut));  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   147
    G: preserves(lift(Out)); M \<in> Allowed(G) |]  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   148
  ==> M \<squnion> G \<in> Always  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   149
    ({s \<in> state. msetsum(%i. bag_of(sublist(s`Out,  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   150
      {k \<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})),  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   151
                   Nclients, A) = bag_of(s`Out)})"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   152
apply (rule Always_Diff_Un_eq [THEN iffD1]) 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   153
apply (rule_tac [2] state_AlwaysI [THEN Always_weaken]) 
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   154
apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded], auto)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   155
apply (subst bag_of_sublist_UN_disjoint [symmetric])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   156
apply (auto simp add: nat_into_Finite set_of_list_conv_nth  [OF iOut_value_type])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   157
apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   158
apply (auto simp add: sublist_upt_eq_take [OF Out_value_type] 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   159
                      length_type  [OF iOut_value_type]  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   160
                      take_all [OF _ Out_value_type] 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   161
                      length_type [OF iOut_value_type])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   162
apply (rule equalityI)
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   163
apply (blast dest: ltD, clarify)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   164
apply (subgoal_tac "length (x ` iOut) \<in> nat")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   165
 prefer 2 apply (simp add: length_type [OF iOut_value_type]) 
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   166
apply (subgoal_tac "xa \<in> nat")
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   167
apply (simp_all add: Ord_mem_iff_lt)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   168
prefer 2 apply (blast intro: lt_trans)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 32960
diff changeset
   169
apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   170
apply (simp add: ltI nat_into_Ord)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   171
apply (blast dest: ltD)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   172
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   173
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   174
theorem (in merge) merge_bag_Follows: 
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   175
    "M \<in> (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))  
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   176
            guarantees   
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   177
      (%s. bag_of(s`Out)) Fols  
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   178
      (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)"
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   179
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   180
apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   181
     apply (simp_all add: M_ok_iff, clarify)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   182
apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   183
   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   184
apply (simp add: INT_iff merge_spec_def merge_follows_def, clarify)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   185
apply (cut_tac merge_spec)
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   186
apply (subgoal_tac "M ok G")
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   187
 prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   188
apply (drule guaranteesD, assumption)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14073
diff changeset
   189
  apply (simp add: merge_spec_def merge_follows_def, blast)
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   190
apply (simp cong add: Follows_cong
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   191
            add: refl_prefix
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   192
               mono_bag_of [THEN subset_Follows_comp, THEN subsetD, 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   193
                            unfolded metacomp_def])
14073
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   194
done
21e2ff495d81 Conversion of "Merge" to Isar format
paulson
parents: 14057
diff changeset
   195
14053
4daa384f4fd7 Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
diff changeset
   196
end