Test.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Fri, 23 May 2014 15:19:32 +0100
changeset 36 af38526275f8
child 37 c820ac0f3088
permissions -rw-r--r--
added a test theory for polishing teh proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
theory Test 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
imports Precedence_ord
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
begin
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
type_synonym thread = nat -- {* Type for thread identifiers. *}
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
type_synonym priority = nat  -- {* Type for priorities. *}
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
datatype event = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
  Create thread priority 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
| Exit thread 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
| P thread cs 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
| V thread cs 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
| Set thread priority 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
type_synonym state = "event list"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
fun threads :: "state \<Rightarrow> thread set"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
  where 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
  "threads [] = {}" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
| "threads (Create th prio#s) = {th} \<union> threads s" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
| "threads (Exit th # s) = (threads s) - {th}" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
| "threads (_#s) = threads s" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
  where
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
  "priority th [] = 0" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
| "priority th (Create th' prio#s) = (if th' = th then prio else priority th s)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
| "priority th (Set th' prio#s) = (if th' = th then prio else priority th s)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
| "priority th (_#s) = priority th s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
  where
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
  "last_set th [] = 0" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
| "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
| "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
| "last_set th (_#s) = last_set th s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
  where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
  "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
datatype node = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
  Th "thread" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
| Cs "cs" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  "RAG wq \<equiv> {(Th th, Cs cs) | th cs. waits wq th cs} \<union> {(Cs cs, Th th) | cs th. holds wq th cs}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
  "dependants wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
record schedule_state = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
  wq_fun :: "cs \<Rightarrow> thread list" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
  cprec_fun :: "thread \<Rightarrow> precedence" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
  where 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
abbreviation
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
abbreviation 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
abbreviation
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
  "release qs \<equiv> case qs of
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
             [] => [] 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
fun schs :: "state \<Rightarrow> schedule_state"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
  where 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
  "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
| "schs (Create th prio # s) = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
       (let wq = wq_fun (schs s) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
|  "schs (Exit th # s) = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
       (let wq = wq_fun (schs s) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
          (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
|  "schs (Set th prio # s) = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
       (let wq = wq_fun (schs s) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
          (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
|  "schs (P th cs # s) = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
       (let wq = wq_fun (schs s) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
        let new_wq = wq(cs := (wq cs @ [th])) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
|  "schs (V th cs # s) = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
       (let wq = wq_fun (schs s) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
        let new_wq = wq(cs := release (wq cs)) in
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
  where "wq s = wq_fun (schs s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
  where "cp s \<equiv> cprec_fun (schs s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   105
  "holds2 s \<equiv> holds (wq_fun (schs s))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
  "waits2 s \<equiv> waits (wq_fun (schs s))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
  "RAG2 s \<equiv> RAG (wq_fun (schs s))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
  
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
definition
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
  "dependants2 s \<equiv> dependants (wq_fun (schs s))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
definition readys :: "state \<Rightarrow> thread set"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
  where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waits2 s th cs)}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
definition runing :: "state \<Rightarrow> thread set"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
  where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
  where "holding s th \<equiv> {cs . holds2 s th cs}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   125
lemma holding_RAG: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
  "holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
unfolding holding_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
unfolding holds2_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
unfolding RAG2_def RAG_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
unfolding holds_def waits_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
by auto
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
  where
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
  step_Create: "\<lbrakk>th \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create th prio)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
| step_Exit: "\<lbrakk>th \<in> runing s; holding s th = {}\<rbrakk> \<Longrightarrow> step s (Exit th)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
| step_P: "\<lbrakk>th \<in> runing s;  (Cs cs, Th th)  \<notin> (RAG2 s)^+\<rbrakk> \<Longrightarrow> step s (P th cs)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
| step_V: "\<lbrakk>th \<in> runing s;  holds2 s th cs\<rbrakk> \<Longrightarrow> step s (V th cs)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
| step_Set: "\<lbrakk>th \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set th prio)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
inductive vt :: "state \<Rightarrow> bool"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   142
  where
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
  vt_nil[intro]: "vt []" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
| vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
lemma runing_ready: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
  shows "runing s \<subseteq> readys s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
  unfolding runing_def readys_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
  by auto 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
lemma readys_threads:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
  shows "readys s \<subseteq> threads s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
  unfolding readys_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   154
  by auto
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
lemma wq_distinct_step: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
  assumes "step s e" "distinct (wq s cs)" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
  shows "distinct (wq (e # s) cs)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
using assms
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
apply(induct)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
apply(auto simp add: wq_def Let_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   162
apply(auto simp add: wq_def Let_def RAG2_def RAG_def holds_def runing_def waits2_def waits_def readys_def)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   163
apply(auto split: list.split)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   164
apply(rule someI2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   165
apply(auto)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   166
done
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   167
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
lemma wq_distinct: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
  assumes "vt s" 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   170
  shows "distinct (wq s cs)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
using assms
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
apply(induct)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
apply(simp add: wq_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
apply(simp add: wq_distinct_step)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
done
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   176
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   177
lemma RAG_set_unchanged[simp]: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
  shows "RAG2 (Set th prio # s) = RAG2 s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
unfolding RAG2_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
by (simp add: Let_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
lemma RAG_create_unchanged[simp]: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
  "RAG2 (Create th prio # s) = RAG2 s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
unfolding RAG2_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
by (simp add: Let_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   187
lemma RAG_exit_unchanged[simp]: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   188
  shows "RAG2 (Exit th # s) = RAG2 s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   189
unfolding RAG2_def
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
by (simp add: Let_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
lemma RAG_p1:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
  assumes "wq s cs = []"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
  shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
  using assms
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
  apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
  apply (metis in_set_insert insert_Nil list.distinct(1))
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   198
  done
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   199
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   200
lemma RAG_p2:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
  assumes "vt (P th cs#s)" "wq s cs \<noteq> []"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   202
  shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   203
  using assms
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   204
  apply(simp add: RAG2_def Let_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   205
  apply(erule_tac vt.cases)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   206
  apply(simp)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   207
  apply(clarify)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   208
  apply(simp)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
  apply(erule_tac step.cases)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   210
  apply(simp_all)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   211
  apply(simp add: wq_def RAG_def RAG2_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   212
  apply(simp add: waits_def holds_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
  apply(auto)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
  done
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   217
  where "next_th s th cs t = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   218
    (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
lemma RAG_v:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
assumes vt:"vt (V th cs#s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
shows "
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
  RAG2 (V th cs # s) =
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
  RAG2 s - {(Cs cs, Th th)} -
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
  {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   226
  {(Cs cs, Th th') |th'.  next_th s th cs th'}"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
  apply (insert vt, unfold RAG2_def RAG_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
  sorry
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
lemma waiting_unique:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
  assumes "vt s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
  and "waits2 s th cs1"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
  and "waits2 s th cs2"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
  shows "cs1 = cs2"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
sorry
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   236
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
lemma singleton_Un:
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
  shows "A \<union> {x} = insert x A"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
by simp
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
lemma acyclic_RAG_step: 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
  assumes vt: "vt s"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
  and     stp: "step s e"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   245
  and     ac: "acyclic (RAG2 s)"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
  shows "acyclic (RAG2 (e # s))"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
using stp vt ac
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
proof (induct)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   249
  case (step_P th s cs)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
  have vt: "vt s" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   251
  have ac: "acyclic (RAG2 s)" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   252
  have rn: "th \<in> runing s" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
  have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
  have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
  { assume a: "wq s cs = []" -- "case waiting queue is empty"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   256
    have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"  
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   257
    proof
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   258
      assume "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>*"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   259
      then have "(Th th, Cs cs) \<in> (RAG2 s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   260
      then obtain x where "(x, Cs cs) \<in> RAG2 s" using tranclD2 by metis 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
      with a show False by (auto simp: RAG2_def RAG_def wq_def waits_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
    qed
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   263
    with acyclic_insert ac
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
    have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   265
    then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   266
  }
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
  moreover
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
  { assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
    from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   270
    with acyclic_insert ac 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   271
    have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   272
    then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
  }
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
  ultimately show "acyclic (RAG2 (P th cs # s))" by metis
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   275
next    
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   276
  case (step_V th s cs) 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   277
  have vt: "vt s" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   278
  have ac: "acyclic (RAG2 s)" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   279
  have rn: "th \<in> runing s" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   280
  have hd: "holds2 s th cs" by fact
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   281
  from hd 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   282
  have th_in: "th \<in> set (wq s cs)" and
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   283
       eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   284
  then obtain rest where
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   285
    eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   286
  show ?case
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   287
    apply(subst RAG_v)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   288
    apply(rule vt_cons)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
    apply(rule vt)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
    apply(rule step.step_V)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
    apply(rule rn)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   292
    apply(rule hd)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   293
    using eq_wq
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   294
    apply(cases "rest = []")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
    apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   296
    apply(simp)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
    apply(rule acyclic_subset)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   298
    apply(rule ac)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
    apply(auto simp add: next_th_def)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   301
    -- "case wq more than a singleton"
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   302
    apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} = 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   303
      {(Cs cs, Th th') |th'. next_th s th cs th'}")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
    apply(rotate_tac 2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   305
    apply(drule sym)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
    apply(simp only: singleton_Un)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   307
    apply(simp only: acyclic_insert)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   308
    apply(rule conjI)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
    apply(rule acyclic_subset)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
    apply(rule ac)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   311
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
    apply(rotate_tac 2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   313
    apply(thin_tac "?X")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   314
    defer 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   315
    apply(simp add: next_th_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   316
    apply(clarify)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   317
    apply(simp add: rtrancl_eq_or_trancl)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   318
    apply(drule tranclD)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   319
    apply(erule exE)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   320
    apply(drule conjunct1)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   321
    apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   322
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   323
    apply(simp)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   324
    apply(case_tac z)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   325
    apply(simp add: RAG2_def RAG_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   326
    apply(clarify)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   327
    apply(simp)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   328
    apply(simp add: next_th_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   329
    apply(rule waiting_unique)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   330
    apply(rule vt)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   331
    apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   332
    apply(rotate_tac 2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   333
    apply(thin_tac "?X")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   334
    apply(subgoal_tac "distinct (wq s cs)")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   335
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   336
    apply(rule wq_distinct)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   337
    apply(rule vt)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   338
    apply (unfold waits2_def waits_def wq_def, auto)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   339
    apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   340
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   341
    apply (metis (mono_tags) set_empty tfl_some)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   342
    apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   343
                set (SOME q. distinct q \<and> set q = set rest)") 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   344
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   345
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   346
    apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   347
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   348
    apply(rule someI2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   349
    apply(auto)[2]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   350
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   351
    apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   352
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   353
    apply (metis (mono_tags) set_empty tfl_some)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   354
    apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in> 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   355
                set (SOME q. distinct q \<and> set q = set rest)") 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   356
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   357
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   358
    apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest") 
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   359
    prefer 2
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   360
    apply(rule someI2)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   361
    apply(auto)[2]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   362
    apply(auto)[1]
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   363
    done
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   364
qed (simp_all)
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   365
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   366
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   367
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   368
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   369
af38526275f8 added a test theory for polishing teh proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   370