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