src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 60754 02924903a6fd
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
wenzelm@40945
     2
    Author:     Olaf Müller
wenzelm@17256
     3
*)
mueller@3071
     4
wenzelm@17256
     5
theory ShortExecutions
wenzelm@17256
     6
imports Traces
wenzelm@17256
     7
begin
mueller@3071
     8
wenzelm@17256
     9
text {*
wenzelm@17256
    10
  Some properties about @{text "Cut ex"}, defined as follows:
mueller@3071
    11
wenzelm@17256
    12
  For every execution ex there is another shorter execution @{text "Cut ex"}
wenzelm@17256
    13
  that has the same trace as ex, but its schedule ends with an external action.
wenzelm@17256
    14
*}
mueller@3071
    15
wenzelm@25135
    16
definition
wenzelm@25135
    17
  oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
wenzelm@25135
    18
  "oraclebuild P = (fix$(LAM h s t. case t of
mueller@3275
    19
       nil => nil
wenzelm@17256
    20
    | x##xs =>
wenzelm@17256
    21
      (case x of
wenzelm@12028
    22
        UU => UU
nipkow@10835
    23
      | Def y => (Takewhile (%x.~P x)$s)
nipkow@10835
    24
                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
mueller@3275
    25
      )
mueller@3275
    26
    ))"
mueller@3275
    27
wenzelm@25135
    28
definition
wenzelm@25135
    29
  Cut :: "('a => bool) => 'a Seq => 'a Seq" where
wenzelm@25135
    30
  "Cut P s = oraclebuild P$s$(Filter P$s)"
mueller@3071
    31
wenzelm@25135
    32
definition
wenzelm@25135
    33
  LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where
wenzelm@25135
    34
  "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)"
mueller@3071
    35
wenzelm@25135
    36
(* LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
wenzelm@25135
    37
(* LastActExtex_def:
wenzelm@25135
    38
  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
mueller@3071
    39
wenzelm@25135
    40
axiomatization where
wenzelm@25135
    41
  Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
mueller@3071
    42
wenzelm@25135
    43
axiomatization where
wenzelm@25135
    44
  LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
wenzelm@25135
    45
wenzelm@25135
    46
axiomatization where
wenzelm@25135
    47
  LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
wenzelm@19741
    48
wenzelm@19741
    49
wenzelm@19741
    50
ML {*
wenzelm@19741
    51
fun thin_tac' j =
wenzelm@19741
    52
  rotate_tac (j - 1) THEN'
wenzelm@19741
    53
  etac thin_rl THEN'
wenzelm@19741
    54
  rotate_tac (~ (j - 1))
wenzelm@19741
    55
*}
wenzelm@19741
    56
wenzelm@19741
    57
wenzelm@19741
    58
subsection "oraclebuild rewrite rules"
wenzelm@19741
    59
wenzelm@19741
    60
wenzelm@19741
    61
lemma oraclebuild_unfold:
wenzelm@25135
    62
"oraclebuild P = (LAM s t. case t of
wenzelm@19741
    63
       nil => nil
wenzelm@25135
    64
    | x##xs =>
wenzelm@19741
    65
      (case x of
wenzelm@19741
    66
        UU => UU
wenzelm@19741
    67
      | Def y => (Takewhile (%a.~ P a)$s)
wenzelm@19741
    68
                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))
wenzelm@19741
    69
      )
wenzelm@19741
    70
    )"
wenzelm@19741
    71
apply (rule trans)
wenzelm@19741
    72
apply (rule fix_eq2)
wenzelm@25135
    73
apply (simp only: oraclebuild_def)
wenzelm@19741
    74
apply (rule beta_cfun)
wenzelm@19741
    75
apply simp
wenzelm@19741
    76
done
wenzelm@19741
    77
wenzelm@19741
    78
lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU"
wenzelm@19741
    79
apply (subst oraclebuild_unfold)
wenzelm@19741
    80
apply simp
wenzelm@19741
    81
done
wenzelm@19741
    82
wenzelm@19741
    83
lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil"
wenzelm@19741
    84
apply (subst oraclebuild_unfold)
wenzelm@19741
    85
apply simp
wenzelm@19741
    86
done
wenzelm@19741
    87
wenzelm@25135
    88
lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
wenzelm@25135
    89
          (Takewhile (%a.~ P a)$s)
wenzelm@19741
    90
           @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"
wenzelm@19741
    91
apply (rule trans)
wenzelm@19741
    92
apply (subst oraclebuild_unfold)
wenzelm@19741
    93
apply (simp add: Consq_def)
wenzelm@19741
    94
apply (simp add: Consq_def)
wenzelm@19741
    95
done
wenzelm@19741
    96
wenzelm@19741
    97
wenzelm@19741
    98
subsection "Cut rewrite rules"
wenzelm@19741
    99
wenzelm@25135
   100
lemma Cut_nil:
wenzelm@25135
   101
"[| Forall (%a.~ P a) s; Finite s|]
wenzelm@19741
   102
            ==> Cut P s =nil"
wenzelm@19741
   103
apply (unfold Cut_def)
wenzelm@19741
   104
apply (subgoal_tac "Filter P$s = nil")
wenzelm@19741
   105
apply (simp (no_asm_simp) add: oraclebuild_nil)
wenzelm@19741
   106
apply (rule ForallQFilterPnil)
wenzelm@19741
   107
apply assumption+
wenzelm@19741
   108
done
wenzelm@19741
   109
wenzelm@25135
   110
lemma Cut_UU:
wenzelm@25135
   111
"[| Forall (%a.~ P a) s; ~Finite s|]
wenzelm@19741
   112
            ==> Cut P s =UU"
wenzelm@19741
   113
apply (unfold Cut_def)
wenzelm@19741
   114
apply (subgoal_tac "Filter P$s= UU")
wenzelm@19741
   115
apply (simp (no_asm_simp) add: oraclebuild_UU)
wenzelm@19741
   116
apply (rule ForallQFilterPUU)
wenzelm@19741
   117
apply assumption+
wenzelm@19741
   118
done
wenzelm@19741
   119
wenzelm@25135
   120
lemma Cut_Cons:
wenzelm@25135
   121
"[| P t;  Forall (%x.~ P x) ss; Finite ss|]
wenzelm@25135
   122
            ==> Cut P (ss @@ (t>> rs))
wenzelm@19741
   123
                 = ss @@ (t >> Cut P rs)"
wenzelm@19741
   124
apply (unfold Cut_def)
wenzelm@19741
   125
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
wenzelm@19741
   126
done
wenzelm@19741
   127
wenzelm@19741
   128
wenzelm@19741
   129
subsection "Cut lemmas for main theorem"
wenzelm@19741
   130
wenzelm@19741
   131
lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
wenzelm@19741
   132
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in take_lemma_induct [THEN mp])
wenzelm@19741
   133
prefer 3 apply (fast)
wenzelm@19741
   134
apply (case_tac "Finite s")
wenzelm@19741
   135
apply (simp add: Cut_nil ForallQFilterPnil)
wenzelm@19741
   136
apply (simp add: Cut_UU ForallQFilterPUU)
wenzelm@19741
   137
(* main case *)
wenzelm@19741
   138
apply (simp add: Cut_Cons ForallQFilterPnil)
wenzelm@19741
   139
done
wenzelm@19741
   140
wenzelm@19741
   141
wenzelm@19741
   142
lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
wenzelm@19741
   143
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in
wenzelm@19741
   144
  take_lemma_less_induct [THEN mp])
wenzelm@19741
   145
prefer 3 apply (fast)
wenzelm@19741
   146
apply (case_tac "Finite s")
wenzelm@19741
   147
apply (simp add: Cut_nil ForallQFilterPnil)
wenzelm@19741
   148
apply (simp add: Cut_UU ForallQFilterPUU)
wenzelm@19741
   149
(* main case *)
wenzelm@19741
   150
apply (simp add: Cut_Cons ForallQFilterPnil)
wenzelm@19741
   151
apply (rule take_reduction)
wenzelm@19741
   152
apply auto
wenzelm@19741
   153
done
wenzelm@19741
   154
wenzelm@19741
   155
wenzelm@19741
   156
lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
wenzelm@19741
   157
apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P (f x) " and x1 = "s" in
wenzelm@19741
   158
  take_lemma_less_induct [THEN mp])
wenzelm@19741
   159
prefer 3 apply (fast)
wenzelm@19741
   160
apply (case_tac "Finite s")
wenzelm@19741
   161
apply (simp add: Cut_nil)
wenzelm@19741
   162
apply (rule Cut_nil [symmetric])
wenzelm@19741
   163
apply (simp add: ForallMap o_def)
wenzelm@19741
   164
apply (simp add: Map2Finite)
wenzelm@19741
   165
(* csae ~ Finite s *)
wenzelm@19741
   166
apply (simp add: Cut_UU)
wenzelm@19741
   167
apply (rule Cut_UU)
wenzelm@19741
   168
apply (simp add: ForallMap o_def)
wenzelm@19741
   169
apply (simp add: Map2Finite)
wenzelm@19741
   170
(* main case *)
wenzelm@19741
   171
apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
wenzelm@19741
   172
apply (rule take_reduction)
wenzelm@19741
   173
apply auto
wenzelm@19741
   174
done
wenzelm@19741
   175
wenzelm@19741
   176
wenzelm@19741
   177
lemma Cut_prefixcl_nFinite [rule_format (no_asm)]: "~Finite s --> Cut P s << s"
wenzelm@19741
   178
apply (intro strip)
wenzelm@19741
   179
apply (rule take_lemma_less [THEN iffD1])
wenzelm@19741
   180
apply (intro strip)
wenzelm@19741
   181
apply (rule mp)
wenzelm@19741
   182
prefer 2 apply (assumption)
wenzelm@19741
   183
apply (tactic "thin_tac' 1 1")
wenzelm@19741
   184
apply (rule_tac x = "s" in spec)
wenzelm@19741
   185
apply (rule nat_less_induct)
wenzelm@19741
   186
apply (intro strip)
wenzelm@19741
   187
apply (rename_tac na n s)
wenzelm@19741
   188
apply (case_tac "Forall (%x. ~ P x) s")
wenzelm@19741
   189
apply (rule take_lemma_less [THEN iffD2, THEN spec])
wenzelm@19741
   190
apply (simp add: Cut_UU)
wenzelm@19741
   191
(* main case *)
wenzelm@19741
   192
apply (drule divide_Seq3)
wenzelm@19741
   193
apply (erule exE)+
wenzelm@19741
   194
apply (erule conjE)+
wenzelm@19741
   195
apply hypsubst
wenzelm@19741
   196
apply (simp add: Cut_Cons)
wenzelm@19741
   197
apply (rule take_reduction_less)
wenzelm@19741
   198
(* auto makes also reasoning about Finiteness of parts of s ! *)
wenzelm@19741
   199
apply auto
wenzelm@19741
   200
done
wenzelm@19741
   201
wenzelm@19741
   202
wenzelm@19741
   203
lemma execThruCut: "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"
wenzelm@19741
   204
apply (case_tac "Finite ex")
wenzelm@19741
   205
apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
wenzelm@19741
   206
apply assumption
wenzelm@19741
   207
apply (erule exE)
wenzelm@19741
   208
apply (rule exec_prefix2closed)
wenzelm@19741
   209
apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
wenzelm@19741
   210
apply assumption
wenzelm@19741
   211
apply (erule exec_prefixclosed)
wenzelm@19741
   212
apply (erule Cut_prefixcl_nFinite)
wenzelm@19741
   213
done
wenzelm@19741
   214
wenzelm@19741
   215
wenzelm@19741
   216
subsection "Main Cut Theorem"
wenzelm@19741
   217
wenzelm@25135
   218
lemma exists_LastActExtsch:
wenzelm@25135
   219
 "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
wenzelm@25135
   220
    ==> ? sch. sch : schedules A &
wenzelm@25135
   221
               tr = Filter (%a. a:ext A)$sch &
wenzelm@19741
   222
               LastActExtsch A sch"
wenzelm@19741
   223
wenzelm@19741
   224
apply (unfold schedules_def has_schedule_def)
haftmann@26359
   225
apply auto
wenzelm@19741
   226
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
wenzelm@19741
   227
apply (simp add: executions_def)
wenzelm@27208
   228
apply (tactic {* pair_tac @{context} "ex" 1 *})
haftmann@26359
   229
apply auto
wenzelm@19741
   230
apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
wenzelm@19741
   231
apply (simp (no_asm_simp))
wenzelm@19741
   232
wenzelm@19741
   233
(* Subgoal 1: Lemma:  propagation of execution through Cut *)
wenzelm@19741
   234
wenzelm@19741
   235
apply (simp add: execThruCut)
wenzelm@19741
   236
wenzelm@19741
   237
(* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
wenzelm@19741
   238
wenzelm@19741
   239
apply (simp (no_asm) add: filter_act_def)
wenzelm@19741
   240
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
wenzelm@19741
   241
wenzelm@19741
   242
apply (rule_tac [2] MapCut [unfolded o_def])
wenzelm@19741
   243
apply (simp add: FilterCut [symmetric])
wenzelm@19741
   244
wenzelm@19741
   245
(* Subgoal 3: Lemma: Cut idempotent  *)
wenzelm@19741
   246
wenzelm@19741
   247
apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
wenzelm@19741
   248
apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
wenzelm@19741
   249
apply (rule_tac [2] MapCut [unfolded o_def])
wenzelm@19741
   250
apply (simp add: Cut_idemp)
wenzelm@19741
   251
done
wenzelm@19741
   252
wenzelm@19741
   253
wenzelm@19741
   254
subsection "Further Cut lemmas"
wenzelm@19741
   255
wenzelm@25135
   256
lemma LastActExtimplnil:
wenzelm@25135
   257
  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
wenzelm@19741
   258
    ==> sch=nil"
wenzelm@19741
   259
apply (unfold LastActExtsch_def)
wenzelm@19741
   260
apply (drule FilternPnilForallP)
wenzelm@19741
   261
apply (erule conjE)
wenzelm@19741
   262
apply (drule Cut_nil)
wenzelm@19741
   263
apply assumption
wenzelm@19741
   264
apply simp
wenzelm@19741
   265
done
wenzelm@19741
   266
wenzelm@25135
   267
lemma LastActExtimplUU:
wenzelm@25135
   268
  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
wenzelm@19741
   269
    ==> sch=UU"
wenzelm@19741
   270
apply (unfold LastActExtsch_def)
wenzelm@19741
   271
apply (drule FilternPUUForallP)
wenzelm@19741
   272
apply (erule conjE)
wenzelm@19741
   273
apply (drule Cut_UU)
wenzelm@19741
   274
apply assumption
wenzelm@19741
   275
apply simp
wenzelm@19741
   276
done
wenzelm@17256
   277
mueller@3071
   278
end