CpsG.thy
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 03 Jun 2014 15:00:12 +0100
changeset 40 0781a2fc93f1
parent 35 92f61f6a0fe7
child 45 fc83f79009bd
permissions -rw-r--r--
added a library about graphs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
     1
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
theory CpsG
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
     3
imports PrioG Max
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
lemma not_thread_holdents:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
  fixes th s
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
  and not_in: "th \<notin> threads s" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
  shows "holdents s th = {}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
  from vt not_in show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
  proof(induct arbitrary:th)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
    case (vt_cons s e th)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
    assume vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
      and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
      and stp: "step s e"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
      and not_in: "th \<notin> threads (e # s)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
    from stp show ?case
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
    proof(cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
      case (thread_create thread prio)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
      assume eq_e: "e = Create thread prio"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
        and not_in': "thread \<notin> threads s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
      have "holdents (e # s) th = holdents s th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
        apply (unfold eq_e holdents_test)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
    26
        by (simp add:RAG_create_unchanged)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
      moreover have "th \<notin> threads s" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
        from not_in eq_e show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
      moreover note ih ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
      case (thread_exit thread)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
      assume eq_e: "e = Exit thread"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
      and nh: "holdents s thread = {}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
      show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
      proof(cases "th = thread")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
        case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
        with nh eq_e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
        show ?thesis 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
    41
          by (auto simp:holdents_test RAG_exit_unchanged)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
      next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
        case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
        with not_in and eq_e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
        have "th \<notin> threads s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
        from ih[OF this] False eq_e show ?thesis 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
    47
          by (auto simp:holdents_test RAG_exit_unchanged)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
      case (thread_P thread cs)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
      assume eq_e: "e = P thread cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
      and is_runing: "thread \<in> runing s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
      from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
      have neq_th: "th \<noteq> thread" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
        from not_in eq_e have "th \<notin> threads s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
        moreover from is_runing have "thread \<in> threads s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
          by (simp add:runing_def readys_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
        ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
      hence "holdents (e # s) th  = holdents s th "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
        apply (unfold cntCS_def holdents_test eq_e)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
    63
        by (unfold step_RAG_p[OF vtp], auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
      moreover have "holdents s th = {}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
      proof(rule ih)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
        from not_in eq_e show "th \<notin> threads s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
      ultimately show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
      case (thread_V thread cs)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
      assume eq_e: "e = V thread cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    72
        and is_runing: "thread \<in> runing s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
        and hold: "holding s thread cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    74
      have neq_th: "th \<noteq> thread" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
        from not_in eq_e have "th \<notin> threads s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
        moreover from is_runing have "thread \<in> threads s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
          by (simp add:runing_def readys_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
        ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
      from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
      from hold obtain rest 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
        where eq_wq: "wq s cs = thread # rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
        by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
      from not_in eq_e eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
      have "\<not> next_th s thread cs th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
        apply (auto simp:next_th_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    89
        assume ne: "rest \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
          and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
        have "?t \<in> set rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
        proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
          show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
        next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
          fix x assume "distinct x \<and> set x = set rest" with ne
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
          show "hd x \<in> set rest" by (cases x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
        with eq_wq have "?t \<in> set (wq s cs)" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   100
        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
        show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
      moreover note neq_th eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
      ultimately have "holdents (e # s) th  = holdents s th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   105
        by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
      moreover have "holdents s th = {}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
      proof(rule ih)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
        from not_in eq_e show "th \<notin> threads s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
      ultimately show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
      case (thread_set thread prio)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
      print_facts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   114
      assume eq_e: "e = Set thread prio"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
        and is_runing: "thread \<in> runing s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
      from not_in and eq_e have "th \<notin> threads s" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
      from ih [OF this] and eq_e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
      show ?thesis 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
        apply (unfold eq_e cntCS_def holdents_test)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   120
        by (simp add:RAG_set_unchanged)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
      case vt_nil
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
      show ?case
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   125
      by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   130
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
lemma next_th_neq: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
  and nt: "next_th s th cs th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
  shows "th' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
  from nt show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
    apply (auto simp:next_th_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
    fix rest
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
      and ne: "rest \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   142
    have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   143
    proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
      from wq_distinct[OF vt, of cs] eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
      show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
      fix x
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
      assume "distinct x \<and> set x = set rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
      hence eq_set: "set x = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
      with ne have "x \<noteq> []" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
      hence "hd x \<in> set x" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
      with eq_set show "hd x \<in> set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   154
    with wq_distinct[OF vt, of cs] eq_wq show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   155
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
lemma next_th_unique: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
  assumes nt1: "next_th s th cs th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
  and nt2: "next_th s th cs th2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
  shows "th1 = th2"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   162
using assms by (unfold next_th_def, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   163
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   164
lemma wf_RAG:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   165
  assumes vt: "vt s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   166
  shows "wf (RAG s)"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   167
proof(rule finite_acyclic_wf)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   168
  from finite_RAG[OF vt] show "finite (RAG s)" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
next
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   170
  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   173
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
definition child :: "state \<Rightarrow> (node \<times> node) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   176
  where "child s \<equiv>
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   177
            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
lemma children_def2:
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   183
  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
unfolding child_def children_def by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   186
lemma children_dependants: 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   187
  "children s th \<subseteq> dependants (wq s) th"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   188
  unfolding children_def2
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   189
  unfolding cs_dependants_def
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   190
  by (auto simp add: eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
lemma child_unique:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
  and ch1: "(Th th, Th th1) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
  and ch2: "(Th th, Th th2) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
  shows "th1 = th2"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   197
using ch1 ch2 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   198
proof(unfold child_def, clarsimp)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   199
  fix cs csa
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   200
  assume h1: "(Th th, Cs cs) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   201
    and h2: "(Cs cs, Th th1) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   202
    and h3: "(Th th, Cs csa) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   203
    and h4: "(Cs csa, Th th2) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   204
  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   205
  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   206
  from unique_RAG[OF vt h2 this]
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   207
  show "th1 = th2" by simp
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   208
qed 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   210
lemma RAG_children:
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   211
  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   212
  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
  from h show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
  proof(induct rule: tranclE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
    fix c th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   217
    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   218
    and h2: "(c, Th th2) \<in> RAG s"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
    from h2 obtain cs where eq_c: "c = Cs cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   220
      by (case_tac c, auto simp:s_RAG_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   221
    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
    proof(rule tranclE[OF h1])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
      fix ca
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   224
      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   225
        and h4: "(ca, c) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   226
      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   229
          by (case_tac ca, auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
        from eq_ca h4 h2 eq_c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
        have "th3 \<in> children s th2" by (auto simp:children_def child_def)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   232
        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
        ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
    next
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   236
      assume "(Th th1, c) \<in> RAG s"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
      with h2 eq_c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
      have "th1 \<in> children s th2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
        by (auto simp:children_def child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
      thus ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
  next
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   243
    assume "(Th th1, Th th2) \<in> RAG s"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
    thus ?thesis
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   245
      by (auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   249
lemma sub_child: "child s \<subseteq> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
  by (unfold child_def, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   251
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   252
lemma wf_child: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
  shows "wf (child s)"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   255
apply(rule wf_subset)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   256
apply(rule wf_trancl[OF wf_RAG[OF vt]])
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   257
apply(rule sub_child)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   258
done
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   259
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   260
lemma RAG_child_pre:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
  shows
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   263
  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   265
  from wf_trancl[OF wf_RAG[OF vt]]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   266
  have wf: "wf ((RAG s)^+)" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
  show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
  proof(rule wf_induct[OF wf, of ?P], clarsimp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
    fix th'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   270
    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   271
               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   272
    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
    show "(Th th, Th th') \<in> (child s)\<^sup>+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
    proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   275
      from RAG_children[OF h]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   276
      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   277
      thus ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   278
      proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   279
        assume "th \<in> children s th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   280
        thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   281
      next
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   282
        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   283
        then obtain th3 where th3_in: "th3 \<in> children s th'" 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   284
          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   285
        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   286
        from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   287
        with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   288
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   292
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   293
lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   294
  by (insert RAG_child_pre, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   296
lemma child_RAG_p:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
  assumes "(n1, n2) \<in> (child s)^+"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   298
  shows "(n1, n2) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
  from assms show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   301
  proof(induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   302
    case (base y)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   303
    with sub_child show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   305
    case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
    assume "(y, z) \<in> child s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   307
    with sub_child have "(y, z) \<in> (RAG s)^+" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   308
    moreover have "(n1, y) \<in> (RAG s)^+" by fact
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
    ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   311
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   313
lemma child_RAG_eq: 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   314
  assumes vt: "vt s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   315
  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   316
  by (auto intro: RAG_child[OF vt] child_RAG_p)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   317
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   318
lemma children_no_dep:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   319
  fixes s th th1 th2 th3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   320
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   321
  and ch1: "(Th th1, Th th) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   322
  and ch2: "(Th th2, Th th) \<in> child s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   323
  and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   324
  shows "False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   325
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   326
  from RAG_child[OF vt ch3]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   327
  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   328
  thus ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   329
  proof(rule converse_tranclE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   330
    assume "(Th th1, Th th2) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   331
    from child_unique[OF vt ch1 this] have "th = th2" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   332
    with ch2 have "(Th th2, Th th2) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   333
    with wf_child[OF vt] show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   334
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   335
    fix c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   336
    assume h1: "(Th th1, c) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   337
      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   338
    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   339
    with h1 have "(Th th1, Th th3) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   340
    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   341
    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   342
    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   343
    moreover have "wf ((child s)\<^sup>+)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   344
    proof(rule wf_trancl)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   345
      from wf_child[OF vt] show "wf (child s)" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   346
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   347
    ultimately show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   348
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   349
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   350
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   351
lemma unique_RAG_p:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   352
  assumes vt: "vt s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   353
  and dp1: "(n, n1) \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   354
  and dp2: "(n, n2) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   355
  and neq: "n1 \<noteq> n2"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   356
  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   357
proof(rule unique_chain [OF _ dp1 dp2 neq])
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   358
  from unique_RAG[OF vt]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   359
  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   360
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   361
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   362
lemma dependants_child_unique:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   363
  fixes s th th1 th2 th3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   364
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   365
  and ch1: "(Th th1, Th th) \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   366
  and ch2: "(Th th2, Th th) \<in> child s"
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   367
  and dp1: "th3 \<in> dependants s th1"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   368
  and dp2: "th3 \<in> dependants s th2"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   369
shows "th1 = th2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   370
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   371
  { assume neq: "th1 \<noteq> th2"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   372
    from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   373
      by (simp add:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   374
    from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   375
      by (simp add:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   376
    from unique_RAG_p[OF vt dp1 dp2] and neq
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   377
    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   378
    hence False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   379
    proof
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   380
      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   381
      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   382
    next
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   383
      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   384
      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   385
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   386
  } thus ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   387
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   388
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   389
lemma RAG_plus_elim:
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   390
  assumes "vt s"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   391
  fixes x
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   392
  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   393
  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   394
  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   395
  apply (unfold children_def)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   396
  by (metis assms(2) children_def RAG_children eq_RAG)
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   397
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   398
lemma dependants_expand:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   399
  assumes "vt s"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   400
  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   401
apply(simp add: image_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   402
unfolding cs_dependants_def
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   403
apply(auto)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   404
apply (metis assms RAG_plus_elim mem_Collect_eq)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   405
apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   406
by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   407
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   408
lemma finite_children:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   409
  assumes "vt s"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   410
  shows "finite (children s th)"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   411
  using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   412
  by (metis rev_finite_subset)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   413
  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   414
lemma finite_dependants:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   415
  assumes "vt s"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   416
  shows "finite (dependants (wq s) th')"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   417
  using dependants_threads[OF assms] finite_threads[OF assms]
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   418
  by (metis rev_finite_subset)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   419
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   420
abbreviation
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   421
  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   422
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   423
abbreviation
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   424
  "cpreceds s ths \<equiv> (cp s) ` ths"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   425
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   426
lemma Un_compr:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   427
  "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   428
by auto
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   429
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   430
lemma in_disj:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   431
  shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   432
by metis
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   433
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   434
lemma UN_exists:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   435
  shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   436
by auto
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   437
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   438
lemma cp_rec:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   439
  fixes s th
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   440
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   441
  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   442
proof(cases "children s th = {}")
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   443
  case True
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   444
  show ?thesis
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   445
    unfolding cp_eq_cpreced cpreced_def 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   446
    by (subst dependants_expand[OF `vt s`]) (simp add: True)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   447
next
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   448
  case False
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   449
  show ?thesis (is "?LHS = ?RHS")
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   450
  proof -
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   451
    have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   452
      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   453
  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   454
    have not_emptyness_facts[simp]: 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   455
      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   456
      using False dependants_expand[OF assms] by(auto simp only: Un_empty)
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   457
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   458
    have finiteness_facts[simp]:
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   459
      "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   460
      by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   461
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   462
    (* expanding definition *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   463
    have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   464
      unfolding eq_cp by (simp add: Un_compr)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   465
    
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   466
    (* moving Max in *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   467
    also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   468
      by (simp add: Max_Un)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   469
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   470
    (* expanding dependants *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   471
    also have "\<dots> = max (Max {preced th s}) 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   472
      (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   473
      by (subst dependants_expand[OF `vt s`]) (simp)
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   474
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   475
    (* moving out big Union *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   476
    also have "\<dots> = max (Max {preced th s})
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   477
      (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   478
      by simp
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   479
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   480
    (* moving in small union *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   481
    also have "\<dots> = max (Max {preced th s})
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   482
      (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   483
      by (simp add: in_disj)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   484
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   485
    (* moving in preceds *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   486
    also have "\<dots> = max (Max {preced th s})  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   487
      (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   488
      by (simp add: UN_exists)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   489
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   490
    (* moving in Max *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   491
    also have "\<dots> = max (Max {preced th s})  
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   492
      (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   493
      by (subst Max_Union) (auto simp add: image_image)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   494
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   495
    (* folding cp + moving out Max *)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   496
    also have "\<dots> = ?RHS" 
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   497
      unfolding eq_cp by (simp add: Max_insert)
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   498
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
   499
    finally show "?LHS = ?RHS" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   500
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   501
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   502
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   503
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   504
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   505
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   506
locale step_set_cps =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   507
  fixes s' th prio s 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   508
  defines s_def : "s \<equiv> (Set th prio#s')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   509
  assumes vt_s: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   510
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   511
context step_set_cps 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   512
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   513
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   514
lemma eq_preced:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   515
  fixes th'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   516
  assumes "th' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   517
  shows "preced th' s = preced th' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   518
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   519
  from assms show ?thesis 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   520
    by (unfold s_def, auto simp:preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   521
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   522
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   523
lemma eq_dep: "RAG s = RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   524
  by (unfold s_def RAG_set_unchanged, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   525
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   526
lemma eq_cp_pre:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   527
  fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   528
  assumes neq_th: "th' \<noteq> th"
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   529
  and nd: "th \<notin> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   530
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   531
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   532
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   533
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   534
    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   535
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   536
    fix th1 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   537
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   538
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   539
    hence "preced th1 s = preced th1 s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   540
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   541
      assume "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   542
      with eq_preced[OF neq_th]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   543
      show "preced th1 s = preced th1 s'" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   544
    next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   545
      assume "th1 \<in> dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   546
      with nd and eq_dp have "th1 \<noteq> th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   547
        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   548
      from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   549
    qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   550
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   551
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   552
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   553
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   554
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   555
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   556
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   557
lemma no_dependants:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   558
  assumes "th' \<noteq> th"
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   559
  shows "th \<notin> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   560
proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   561
  assume h: "th \<in> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   562
  from step_back_step [OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   563
  have "step s' (Set th prio)" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   564
  hence "th \<in> runing s'" by (cases, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   565
  hence rd_th: "th \<in> readys s'" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   566
    by (simp add:readys_def runing_def)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   567
  from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   568
    by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   569
  from tranclD[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   570
  obtain z where "(Th th, z) \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   571
  with rd_th show "False"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   572
    apply (case_tac z, auto simp:readys_def s_waiting_def s_RAG_def s_waiting_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   573
    by (fold wq_def, blast)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   574
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   575
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   576
(* Result improved *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   577
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   578
 fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   579
  assumes neq_th: "th' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   580
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   581
proof(rule eq_cp_pre [OF neq_th])
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   582
  from no_dependants[OF neq_th] 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   583
  show "th \<notin> dependants s th'" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   584
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   585
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   586
lemma eq_up:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   587
  fixes th' th''
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   588
  assumes dp1: "th \<in> dependants s th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   589
  and dp2: "th' \<in> dependants s th''"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   590
  and eq_cps: "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   591
  shows "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   592
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   593
  from dp2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   594
  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   595
  from RAG_child[OF vt_s this[unfolded eq_RAG]]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   596
  have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   597
  moreover { fix n th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   598
    have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   599
                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   600
    proof(erule trancl_induct, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   601
      fix y th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   602
      assume y_ch: "(y, Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   603
        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   604
        and ch': "(Th th', y) \<in> (child s)\<^sup>+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   605
      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   606
      with ih have eq_cpy:"cp s thy = cp s' thy" by blast
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   607
      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   608
      moreover from child_RAG_p[OF ch'] and eq_y
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   609
      have "(Th th', Th thy) \<in> (RAG s)^+" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   610
      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   611
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   612
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   613
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   614
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   615
        proof(rule eq_preced)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   616
          show "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   617
          proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   618
            assume "th'' = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   619
            with dp_thy y_ch[unfolded eq_y] 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   620
            have "(Th th, Th th) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   621
              by (auto simp:child_def)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   622
            with wf_trancl[OF wf_RAG[OF vt_s]] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   623
            show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   624
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   625
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   626
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   627
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   628
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   629
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   630
          proof(cases "th1 = thy")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   631
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   632
            with eq_cpy show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   633
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   634
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   635
            have neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   636
            proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   637
              assume eq_th1: "th1 = th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   638
              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   639
              from children_no_dep[OF vt_s _ _ this] and 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   640
              th1_in y_ch eq_y show False by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   641
            qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   642
            have "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   643
            proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   644
              assume h:"th \<in> dependants s th1"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   645
              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   646
              from dependants_child_unique[OF vt_s _ _ h this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   647
              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   648
              with False show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   649
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   650
            from eq_cp_pre[OF neq_th1 this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   651
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   652
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   653
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   654
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   655
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   656
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   657
          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   658
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   659
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   660
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   661
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   662
      fix th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   663
      assume dp': "(Th th', Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   664
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   665
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   666
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   667
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   668
        proof(rule eq_preced)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   669
          show "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   670
          proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   671
            assume "th'' = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   672
            with dp1 dp'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   673
            have "(Th th, Th th) \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   674
              by (auto simp:child_def s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   675
            with wf_trancl[OF wf_RAG[OF vt_s]] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   676
            show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   677
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   678
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   679
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   680
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   681
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   682
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   683
          proof(cases "th1 = th'")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   684
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   685
            with eq_cps show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   686
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   687
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   688
            have neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   689
            proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   690
              assume eq_th1: "th1 = th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   691
              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   692
                by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   693
              from children_no_dep[OF vt_s _ _ this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   694
              th1_in dp'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   695
              show False by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   696
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   697
            thus ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   698
            proof(rule eq_cp_pre)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   699
              show "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   700
              proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   701
                assume "th \<in> dependants s th1"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   702
                from dependants_child_unique[OF vt_s _ _ this dp1]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   703
                th1_in dp' have "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   704
                  by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   705
                with False show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   706
              qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   707
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   708
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   709
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   710
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   711
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   712
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   713
          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   714
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   715
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   716
      qed     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   717
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   718
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   719
  ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   720
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   721
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   722
lemma eq_up_self:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   723
  fixes th' th''
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   724
  assumes dp: "th \<in> dependants s th''"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   725
  and eq_cps: "cp s th = cp s' th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   726
  shows "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   727
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   728
  from dp
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   729
  have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   730
  from RAG_child[OF vt_s this[unfolded eq_RAG]]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   731
  have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   732
  moreover { fix n th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   733
    have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   734
                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   735
    proof(erule trancl_induct, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   736
      fix y th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   737
      assume y_ch: "(y, Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   738
        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   739
        and ch': "(Th th, y) \<in> (child s)\<^sup>+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   740
      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   741
      with ih have eq_cpy:"cp s thy = cp s' thy" by blast
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   742
      from child_RAG_p[OF ch'] and eq_y
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   743
      have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   744
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   745
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   746
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   747
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   748
        proof(rule eq_preced)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   749
          show "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   750
          proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   751
            assume "th'' = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   752
            with dp_thy y_ch[unfolded eq_y] 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   753
            have "(Th th, Th th) \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   754
              by (auto simp:child_def)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   755
            with wf_trancl[OF wf_RAG[OF vt_s]] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   756
            show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   757
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   758
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   759
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   760
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   761
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   762
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   763
          proof(cases "th1 = thy")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   764
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   765
            with eq_cpy show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   766
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   767
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   768
            have neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   769
            proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   770
              assume eq_th1: "th1 = th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   771
              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   772
              from children_no_dep[OF vt_s _ _ this] and 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   773
              th1_in y_ch eq_y show False by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   774
            qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   775
            have "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   776
            proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   777
              assume h:"th \<in> dependants s th1"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   778
              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   779
              from dependants_child_unique[OF vt_s _ _ h this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   780
              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   781
              with False show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   782
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   783
            from eq_cp_pre[OF neq_th1 this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   784
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   785
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   786
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   787
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   788
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   789
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   790
          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   791
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   792
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   793
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   794
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   795
      fix th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   796
      assume dp': "(Th th, Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   797
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   798
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   799
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   800
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   801
        proof(rule eq_preced)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   802
          show "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   803
          proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   804
            assume "th'' = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   805
            with dp dp'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   806
            have "(Th th, Th th) \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   807
              by (auto simp:child_def s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   808
            with wf_trancl[OF wf_RAG[OF vt_s]] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   809
            show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   810
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   811
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   812
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   813
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   814
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   815
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   816
          proof(cases "th1 = th")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   817
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   818
            with eq_cps show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   819
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   820
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   821
            assume neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   822
            thus ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   823
            proof(rule eq_cp_pre)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   824
              show "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   825
              proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   826
                assume "th \<in> dependants s th1"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   827
                hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   828
                from children_no_dep[OF vt_s _ _ this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   829
                and th1_in dp' show False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   830
                  by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   831
              qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   832
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   833
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   834
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   835
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   836
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   837
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   838
          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   839
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   840
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   841
      qed     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   842
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   843
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   844
  ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   845
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   846
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   847
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   848
lemma next_waiting:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   849
  assumes vt: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   850
  and nxt: "next_th s th cs th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   851
  shows "waiting s th' cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   852
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   853
  from assms show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   854
    apply (auto simp:next_th_def s_waiting_def[folded wq_def])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   855
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   856
    fix rest
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   857
    assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   858
      and eq_wq: "wq s cs = th # rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   859
      and ne: "rest \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   860
    have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   861
    proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   862
      from wq_distinct[OF vt, of cs] eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   863
      show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   864
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   865
      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   866
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   867
    with ni
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   868
    have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   869
      by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   870
    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   871
    proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   872
      from wq_distinct[OF vt, of cs] eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   873
      show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   874
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   875
      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   876
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   877
    ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   878
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   879
    fix rest
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   880
    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   881
      and ne: "rest \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   882
    have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   883
    proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   884
      from wq_distinct[OF vt, of cs] eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   885
      show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   886
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   887
      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   888
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   889
    hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   890
      by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   891
    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   892
    proof(rule someI2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   893
      from wq_distinct[OF vt, of cs] eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   894
      show "distinct rest \<and> set rest = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   895
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   896
      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   897
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   898
    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   899
    with eq_wq and wq_distinct[OF vt, of cs]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   900
    show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   901
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   902
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   903
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   904
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   905
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   906
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   907
locale step_v_cps =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   908
  fixes s' th cs s 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   909
  defines s_def : "s \<equiv> (V th cs#s')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   910
  assumes vt_s: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   911
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   912
locale step_v_cps_nt = step_v_cps +
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   913
  fixes th'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   914
  assumes nt: "next_th s' th cs th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   915
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   916
context step_v_cps_nt
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   917
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   918
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   919
lemma RAG_s:
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   920
  "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   921
                                         {(Cs cs, Th th')}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   922
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   923
  from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   924
    and nt show ?thesis  by (auto intro:next_th_unique)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   925
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   926
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   927
lemma dependants_kept:
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   928
  fixes th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   929
  assumes neq1: "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   930
  and neq2: "th'' \<noteq> th'"
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   931
  shows "dependants (wq s) th'' = dependants (wq s') th''"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   932
proof(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   933
  fix x
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
   934
  assume "x \<in> dependants (wq s) th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   935
  hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   936
    by (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   937
  { fix n
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   938
    have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s')^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   939
    proof(induct rule:converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   940
      fix y 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   941
      assume "(y, Th th'') \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   942
      with RAG_s neq1 neq2
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   943
      have "(y, Th th'') \<in> RAG s'" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   944
      thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   945
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   946
      fix y z 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   947
      assume yz: "(y, z) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   948
        and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   949
        and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   950
      have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   951
      proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   952
        show "y \<noteq> Cs cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   953
        proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   954
          assume eq_y: "y = Cs cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   955
          with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   956
          from RAG_s
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   957
          have cst': "(Cs cs, Th th') \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   958
          from unique_RAG[OF vt_s this dp_yz] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   959
          have eq_z: "z = Th th'" by simp
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   960
          with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   961
          from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   962
          obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   963
            by (auto simp:s_RAG_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   964
          with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   965
          from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG s)^+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   966
          moreover have "cs' = cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   967
          proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   968
            from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   969
            have "(Th th', Cs cs) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   970
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   971
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   972
            show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   973
          qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   974
          ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   975
          moreover note wf_trancl[OF wf_RAG[OF vt_s]]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   976
          ultimately show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   977
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   978
      next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   979
        show "y \<noteq> Th th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   980
        proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   981
          assume eq_y: "y = Th th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   982
          with yz have dps: "(Th th', z) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   983
          with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   984
          have "z = Cs cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   985
          proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   986
            from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   987
            have "(Th th', Cs cs) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   988
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   989
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   990
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   991
          qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   992
          with dps RAG_s show False by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   993
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   994
      qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   995
      with RAG_s yz have "(y, z) \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   996
      with ztp'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
   997
      show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   998
    qed    
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   999
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1000
  from this[OF dp]
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1001
  show "x \<in> dependants (wq s') th''" 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1002
    by (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1003
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1004
  fix x
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1005
  assume "x \<in> dependants (wq s') th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1006
  hence dp: "(Th x, Th th'') \<in> (RAG s')^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1007
    by (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1008
  { fix n
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1009
    have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s)^+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1010
    proof(induct rule:converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1011
      fix y 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1012
      assume "(y, Th th'') \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1013
      with RAG_s neq1 neq2
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1014
      have "(y, Th th'') \<in> RAG s" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1015
      thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1016
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1017
      fix y z 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1018
      assume yz: "(y, z) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1019
        and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1020
        and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1021
      have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1022
      proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1023
        show "y \<noteq> Cs cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1024
        proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1025
          assume eq_y: "y = Cs cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1026
          with yz have dp_yz: "(Cs cs, z) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1027
          from this have eq_z: "z = Th th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1028
          proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1029
            from step_back_step[OF vt_s[unfolded s_def]]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1030
            have "(Cs cs, Th th) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1031
              by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1032
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1033
            show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1034
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1035
          from converse_tranclE[OF ztp]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1036
          obtain u where "(z, u) \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1037
          moreover 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1038
          from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1039
          have "th \<in> readys s'" by (cases, simp add:runing_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1040
          moreover note eq_z
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1041
          ultimately show False 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1042
            by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1043
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1044
      next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1045
        show "y \<noteq> Th th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1046
        proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1047
          assume eq_y: "y = Th th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1048
          with yz have dps: "(Th th', z) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1049
          have "z = Cs cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1050
          proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1051
            from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1052
            have "(Th th', Cs cs) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1053
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1054
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1055
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1056
          qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1057
          with ztp have cs_i: "(Cs cs, Th th'') \<in>  (RAG s')\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1058
          from step_back_step[OF vt_s[unfolded s_def]]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1059
          have cs_th: "(Cs cs, Th th) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1060
            by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1061
          have "(Cs cs, Th th'') \<notin>  RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1062
          proof
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1063
            assume "(Cs cs, Th th'') \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1064
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1065
            and neq1 show "False" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1066
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1067
          with converse_tranclE[OF cs_i]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1068
          obtain u where cu: "(Cs cs, u) \<in> RAG s'"  
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1069
            and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1070
          have "u = Th th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1071
          proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1072
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1073
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1074
          qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1075
          with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1076
          from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1077
          obtain v where "(Th th, v) \<in> (RAG s')" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1078
          moreover from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1079
          have "th \<in> readys s'" by (cases, simp add:runing_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1080
          ultimately show False 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1081
            by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1082
        qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1083
      qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1084
      with RAG_s yz have "(y, z) \<in> RAG s" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1085
      with ztp'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1086
      show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1087
    qed    
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1088
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1089
  from this[OF dp]
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1090
  show "x \<in> dependants (wq s) th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1091
    by (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1092
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1093
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1094
lemma cp_kept:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1095
  fixes th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1096
  assumes neq1: "th'' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1097
  and neq2: "th'' \<noteq> th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1098
  shows "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1099
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1100
  from dependants_kept[OF neq1 neq2]
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1101
  have "dependants (wq s) th'' = dependants (wq s') th''" .
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1102
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1103
    fix th1
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1104
    assume "th1 \<in> dependants (wq s) th''"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1105
    have "preced th1 s = preced th1 s'" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1106
      by (unfold s_def, auto simp:preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1107
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1108
  moreover have "preced th'' s = preced th'' s'" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1109
    by (unfold s_def, auto simp:preced_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1110
  ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1111
    ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1112
    by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1113
  thus ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1114
    by (unfold cp_eq_cpreced cpreced_def, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1115
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1116
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1117
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1119
locale step_v_cps_nnt = step_v_cps +
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1120
  assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1121
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1122
context step_v_cps_nnt
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1123
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1124
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1125
lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1126
proof
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1127
  assume "(Th th1, Cs cs) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1128
  thus "False"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1129
    apply (auto simp:s_RAG_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1130
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1131
    assume h1: "th1 \<in> set (wq s' cs)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1132
      and h2: "th1 \<noteq> hd (wq s' cs)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1133
    from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1134
    show "False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1135
    proof(cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1136
      assume "holding s' th cs" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1137
      then obtain rest where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1138
        eq_wq: "wq s' cs = th#rest"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1139
        apply (unfold s_holding_def wq_def[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1140
        by (case_tac "(wq s' cs)", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1141
      with h1 h2 have ne: "rest \<noteq> []" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1142
      with eq_wq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1143
      have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1144
        by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1145
      with nnt show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1146
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1147
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1148
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1149
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1150
lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1151
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1152
  from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1153
  show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1154
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1155
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1156
lemma child_kept_left:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1157
  assumes 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1158
  "(n1, n2) \<in> (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1159
  shows "(n1, n2) \<in> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1160
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1161
  from assms show ?thesis 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1162
  proof(induct rule: converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1163
    case (base y)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1164
    from base obtain th1 cs1 th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1165
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1166
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1167
      and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1168
    have "cs1 \<noteq> cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1169
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1170
      assume eq_cs: "cs1 = cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1171
      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1172
      with nw_cs eq_cs show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1173
    qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1174
    with h1 h2 RAG_s have 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1175
      h1': "(Th th1, Cs cs1) \<in> RAG s" and
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1176
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1177
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1178
    with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1179
    thus ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1180
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1181
    case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1182
    have "(y, z) \<in> child s'" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1183
    then obtain th1 cs1 th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1184
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1185
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1186
      and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1187
    have "cs1 \<noteq> cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1188
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1189
      assume eq_cs: "cs1 = cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1190
      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1191
      with nw_cs eq_cs show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1192
    qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1193
    with h1 h2 RAG_s have 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1194
      h1': "(Th th1, Cs cs1) \<in> RAG s" and
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1195
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1196
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1197
    with eq_y eq_z have "(y, z) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1198
    moreover have "(z, n2) \<in> (child s)^+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1199
    ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1200
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1201
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1202
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1203
lemma  child_kept_right:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1204
  assumes
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1205
  "(n1, n2) \<in> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1206
  shows "(n1, n2) \<in> (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1207
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1208
  from assms show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1209
  proof(induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1210
    case (base y)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1211
    from base and RAG_s 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1212
    have "(n1, y) \<in> child s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1213
      by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1214
    thus ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1215
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1216
    case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1217
    have "(y, z) \<in> child s" by fact
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1218
    with RAG_s have "(y, z) \<in> child s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1219
      by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1220
    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1221
    ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1222
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1223
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1224
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1225
lemma eq_child: "(child s)^+ = (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1226
  by (insert child_kept_left child_kept_right, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1227
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1228
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1229
  fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1230
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1231
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1232
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1233
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1234
    apply (unfold cs_dependants_def, unfold eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1235
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1236
    from eq_child
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1237
    have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1238
      by simp
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1239
    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1240
    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1241
      by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1242
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1243
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1244
    fix th1 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1245
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1246
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1247
    hence "preced th1 s = preced th1 s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1248
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1249
      assume "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1250
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1251
    next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1252
      assume "th1 \<in> dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1253
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1254
    qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1255
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1256
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1257
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1258
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1259
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1260
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1261
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1262
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1263
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1264
locale step_P_cps =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1265
  fixes s' th cs s 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1266
  defines s_def : "s \<equiv> (P th cs#s')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1267
  assumes vt_s: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1268
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1269
locale step_P_cps_ne =step_P_cps +
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1270
  assumes ne: "wq s' cs \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1272
locale step_P_cps_e =step_P_cps +
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1273
  assumes ee: "wq s' cs = []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1274
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1275
context step_P_cps_e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1276
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1277
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1278
lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1279
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1280
  from ee and  step_RAG_p[OF vt_s[unfolded s_def], folded s_def]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1281
  show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1282
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1283
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1284
lemma child_kept_left:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1285
  assumes 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1286
  "(n1, n2) \<in> (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1287
  shows "(n1, n2) \<in> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1288
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1289
  from assms show ?thesis 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1290
  proof(induct rule: converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1291
    case (base y)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1292
    from base obtain th1 cs1 th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1293
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1294
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1295
      and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1296
    have "cs1 \<noteq> cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1297
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1298
      assume eq_cs: "cs1 = cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1299
      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1300
      with ee show False
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1301
        by (auto simp:s_RAG_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1302
    qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1303
    with h1 h2 RAG_s have 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1304
      h1': "(Th th1, Cs cs1) \<in> RAG s" and
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1305
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1306
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1307
    with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1308
    thus ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1309
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1310
    case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1311
    have "(y, z) \<in> child s'" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1312
    then obtain th1 cs1 th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1313
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1314
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1315
      and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1316
    have "cs1 \<noteq> cs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1317
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1318
      assume eq_cs: "cs1 = cs"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1319
      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1320
      with ee show False 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1321
        by (auto simp:s_RAG_def cs_waiting_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1322
    qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1323
    with h1 h2 RAG_s have 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1324
      h1': "(Th th1, Cs cs1) \<in> RAG s" and
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1325
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1326
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1327
    with eq_y eq_z have "(y, z) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1328
    moreover have "(z, n2) \<in> (child s)^+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1329
    ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1330
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1331
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1332
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1333
lemma  child_kept_right:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1334
  assumes
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1335
  "(n1, n2) \<in> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1336
  shows "(n1, n2) \<in> (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1337
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1338
  from assms show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1339
  proof(induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1340
    case (base y)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1341
    from base and RAG_s
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1342
    have "(n1, y) \<in> child s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1343
      apply (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1344
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1345
        fix th'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1346
        assume "(Th th', Cs cs) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1347
        with ee have "False"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1348
          by (auto simp:s_RAG_def cs_waiting_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1349
        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1350
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1351
    thus ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1352
  next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1353
    case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1354
    have "(y, z) \<in> child s" by fact
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1355
    with RAG_s have "(y, z) \<in> child s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1356
      apply (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1357
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1358
        fix th'
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1359
        assume "(Th th', Cs cs) \<in> RAG s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1360
        with ee have "False"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1361
          by (auto simp:s_RAG_def cs_waiting_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1362
        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1363
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1364
    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1365
    ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1366
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1367
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1368
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1369
lemma eq_child: "(child s)^+ = (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1370
  by (insert child_kept_left child_kept_right, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1371
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1372
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1373
  fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1374
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1375
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1376
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1377
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1378
    apply (unfold cs_dependants_def, unfold eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1379
  proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1380
    from eq_child
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1381
    have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1382
      by auto
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1383
    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1384
    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1385
      by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1386
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1387
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1388
    fix th1 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1389
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1390
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1391
    hence "preced th1 s = preced th1 s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1392
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1393
      assume "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1394
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1395
    next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1396
      assume "th1 \<in> dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1397
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1398
    qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1399
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1400
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1401
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1402
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1403
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1404
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1405
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1406
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1407
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1408
context step_P_cps_ne
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1409
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1410
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1411
lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1412
proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1413
  from step_RAG_p[OF vt_s[unfolded s_def]] and ne
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1414
  show ?thesis by (simp add:s_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1415
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1416
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1417
lemma eq_child_left:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1418
  assumes nd: "(Th th, Th th') \<notin> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1419
  shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1420
proof(induct rule:converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1421
  case (base y)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1422
  from base obtain th1 cs1
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1423
    where h1: "(Th th1, Cs cs1) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1424
    and h2: "(Cs cs1, Th th') \<in> RAG s"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1425
    and eq_y: "y = Th th1"   by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1426
  have "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1427
  proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1428
    assume "th1 = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1429
    with base eq_y have "(Th th, Th th') \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1430
    with nd show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1431
  qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1432
  with h1 h2 RAG_s 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1433
  have h1': "(Th th1, Cs cs1) \<in> RAG s'" and 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1434
       h2': "(Cs cs1, Th th') \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1435
  with eq_y show ?case by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1436
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1437
  case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1438
  have yz: "(y, z) \<in> child s" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1439
  then obtain th1 cs1 th2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1440
    where h1: "(Th th1, Cs cs1) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1441
    and h2: "(Cs cs1, Th th2) \<in> RAG s"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1442
    and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1443
  have "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1444
  proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1445
    assume "th1 = th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1446
    with yz eq_y have "(Th th, z) \<in> child s" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1447
    moreover have "(z, Th th') \<in> (child s)^+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1448
    ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1449
    with nd show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1450
  qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1451
  with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1452
                       and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1453
  with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1454
  moreover have "(z, Th th') \<in> (child s')^+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1455
  ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1456
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1457
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1458
lemma eq_child_right:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1459
  shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1460
proof(induct rule:converse_trancl_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1461
  case (base y)
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1462
  with RAG_s show ?case by (auto simp:child_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1463
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1464
  case (step y z)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1465
  have "(y, z) \<in> child s'" by fact
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1466
  with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1467
  moreover have "(z, Th th') \<in> (child s)^+" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1468
  ultimately show ?case by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1469
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1470
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1471
lemma eq_child:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1472
  assumes nd: "(Th th, Th th') \<notin> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1473
  shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1474
  by (insert eq_child_left[OF nd] eq_child_right, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1475
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1476
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1477
  fixes th' 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1478
  assumes nd: "th \<notin> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1479
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1480
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1481
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1482
  have nd': "(Th th, Th th') \<notin> (child s)^+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1483
  proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1484
    assume "(Th th, Th th') \<in> (child s)\<^sup>+"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1485
    with child_RAG_eq[OF vt_s]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1486
    have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1487
    with nd show False 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1488
      by (simp add:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1489
  qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1490
  have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1491
  proof(auto)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1492
    fix x assume " x \<in> dependants (wq s) th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1493
    thus "x \<in> dependants (wq s') th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1494
      apply (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1495
    proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1496
      assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1497
      with  child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1498
      with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1499
      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1500
      show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1501
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1502
  next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1503
    fix x assume "x \<in> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1504
    thus "x \<in> dependants (wq s) th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1505
      apply (auto simp:cs_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1506
    proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1507
      assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1508
      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1509
      have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1510
      with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1511
      with  child_RAG_eq[OF vt_s]
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1512
      show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1513
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1514
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1515
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1516
    fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1517
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1518
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1519
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1520
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1521
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1522
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1523
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1524
lemma eq_up:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1525
  fixes th' th''
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1526
  assumes dp1: "th \<in> dependants s th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1527
  and dp2: "th' \<in> dependants s th''"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1528
  and eq_cps: "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1529
  shows "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1530
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1531
  from dp2
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1532
  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1533
  from RAG_child[OF vt_s this[unfolded eq_RAG]]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1534
  have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1535
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1536
    fix n th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1537
    have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1538
                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1539
    proof(erule trancl_induct, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1540
      fix y th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1541
      assume y_ch: "(y, Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1542
        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1543
        and ch': "(Th th', y) \<in> (child s)\<^sup>+"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1544
      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1545
      with ih have eq_cpy:"cp s thy = cp s' thy" by blast
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1546
      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1547
      moreover from child_RAG_p[OF ch'] and eq_y
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1548
      have "(Th th', Th thy) \<in> (RAG s)^+" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1549
      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1550
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1551
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1552
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1553
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1554
          by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1555
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1556
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1557
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1558
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1559
          proof(cases "th1 = thy")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1560
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1561
            with eq_cpy show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1562
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1563
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1564
            have neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1565
            proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1566
              assume eq_th1: "th1 = th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1567
              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1568
              from children_no_dep[OF vt_s _ _ this] and 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1569
              th1_in y_ch eq_y show False by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1570
            qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1571
            have "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1572
            proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1573
              assume h:"th \<in> dependants s th1"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1574
              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1575
              from dependants_child_unique[OF vt_s _ _ h this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1576
              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1577
              with False show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1578
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1579
            from eq_cp[OF this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1580
            show ?thesis .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1581
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1582
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1583
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1584
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1585
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1586
          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1587
          apply (fold s_def, auto simp:RAG_s)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1588
          proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1589
            assume "(Cs cs, Th th'') \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1590
            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1591
            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1592
              by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1593
            from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1594
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1595
              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1596
              by (auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1597
            have eq_cs: "cs1 = cs" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1598
            proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1599
              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1600
              from unique_RAG[OF vt_s this h1]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1601
              show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1602
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1603
            have False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1604
            proof(rule converse_tranclE[OF h2])
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1605
              assume "(Cs cs1, Th th') \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1606
              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1607
              from unique_RAG[OF vt_s this cs_th']
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1608
              have "th' = th''" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1609
              with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1610
              with wf_trancl[OF wf_child[OF vt_s]] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1611
              show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1612
            next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1613
              fix y
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1614
              assume "(Cs cs1, y) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1615
                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1616
              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1617
              from unique_RAG[OF vt_s this cs_th']
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1618
              have "y = Th th''" .
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1619
              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1620
              from RAG_child[OF vt_s this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1621
              have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1622
              moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1623
              ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1624
              with wf_trancl[OF wf_child[OF vt_s]] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1625
              show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1626
            qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1627
            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1628
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1629
          ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1630
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1631
      qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1632
    next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1633
      fix th''
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1634
      assume dp': "(Th th', Th th'') \<in> child s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1635
      show "cp s th'' = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1636
        apply (subst cp_rec[OF vt_s])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1637
      proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1638
        have "preced th'' s = preced th'' s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1639
          by (simp add:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1640
        moreover { 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1641
          fix th1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1642
          assume th1_in: "th1 \<in> children s th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1643
          have "cp s th1 = cp s' th1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1644
          proof(cases "th1 = th'")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1645
            case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1646
            with eq_cps show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1647
          next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1648
            case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1649
            have neq_th1: "th1 \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1650
            proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1651
              assume eq_th1: "th1 = th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1652
              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1653
                by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1654
              from children_no_dep[OF vt_s _ _ this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1655
              th1_in dp'
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1656
              show False by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1657
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1658
            show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1659
            proof(rule eq_cp)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1660
              show "th \<notin> dependants s th1"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1661
              proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1662
                assume "th \<in> dependants s th1"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1663
                from dependants_child_unique[OF vt_s _ _ this dp1]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1664
                th1_in dp' have "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1665
                  by (auto simp:children_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1666
                with False show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1667
              qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1668
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1669
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1670
        }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1671
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1672
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1673
        moreover have "children s th'' = children s' th''"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1674
          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1675
          apply (fold s_def, auto simp:RAG_s)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1676
          proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1677
            assume "(Cs cs, Th th'') \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1678
            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1679
            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1680
              by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1681
            from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1682
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1683
              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1684
              by (auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1685
            have eq_cs: "cs1 = cs" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1686
            proof -
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1687
              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1688
              from unique_RAG[OF vt_s this h1]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1689
              show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1690
            qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1691
            have False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1692
            proof(rule converse_tranclE[OF h2])
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1693
              assume "(Cs cs1, Th th') \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1694
              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1695
              from unique_RAG[OF vt_s this cs_th']
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1696
              have "th' = th''" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1697
              with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1698
              with wf_trancl[OF wf_child[OF vt_s]] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1699
              show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1700
            next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1701
              fix y
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1702
              assume "(Cs cs1, y) \<in> RAG s"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1703
                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1704
              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1705
              from unique_RAG[OF vt_s this cs_th']
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1706
              have "y = Th th''" .
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1707
              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1708
              from RAG_child[OF vt_s this]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1709
              have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1710
              moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1711
              ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1712
              with wf_trancl[OF wf_child[OF vt_s]] 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1713
              show False by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1714
            qed
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1715
            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1716
          qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1717
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1718
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1719
      qed     
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1720
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1721
  }
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1722
  ultimately show ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1723
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1724
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1725
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1726
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1727
locale step_create_cps =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1728
  fixes s' th prio s 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1729
  defines s_def : "s \<equiv> (Create th prio#s')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1730
  assumes vt_s: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1731
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1732
context step_create_cps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1733
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1734
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1735
lemma eq_dep: "RAG s = RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1736
  by (unfold s_def RAG_create_unchanged, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1737
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1738
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1739
  fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1740
  assumes neq_th: "th' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1741
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1742
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1743
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1744
  have nd: "th \<notin> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1745
  proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1746
    assume "th \<in> dependants s th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1747
    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1748
    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1749
    from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1750
    obtain y where "(Th th, y) \<in> RAG s'" by auto
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1751
    with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1752
    have in_th: "th \<in> threads s'" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1753
    from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1754
    show False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1755
    proof(cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1756
      assume "th \<notin> threads s'" 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1757
      with in_th show ?thesis by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1758
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1759
  qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1760
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1761
    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1762
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1763
    fix th1 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1764
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1765
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1766
    hence "preced th1 s = preced th1 s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1767
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1768
      assume "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1769
      with neq_th
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1770
      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1771
    next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1772
      assume "th1 \<in> dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1773
      with nd and eq_dp have "th1 \<noteq> th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1774
        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1775
      thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1776
    qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1777
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1778
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1779
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1780
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1781
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1782
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1783
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1784
lemma nil_dependants: "dependants s th = {}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1785
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1786
  from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1787
  show ?thesis
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1788
  proof(cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1789
    assume "th \<notin> threads s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1790
    from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1791
    have hdn: " holdents s' th = {}" .
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1792
    have "dependants s' th = {}"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1793
    proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1794
      { assume "dependants s' th \<noteq> {}"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1795
        then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1796
          by (auto simp:s_dependants_def eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1797
        from tranclE[OF this] obtain cs' where 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1798
          "(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1799
        with hdn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1800
        have False by (auto simp:holdents_test)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1801
      } thus ?thesis by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1802
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1803
    thus ?thesis 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1804
      by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1805
  qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1806
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1807
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1808
lemma eq_cp_th: "cp s th = preced th s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1809
  apply (unfold cp_eq_cpreced cpreced_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1810
  by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1811
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1812
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1813
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1814
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1815
locale step_exit_cps =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1816
  fixes s' th prio s 
33
9b9f2117561f simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 32
diff changeset
  1817
  defines s_def : "s \<equiv> Exit th # s'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1818
  assumes vt_s: "vt s"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1819
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1820
context step_exit_cps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1821
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1822
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1823
lemma eq_dep: "RAG s = RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1824
  by (unfold s_def RAG_exit_unchanged, auto)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1825
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1826
lemma eq_cp:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1827
  fixes th' 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1828
  assumes neq_th: "th' \<noteq> th"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1829
  shows "cp s th' = cp s' th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1830
  apply (unfold cp_eq_cpreced cpreced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1831
proof -
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1832
  have nd: "th \<notin> dependants s th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1833
  proof
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1834
    assume "th \<in> dependants s th'"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1835
    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1836
    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1837
    from converse_tranclE[OF this]
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1838
    obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1839
      by (auto simp:s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1840
    from step_back_step[OF vt_s[unfolded s_def]]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1841
    show False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1842
    proof(cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1843
      assume "th \<in> runing s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1844
      with bk show ?thesis
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1845
        apply (unfold runing_def readys_def s_waiting_def s_RAG_def)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1846
        by (auto simp:cs_waiting_def wq_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1847
    qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1848
  qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1849
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1850
    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1851
  moreover {
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1852
    fix th1 
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1853
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1854
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1855
    hence "preced th1 s = preced th1 s'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1856
    proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1857
      assume "th1 = th'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1858
      with neq_th
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1859
      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1860
    next
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1861
      assume "th1 \<in> dependants (wq s') th'"
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1862
      with nd and eq_dp have "th1 \<noteq> th"
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 33
diff changeset
  1863
        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1864
      thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1865
    qed
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1866
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1867
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1868
    by (auto simp:image_def)
32
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1869
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
e861aff29655 made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
  1870
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1871
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1872
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1873
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1874
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
  1875