Attic/ExtGG.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 07 Feb 2017 01:10:46 +0000
changeset 146 2d66c0b0bacf
parent 130 0f124691c191
permissions -rw-r--r--
test
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     1
section {*
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     2
  This file contains lemmas used to guide the recalculation of current precedence 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     3
  after every system call (or system operation)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     4
*}
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
     5
theory Implementation
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
     6
imports PIPBasics
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     7
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     8
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
     9
text {* (* ddd *)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    10
  One beauty of our modelling is that we follow the definitional extension tradition of HOL.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    11
  The benefit of such a concise and miniature model is that  large number of intuitively 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    12
  obvious facts are derived as lemmas, rather than asserted as axioms.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    13
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    14
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    15
text {*
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    16
  However, the lemmas in the forthcoming several locales are no longer 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    17
  obvious. These lemmas show how the current precedences should be recalculated 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    18
  after every execution step (in our model, every step is represented by an event, 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    19
  which in turn, represents a system call, or operation). Each operation is 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    20
  treated in a separate locale.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    21
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    22
  The complication of current precedence recalculation comes 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    23
  because the changing of RAG needs to be taken into account, 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    24
  in addition to the changing of precedence. 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    25
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    26
  The reason RAG changing affects current precedence is that,
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    27
  according to the definition, current precedence 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    28
  of a thread is the maximum of the precedences of every threads in its subtree, 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    29
  where the notion of sub-tree in RAG is defined in RTree.thy.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    30
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    31
  Therefore, for each operation, lemmas about the change of precedences 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    32
  and RAG are derived first, on which lemmas about current precedence 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    33
  recalculation are based on.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    34
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    35
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    36
section {* The @{term Set} operation *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    37
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    38
context valid_trace_set
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    39
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    40
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    41
text {* (* ddd *)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    42
  The following two lemmas confirm that @{text "Set"}-operation
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    43
  only changes the precedence of the initiating thread (or actor)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    44
  of the operation (or event).
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    45
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    46
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    47
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    48
lemma eq_preced:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    49
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    50
  shows "preced th' (e#s) = preced th' s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    51
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    52
  from assms show ?thesis 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    53
    by (unfold is_set, auto simp:preced_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    54
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    55
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    56
lemma eq_the_preced: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    57
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    58
  shows "the_preced (e#s) th' = the_preced s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    59
  using assms
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    60
  by (unfold the_preced_def, intro eq_preced, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    61
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    62
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    63
text {* (* ddd *)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    64
  Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    65
  only affects those threads, which as @{text "Th th"} in their sub-trees.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    66
  
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    67
  The proof of this lemma is simplified by using the alternative definition 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    68
  of @{text "cp"}. 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    69
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    70
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    71
lemma eq_cp_pre:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    72
  assumes nd: "Th th \<notin> subtree (RAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    73
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    74
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    75
  -- {* After unfolding using the alternative definition, elements 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    76
        affecting the @{term "cp"}-value of threads become explicit. 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    77
        We only need to prove the following: *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    78
  have "Max (the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    79
        Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    80
        (is "Max (?f ` ?S1) = Max (?g ` ?S2)")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    81
  proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    82
    -- {* The base sets are equal. *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    83
    have "?S1 = ?S2" using RAG_unchanged by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    84
    -- {* The function values on the base set are equal as well. *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    85
    moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    86
    proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    87
      fix th1
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    88
      assume "th1 \<in> ?S2"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    89
      with nd have "th1 \<noteq> th" by (auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    90
      from eq_the_preced[OF this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    91
      show "the_preced (e#s) th1 = the_preced s th1" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    92
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    93
    -- {* Therefore, the image of the functions are equal. *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    94
    ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    95
    thus ?thesis by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    96
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    97
  thus ?thesis by (simp add:cp_alt_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    98
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
    99
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   100
text {*
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   101
  The following lemma shows that @{term "th"} is not in the 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   102
  sub-tree of any other thread. 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   103
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   104
lemma th_in_no_subtree:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   105
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   106
  shows "Th th \<notin> subtree (RAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   107
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   108
  from readys_in_no_subtree[OF th_ready_s assms(1)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   109
  show ?thesis by blast
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   110
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   111
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   112
text {* 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   113
  By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   114
  it is obvious that the change of priority only affects the @{text "cp"}-value 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   115
  of the initiating thread @{text "th"}.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   116
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   117
lemma eq_cp:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   118
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   119
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   120
  by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   121
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   122
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   123
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   124
section {* The @{term V} operation *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   125
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   126
text {*
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   127
  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   128
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   129
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   130
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   131
context valid_trace_v
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   132
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   133
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   134
lemma ancestors_th: "ancestors (RAG s) (Th th) = {}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   135
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   136
  from readys_root[OF th_ready_s]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   137
  show ?thesis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   138
  by (unfold root_def, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   139
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   140
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   141
lemma edge_of_th:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   142
    "(Cs cs, Th th) \<in> RAG s" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   143
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   144
 from holding_th_cs_s
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   145
 show ?thesis 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   146
    by (unfold s_RAG_def holding_eq, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   147
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   148
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   149
lemma ancestors_cs: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   150
  "ancestors (RAG s) (Cs cs) = {Th th}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   151
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   152
  have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th)  \<union>  {Th th}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   153
   by (rule rtree_RAG.ancestors_accum[OF edge_of_th])
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   154
  from this[unfolded ancestors_th] show ?thesis by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   155
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   156
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   157
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   158
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   159
text {*
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   160
  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   161
  which represents the case when there is another thread @{text "th'"}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   162
  to take over the critical resource released by the initiating thread @{text "th"}.
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   163
*}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   164
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   165
context valid_trace_v_n
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   166
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   167
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   168
lemma sub_RAGs': 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   169
  "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   170
     using next_th_RAG[OF next_th_taker]  .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   171
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   172
lemma ancestors_th': 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   173
  "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   174
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   175
  have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   176
  proof(rule  rtree_RAG.ancestors_accum)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   177
    from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   178
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   179
  thus ?thesis using ancestors_th ancestors_cs by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   180
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   181
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   182
lemma RAG_s:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   183
  "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union>
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   184
                                         {(Cs cs, Th taker)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   185
 by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   186
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   187
lemma subtree_kept: (* ddd *)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   188
  assumes "th1 \<notin> {th, taker}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   189
  shows "subtree (RAG (e#s)) (Th th1) = 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   190
                     subtree (RAG s) (Th th1)" (is "_ = ?R")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   191
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   192
  let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   193
  let ?RAG'' = "?RAG' \<union> {(Cs cs, Th taker)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   194
  have "subtree ?RAG' (Th th1) = ?R" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   195
  proof(rule subset_del_subtree_outside)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   196
    show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \<inter> subtree (RAG s) (Th th1) = {}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   197
    proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   198
      have "(Th th) \<notin> subtree (RAG s) (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   199
      proof(rule subtree_refute)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   200
        show "Th th1 \<notin> ancestors (RAG s) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   201
          by (unfold ancestors_th, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   202
      next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   203
        from assms show "Th th1 \<noteq> Th th" by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   204
      qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   205
      moreover have "(Cs cs) \<notin>  subtree (RAG s) (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   206
      proof(rule subtree_refute)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   207
        show "Th th1 \<notin> ancestors (RAG s) (Cs cs)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   208
          by (unfold ancestors_cs, insert assms, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   209
      qed simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   210
      ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s) (Th th1) = {}" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   211
      thus ?thesis by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   212
     qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   213
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   214
  moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   215
  proof(rule subtree_insert_next)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   216
    show "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   217
    proof(rule subtree_refute)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   218
      show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   219
            (is "_ \<notin> ?R")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   220
      proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   221
          have "?R \<subseteq> ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   222
          moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   223
          ultimately show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   224
      qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   225
    next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   226
      from assms show "Th th1 \<noteq> Th taker" by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   227
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   228
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   229
  ultimately show ?thesis by (unfold RAG_s, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   230
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   231
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   232
lemma cp_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   233
  assumes "th1 \<notin> {th, taker}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   234
  shows "cp (e#s) th1 = cp s th1"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   235
    by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   236
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   237
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   238
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   239
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   240
context valid_trace_v_e
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   241
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   242
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   243
find_theorems RAG s e
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   244
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   245
lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   246
  by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   247
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   248
lemma subtree_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   249
  assumes "th1 \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   250
  shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   251
proof(unfold RAG_s, rule subset_del_subtree_outside)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   252
  show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s) (Th th1) = {}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   253
  proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   254
    have "(Th th) \<notin> subtree (RAG s) (Th th1)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   255
    proof(rule subtree_refute)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   256
      show "Th th1 \<notin> ancestors (RAG s) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   257
          by (unfold ancestors_th, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   258
    next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   259
      from assms show "Th th1 \<noteq> Th th" by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   260
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   261
    thus ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   262
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   263
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   264
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   265
lemma cp_kept_1:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   266
  assumes "th1 \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   267
  shows "cp (e#s) th1 = cp s th1"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   268
    by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   269
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   270
lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   271
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   272
  { fix n
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   273
    have "(Cs cs) \<notin> ancestors (RAG s) n"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   274
    proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   275
      assume "Cs cs \<in> ancestors (RAG s) n"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   276
      hence "(n, Cs cs) \<in> (RAG s)^+" by (auto simp:ancestors_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   277
      from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   278
      then obtain th' where "nn = Th th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   279
        by (unfold s_RAG_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   280
      from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   281
      from this[unfolded s_RAG_def]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   282
      have "waiting (wq s) th' cs" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   283
      from this[unfolded cs_waiting_def]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   284
      have "1 < length (wq s cs)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   285
          by (cases "wq s cs", auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   286
      from holding_next_thI[OF holding_th_cs_s this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   287
      obtain th' where "next_th s th cs th'" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   288
      thus False using no_taker by blast
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   289
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   290
  } note h = this
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   291
  {  fix n
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   292
     assume "n \<in> subtree (RAG s) (Cs cs)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   293
     hence "n = (Cs cs)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   294
     by (elim subtreeE, insert h, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   295
  } moreover have "(Cs cs) \<in> subtree (RAG s) (Cs cs)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   296
      by (auto simp:subtree_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   297
  ultimately show ?thesis by auto 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   298
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   299
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   300
lemma subtree_th: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   301
  "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   302
proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   303
  from edge_of_th
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   304
  show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   305
    by (unfold edges_in_def, auto simp:subtree_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   306
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   307
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   308
lemma cp_kept_2: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   309
  shows "cp (e#s) th = cp s th" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   310
 by (unfold cp_alt_def subtree_th the_preced_es, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   311
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   312
lemma eq_cp:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   313
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   314
  using cp_kept_1 cp_kept_2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   315
  by (cases "th' = th", auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   316
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   317
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   318
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   319
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   320
section {* The @{term P} operation *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   321
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   322
context valid_trace_p
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   323
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   324
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   325
lemma root_th: "root (RAG s) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   326
  by (simp add: ready_th_s readys_root)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   327
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   328
lemma in_no_others_subtree:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   329
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   330
  shows "Th th \<notin> subtree (RAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   331
proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   332
  assume "Th th \<in> subtree (RAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   333
  thus False
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   334
  proof(cases rule:subtreeE)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   335
    case 1
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   336
    with assms show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   337
  next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   338
    case 2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   339
    with root_th show ?thesis by (auto simp:root_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   340
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   341
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   342
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   343
lemma preced_kept: "the_preced (e#s) = the_preced s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   344
proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   345
  fix th'
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   346
  show "the_preced (e # s) th' = the_preced s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   347
    by (unfold the_preced_def is_p preced_def, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   348
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   349
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   350
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   351
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   352
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   353
context valid_trace_p_h
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   354
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   355
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   356
lemma subtree_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   357
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   358
  shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   359
proof(unfold RAG_es, rule subtree_insert_next)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   360
  from in_no_others_subtree[OF assms] 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   361
  show "Th th \<notin> subtree (RAG s) (Th th')" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   362
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   363
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   364
lemma cp_kept: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   365
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   366
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   367
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   368
  have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   369
        (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   370
        by (unfold preced_kept subtree_kept[OF assms], simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   371
  thus ?thesis by (unfold cp_alt_def, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   372
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   373
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   374
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   375
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   376
context valid_trace_p_w
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   377
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   378
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   379
lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   380
  using holding_s_holder
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   381
  by (unfold s_RAG_def, fold holding_eq, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   382
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   383
lemma tRAG_s: 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   384
  "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   385
  using local.RAG_tRAG_transfer[OF RAG_es cs_held] .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   386
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   387
lemma cp_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   388
  assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   389
  shows "cp (e#s) th'' = cp s th''"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   390
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   391
  have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   392
  proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   393
    have "Th holder \<notin> subtree (tRAG s) (Th th'')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   394
    proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   395
      assume "Th holder \<in> subtree (tRAG s) (Th th'')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   396
      thus False
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   397
      proof(rule subtreeE)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   398
         assume "Th holder = Th th''"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   399
         from assms[unfolded tRAG_s ancestors_def, folded this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   400
         show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   401
      next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   402
         assume "Th th'' \<in> ancestors (tRAG s) (Th holder)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   403
         moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   404
         proof(rule ancestors_mono)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   405
            show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   406
         qed 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   407
         ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   408
         moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   409
           by (unfold tRAG_s, auto simp:ancestors_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   410
         ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   411
                       by (auto simp:ancestors_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   412
         with assms show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   413
      qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   414
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   415
    from subtree_insert_next[OF this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   416
    have "subtree (tRAG s \<union> {(Th th, Th holder)}) (Th th'') = subtree (tRAG s) (Th th'')" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   417
    from this[folded tRAG_s] show ?thesis .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   418
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   419
  show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   420
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   421
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   422
lemma cp_gen_update_stop: (* ddd *)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   423
  assumes "u \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   424
  and "cp_gen (e#s) u = cp_gen s u"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   425
  and "y \<in> ancestors (tRAG (e#s)) u"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   426
  shows "cp_gen (e#s) y = cp_gen s y"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   427
  using assms(3)
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   428
proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf])
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   429
  case (1 x)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   430
  show ?case (is "?L = ?R")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   431
  proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   432
    from tRAG_ancestorsE[OF 1(2)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   433
    obtain th2 where eq_x: "x = Th th2" by blast
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   434
    from vat_es.cp_gen_rec[OF this]
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   435
    have "?L = 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   436
          Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   437
    also have "... = 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   438
          Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   439
    proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   440
      from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   441
      moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   442
                     cp_gen s ` RTree.children (tRAG s) x"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   443
      proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   444
        have "RTree.children (tRAG (e#s)) x =  RTree.children (tRAG s) x"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   445
        proof(unfold tRAG_s, rule children_union_kept)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   446
          have start: "(Th th, Th holder) \<in> tRAG (e#s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   447
            by (unfold tRAG_s, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   448
          note x_u = 1(2)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   449
          show "x \<notin> Range {(Th th, Th holder)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   450
          proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   451
            assume "x \<in> Range {(Th th, Th holder)}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   452
            hence eq_x: "x = Th holder" using RangeE by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   453
            show False
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   454
            proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   455
              case 1
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   456
              from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   457
              show ?thesis by (auto simp:ancestors_def acyclic_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   458
            next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   459
              case 2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   460
              with x_u[unfolded eq_x]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   461
              have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   462
              with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   463
            qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   464
          qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   465
        qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   466
        moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   467
                       cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   468
        proof(rule f_image_eq)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   469
          fix a
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   470
          assume a_in: "a \<in> ?A"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   471
          from 1(2)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   472
          show "?f a = ?g a"
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   473
          proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   474
             case in_ch
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   475
             show ?thesis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   476
             proof(cases "a = u")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   477
                case True
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   478
                from assms(2)[folded this] show ?thesis .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   479
             next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   480
                case False
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   481
                have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   482
                proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   483
                  assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   484
                  have "a = u"
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   485
                  proof(rule vat_es.rtree_s.ancestors_children_unique)
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   486
                    from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   487
                                          RTree.children (tRAG (e#s)) x" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   488
                  next 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   489
                    from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   490
                                      RTree.children (tRAG (e#s)) x" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   491
                  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   492
                  with False show False by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   493
                qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   494
                from a_in obtain th_a where eq_a: "a = Th th_a" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   495
                    by (unfold RTree.children_def tRAG_alt_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   496
                from cp_kept[OF a_not_in[unfolded eq_a]]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   497
                have "cp (e#s) th_a = cp s th_a" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   498
                from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   499
                show ?thesis .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   500
             qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   501
          next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   502
            case (out_ch z)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   503
            hence h: "z \<in> ancestors (tRAG (e#s)) u" "z \<in> RTree.children (tRAG (e#s)) x" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   504
            show ?thesis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   505
            proof(cases "a = z")
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   506
              case True
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   507
              from h(2) have zx_in: "(z, x) \<in> (tRAG (e#s))" by (auto simp:RTree.children_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   508
              from 1(1)[rule_format, OF this h(1)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   509
              have eq_cp_gen: "cp_gen (e#s) z = cp_gen s z" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   510
              with True show ?thesis by metis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   511
            next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   512
              case False
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   513
              from a_in obtain th_a where eq_a: "a = Th th_a"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   514
                by (auto simp:RTree.children_def tRAG_alt_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   515
              have "a \<notin> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   516
              proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   517
                assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   518
                have "a = z"
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   519
                proof(rule vat_es.rtree_s.ancestors_children_unique)
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   520
                  from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   521
                      by (auto simp:ancestors_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   522
                  with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   523
                                       RTree.children (tRAG (e#s)) x" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   524
                next
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   525
                  from a_in a_in'
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   526
                  show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   527
                    by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   528
                qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   529
                with False show False by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   530
              qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   531
              from cp_kept[OF this[unfolded eq_a]]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   532
              have "cp (e#s) th_a = cp s th_a" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   533
              from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   534
              show ?thesis .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   535
            qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   536
          qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   537
        qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   538
        ultimately show ?thesis by metis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   539
      qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   540
      ultimately show ?thesis by simp
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   541
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   542
    also have "... = ?R"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   543
      by (fold cp_gen_rec[OF eq_x], simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   544
    finally show ?thesis .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   545
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   546
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   547
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   548
lemma cp_up:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   549
  assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   550
  and "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   551
  and "(Th th'') \<in> ancestors (tRAG (e#s)) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   552
  shows "cp (e#s) th'' = cp s th''"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   553
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   554
  have "cp_gen (e#s) (Th th'') = cp_gen s (Th th'')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   555
  proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   556
    from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   557
    show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   558
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   559
  with cp_gen_def_cond[OF refl[of "Th th''"]]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   560
  show ?thesis by metis
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   561
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   562
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   563
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   564
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   565
section {* The @{term Create} operation *}
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   566
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   567
context valid_trace_create
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   568
begin 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   569
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   570
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   571
  by (unfold tRAG_alt_def RAG_unchanged, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   572
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   573
lemma preced_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   574
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   575
  shows "the_preced (e#s) th' = the_preced s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   576
  by (unfold the_preced_def preced_def is_create, insert assms, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   577
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   578
lemma th_not_in: "Th th \<notin> Field (tRAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   579
  by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   580
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   581
lemma eq_cp:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   582
  assumes neq_th: "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   583
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   584
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   585
  have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   586
        (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   587
  proof(unfold tRAG_kept, rule f_image_eq)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   588
    fix a
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   589
    assume a_in: "a \<in> subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   590
    then obtain th_a where eq_a: "a = Th th_a" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   591
    proof(cases rule:subtreeE)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   592
      case 2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   593
      from ancestors_Field[OF 2(2)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   594
      and that show ?thesis by (unfold tRAG_alt_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   595
    qed auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   596
    have neq_th_a: "th_a \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   597
    proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   598
      have "(Th th) \<notin> subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   599
      proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   600
        assume "Th th \<in> subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   601
        thus False
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   602
        proof(cases rule:subtreeE)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   603
          case 2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   604
          from ancestors_Field[OF this(2)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   605
          and th_not_in[unfolded Field_def]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   606
          show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   607
        qed (insert assms, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   608
      qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   609
      with a_in[unfolded eq_a] show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   610
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   611
    from preced_kept[OF this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   612
    show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   613
      by (unfold eq_a, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   614
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   615
  thus ?thesis by (unfold cp_alt_def1, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   616
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   617
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   618
lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   619
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   620
  { fix a
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   621
    assume "a \<in> RTree.children (tRAG (e#s)) (Th th)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   622
    hence "(a, Th th) \<in> tRAG (e#s)" by (auto simp:RTree.children_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   623
    with th_not_in have False 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   624
     by (unfold Field_def tRAG_kept, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   625
  } thus ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   626
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   627
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   628
lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
105
0c89419b4742 Commit to revert
zhangx
parents: 89
diff changeset
   629
 by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
85
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   630
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   631
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   632
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   633
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   634
context valid_trace_exit
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   635
begin
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   636
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   637
lemma preced_kept:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   638
  assumes "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   639
  shows "the_preced (e#s) th' = the_preced s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   640
  using assms
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   641
  by (unfold the_preced_def is_exit preced_def, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   642
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   643
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   644
  by (unfold tRAG_alt_def RAG_unchanged, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   645
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   646
lemma th_RAG: "Th th \<notin> Field (RAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   647
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   648
  have "Th th \<notin> Range (RAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   649
  proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   650
    assume "Th th \<in> Range (RAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   651
    then obtain cs where "holding (wq s) th cs"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   652
      by (unfold Range_iff s_RAG_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   653
    with holdents_th_s[unfolded holdents_def]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   654
    show False by (unfold holding_eq, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   655
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   656
  moreover have "Th th \<notin> Domain (RAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   657
  proof
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   658
    assume "Th th \<in> Domain (RAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   659
    then obtain cs where "waiting (wq s) th cs"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   660
      by (unfold Domain_iff s_RAG_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   661
    with th_ready_s show False by (unfold readys_def waiting_eq, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   662
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   663
  ultimately show ?thesis by (auto simp:Field_def)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   664
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   665
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   666
lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   667
  using th_RAG tRAG_Field by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   668
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   669
lemma eq_cp:
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   670
  assumes neq_th: "th' \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   671
  shows "cp (e#s) th' = cp s th'"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   672
proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   673
  have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   674
        (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   675
  proof(unfold tRAG_kept, rule f_image_eq)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   676
    fix a
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   677
    assume a_in: "a \<in> subtree (tRAG s) (Th th')"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   678
    then obtain th_a where eq_a: "a = Th th_a" 
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   679
    proof(cases rule:subtreeE)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   680
      case 2
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   681
      from ancestors_Field[OF 2(2)]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   682
      and that show ?thesis by (unfold tRAG_alt_def, auto)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   683
    qed auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   684
    have neq_th_a: "th_a \<noteq> th"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   685
    proof -
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   686
      from readys_in_no_subtree[OF th_ready_s assms]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   687
      have "(Th th) \<notin> subtree (RAG s) (Th th')" .
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   688
      with tRAG_subtree_RAG[of s "Th th'"]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   689
      have "(Th th) \<notin> subtree (tRAG s) (Th th')" by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   690
      with a_in[unfolded eq_a] show ?thesis by auto
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   691
    qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   692
    from preced_kept[OF this]
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   693
    show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   694
      by (unfold eq_a, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   695
  qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   696
  thus ?thesis by (unfold cp_alt_def1, simp)
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   697
qed
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   698
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   699
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   700
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   701
end
d239aa953315 Added PrioG.thy as a parallel copy of Correctness.thy
zhangx
parents:
diff changeset
   702