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