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