src/HOLCF/IOA/meta_theory/ShortExecutions.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 9877 b2a62260f8ac
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1997  TU Muenchen
mueller@3071
     5
mueller@3275
     6
Some properties about (Cut ex), defined as follows:
mueller@3071
     7
mueller@3275
     8
For every execution ex there is another shorter execution (Cut ex) 
mueller@3071
     9
that has the same trace as ex, but its schedule ends with an external action.
mueller@3071
    10
mueller@3275
    11
*) 
mueller@3275
    12
mueller@3275
    13
mueller@3361
    14
fun thin_tac' j =
mueller@3361
    15
  rotate_tac (j - 1) THEN'
mueller@3361
    16
  etac thin_rl THEN' 
mueller@3361
    17
  rotate_tac (~ (j - 1));
mueller@3361
    18
mueller@3275
    19
mueller@3275
    20
mueller@3275
    21
(* ---------------------------------------------------------------- *)
mueller@3275
    22
                   section "oraclebuild rewrite rules";
mueller@3275
    23
(* ---------------------------------------------------------------- *)
mueller@3275
    24
mueller@3275
    25
mueller@3275
    26
bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def 
mueller@3275
    27
"oraclebuild P = (LAM s t. case t of \
mueller@3275
    28
\       nil => nil\
mueller@3275
    29
\    | x##xs => \
mueller@3275
    30
\      (case x of\ 
mueller@3275
    31
\        Undef => UU\
nipkow@10835
    32
\      | Def y => (Takewhile (%a.~ P a)$s)\
nipkow@10835
    33
\                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
mueller@3275
    34
\      )\
mueller@3275
    35
\    )");
mueller@3275
    36
nipkow@10835
    37
Goal "oraclebuild P$sch$UU = UU";
mueller@3275
    38
by (stac oraclebuild_unfold 1);
mueller@3275
    39
by (Simp_tac 1);
mueller@3275
    40
qed"oraclebuild_UU";
mueller@3275
    41
nipkow@10835
    42
Goal "oraclebuild P$sch$nil = nil";
mueller@3275
    43
by (stac oraclebuild_unfold 1);
mueller@3275
    44
by (Simp_tac 1);
mueller@3275
    45
qed"oraclebuild_nil";
mueller@3275
    46
nipkow@10835
    47
Goal "oraclebuild P$s$(x>>t) = \
nipkow@10835
    48
\         (Takewhile (%a.~ P a)$s)   \
nipkow@10835
    49
\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";     
paulson@3457
    50
by (rtac trans 1);
mueller@3275
    51
by (stac oraclebuild_unfold 1);
wenzelm@7229
    52
by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
wenzelm@7229
    53
by (simp_tac (simpset() addsimps [Consq_def]) 1);
mueller@3275
    54
qed"oraclebuild_cons";
mueller@3275
    55
mueller@3275
    56
mueller@3275
    57
mueller@3275
    58
 
mueller@3275
    59
(* ---------------------------------------------------------------- *)
mueller@3275
    60
                   section "Cut rewrite rules";
mueller@3275
    61
(* ---------------------------------------------------------------- *)
mueller@3275
    62
wenzelm@5068
    63
Goalw [Cut_def]
paulson@6161
    64
"[| Forall (%a.~ P a) s; Finite s|] \
mueller@3275
    65
\           ==> Cut P s =nil";
nipkow@10835
    66
by (subgoal_tac "Filter P$s = nil" 1);
wenzelm@4098
    67
by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
paulson@3457
    68
by (rtac ForallQFilterPnil 1);
mueller@3275
    69
by (REPEAT (atac 1));
mueller@3275
    70
qed"Cut_nil";
mueller@3275
    71
wenzelm@5068
    72
Goalw [Cut_def]
paulson@6161
    73
"[| Forall (%a.~ P a) s; ~Finite s|] \
mueller@3275
    74
\           ==> Cut P s =UU";
nipkow@10835
    75
by (subgoal_tac "Filter P$s= UU" 1);
wenzelm@4098
    76
by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
paulson@3457
    77
by (rtac ForallQFilterPUU 1);
mueller@3275
    78
by (REPEAT (atac 1));
mueller@3275
    79
qed"Cut_UU";
mueller@3275
    80
wenzelm@5068
    81
Goalw [Cut_def]
paulson@6161
    82
"[| P t;  Forall (%x.~ P x) ss; Finite ss|] \
mueller@3275
    83
\           ==> Cut P (ss @@ (t>> rs)) \
mueller@3275
    84
\                = ss @@ (t >> Cut P rs)";
mueller@3275
    85
wenzelm@4098
    86
by (asm_full_simp_tac (simpset() addsimps [ForallQFilterPnil,oraclebuild_cons,
mueller@3275
    87
          TakewhileConc,DropwhileConc]) 1);
mueller@3275
    88
qed"Cut_Cons";
mueller@3275
    89
mueller@3275
    90
mueller@3275
    91
(* ---------------------------------------------------------------- *)
mueller@3275
    92
                   section "Cut lemmas for main theorem";
mueller@3275
    93
(* ---------------------------------------------------------------- *)
mueller@3275
    94
mueller@3275
    95
nipkow@10835
    96
Goal "Filter P$s = Filter P$(Cut P s)";
mueller@3275
    97
wenzelm@3847
    98
by (res_inst_tac [("A1","%x. True")
mueller@3275
    99
                 ,("Q1","%x.~ P x"), ("x1","s")]
mueller@3275
   100
                 (take_lemma_induct RS mp) 1);
mueller@3275
   101
by (Fast_tac 3);
mueller@3275
   102
by (case_tac "Finite s" 1);
wenzelm@4098
   103
by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
mueller@3275
   104
             ForallQFilterPnil]) 1);
wenzelm@4098
   105
by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
mueller@3275
   106
             ForallQFilterPUU]) 1);
mueller@3275
   107
(* main case *)
wenzelm@4098
   108
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
paulson@4477
   109
by Auto_tac;
mueller@3275
   110
qed"FilterCut";
mueller@3275
   111
mueller@3275
   112
wenzelm@5068
   113
Goal "Cut P (Cut P s) = (Cut P s)";
mueller@3275
   114
wenzelm@3847
   115
by (res_inst_tac [("A1","%x. True")
mueller@3275
   116
                 ,("Q1","%x.~ P x"), ("x1","s")]
mueller@3275
   117
                 (take_lemma_less_induct RS mp) 1);
mueller@3275
   118
by (Fast_tac 3);
mueller@3275
   119
by (case_tac "Finite s" 1);
wenzelm@4098
   120
by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
mueller@3275
   121
             ForallQFilterPnil]) 1);
wenzelm@4098
   122
by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
mueller@3275
   123
             ForallQFilterPUU]) 1);
mueller@3275
   124
(* main case *)
wenzelm@4098
   125
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
paulson@3457
   126
by (rtac take_reduction 1);
paulson@4477
   127
by Auto_tac;
mueller@3275
   128
qed"Cut_idemp";
mueller@3275
   129
mueller@3275
   130
nipkow@10835
   131
Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)";
mueller@3275
   132
wenzelm@3847
   133
by (res_inst_tac [("A1","%x. True")
mueller@3275
   134
                 ,("Q1","%x.~ P (f x)"), ("x1","s")]
mueller@3275
   135
                 (take_lemma_less_induct RS mp) 1);
mueller@3275
   136
by (Fast_tac 3);
mueller@3275
   137
by (case_tac "Finite s" 1);
wenzelm@4098
   138
by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); 
paulson@3457
   139
by (rtac (Cut_nil RS sym) 1);
wenzelm@4098
   140
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
wenzelm@4098
   141
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
mueller@3275
   142
(* csae ~ Finite s *)
wenzelm@4098
   143
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
paulson@3457
   144
by (rtac (Cut_UU RS sym) 1);
wenzelm@4098
   145
by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
wenzelm@4098
   146
by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
mueller@3275
   147
(* main case *)
wenzelm@4098
   148
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
mueller@3275
   149
          ForallMap,FiniteMap1,o_def]) 1);
paulson@3457
   150
by (rtac take_reduction 1);
paulson@4477
   151
by Auto_tac;
mueller@3275
   152
qed"MapCut";
mueller@3275
   153
mueller@3275
   154
wenzelm@5068
   155
Goal "~Finite s --> Cut P s << s";
mueller@3361
   156
by (strip_tac 1);
paulson@3457
   157
by (rtac (take_lemma_less RS iffD1) 1);
mueller@3361
   158
by (strip_tac 1);
paulson@3457
   159
by (rtac mp 1);
paulson@3457
   160
by (assume_tac 2);
mueller@3361
   161
by (thin_tac' 1 1);
mueller@3361
   162
by (res_inst_tac [("x","s")] spec 1);
nipkow@9877
   163
by (rtac nat_less_induct 1);
mueller@3361
   164
by (strip_tac 1);
mueller@3361
   165
ren "na n s" 1;
mueller@3361
   166
by (case_tac "Forall (%x. ~ P x) s" 1);
paulson@3457
   167
by (rtac (take_lemma_less RS iffD2 RS spec) 1);
wenzelm@4098
   168
by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
mueller@3361
   169
(* main case *)
paulson@3457
   170
by (dtac divide_Seq3 1);
mueller@3361
   171
by (REPEAT (etac exE 1));
mueller@3361
   172
by (REPEAT (etac conjE 1));
mueller@3361
   173
by (hyp_subst_tac 1);
wenzelm@4098
   174
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1);
paulson@3457
   175
by (rtac take_reduction_less 1);
mueller@3361
   176
(* auto makes also reasoning about Finiteness of parts of s ! *)
paulson@4477
   177
by Auto_tac;
mueller@3361
   178
qed_spec_mp"Cut_prefixcl_nFinite";
mueller@3361
   179
mueller@3361
   180
mueller@3361
   181
wenzelm@5068
   182
Goal "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
mueller@3361
   183
by (case_tac "Finite ex" 1);
mueller@3361
   184
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
paulson@3457
   185
by (assume_tac 1);
paulson@3457
   186
by (etac exE 1);
paulson@3457
   187
by (rtac exec_prefix2closed 1);
mueller@3361
   188
by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1);
paulson@3457
   189
by (assume_tac 1);
paulson@3457
   190
by (etac exec_prefixclosed 1);
paulson@3457
   191
by (etac Cut_prefixcl_nFinite 1);
mueller@3361
   192
qed"execThruCut";
mueller@3361
   193
mueller@3275
   194
mueller@3275
   195
mueller@3275
   196
(* ---------------------------------------------------------------- *)
mueller@3275
   197
                   section "Main Cut Theorem";
mueller@3275
   198
(* ---------------------------------------------------------------- *)
mueller@3275
   199
mueller@3275
   200
mueller@3275
   201
wenzelm@5068
   202
Goalw [schedules_def,has_schedule_def]
nipkow@10835
   203
 "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \
mueller@3275
   204
\   ==> ? sch. sch : schedules A & \
nipkow@10835
   205
\              tr = Filter (%a. a:ext A)$sch &\
mueller@3275
   206
\              LastActExtsch A sch";
mueller@3275
   207
mueller@3275
   208
by (safe_tac set_cs);
nipkow@10835
   209
by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
wenzelm@4098
   210
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
mueller@3275
   211
by (pair_tac "ex" 1);
mueller@3275
   212
by (safe_tac set_cs);
wenzelm@3847
   213
by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1);
mueller@3275
   214
by (Asm_simp_tac 1);
mueller@3275
   215
mueller@3275
   216
(* Subgoal 1: Lemma:  propagation of execution through Cut *)
mueller@3275
   217
wenzelm@4098
   218
by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1);
mueller@3275
   219
mueller@3275
   220
(* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
mueller@3275
   221
wenzelm@4098
   222
by (simp_tac (simpset() addsimps [filter_act_def]) 1);
nipkow@10835
   223
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
mueller@4283
   224
paulson@3457
   225
by (rtac (rewrite_rule [o_def] MapCut) 2);
wenzelm@4098
   226
by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
mueller@3275
   227
mueller@3275
   228
(* Subgoal 3: Lemma: Cut idempotent  *)
mueller@3275
   229
wenzelm@4098
   230
by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
nipkow@10835
   231
by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
paulson@3457
   232
by (rtac (rewrite_rule [o_def] MapCut) 2);
wenzelm@4098
   233
by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
mueller@3275
   234
qed"exists_LastActExtsch";
mueller@3275
   235
mueller@3275
   236
mueller@3275
   237
(* ---------------------------------------------------------------- *)
mueller@3275
   238
                   section "Further Cut lemmas";
mueller@3275
   239
(* ---------------------------------------------------------------- *)
mueller@3275
   240
wenzelm@5068
   241
Goalw [LastActExtsch_def]
nipkow@10835
   242
  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \
mueller@3275
   243
\   ==> sch=nil";
paulson@3457
   244
by (dtac FilternPnilForallP 1);
paulson@3457
   245
by (etac conjE 1);
paulson@3457
   246
by (dtac Cut_nil 1);
paulson@3457
   247
by (assume_tac 1);
mueller@3275
   248
by (Asm_full_simp_tac 1);
mueller@3275
   249
qed"LastActExtimplnil";
mueller@3275
   250
wenzelm@5068
   251
Goalw [LastActExtsch_def]
nipkow@10835
   252
  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \
mueller@3275
   253
\   ==> sch=UU";
paulson@3457
   254
by (dtac FilternPUUForallP 1);
paulson@3457
   255
by (etac conjE 1);
paulson@3457
   256
by (dtac Cut_UU 1);
paulson@3457
   257
by (assume_tac 1);
mueller@3275
   258
by (Asm_full_simp_tac 1);
mueller@3275
   259
qed"LastActExtimplUU";