src/HOLCF/IOA/meta_theory/ShortExecutions.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,278 +0,0 @@
     1.4 -(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
     1.5 -    Author:     Olaf Müller
     1.6 -*)
     1.7 -
     1.8 -theory ShortExecutions
     1.9 -imports Traces
    1.10 -begin
    1.11 -
    1.12 -text {*
    1.13 -  Some properties about @{text "Cut ex"}, defined as follows:
    1.14 -
    1.15 -  For every execution ex there is another shorter execution @{text "Cut ex"}
    1.16 -  that has the same trace as ex, but its schedule ends with an external action.
    1.17 -*}
    1.18 -
    1.19 -definition
    1.20 -  oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
    1.21 -  "oraclebuild P = (fix$(LAM h s t. case t of
    1.22 -       nil => nil
    1.23 -    | x##xs =>
    1.24 -      (case x of
    1.25 -        UU => UU
    1.26 -      | Def y => (Takewhile (%x.~P x)$s)
    1.27 -                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
    1.28 -      )
    1.29 -    ))"
    1.30 -
    1.31 -definition
    1.32 -  Cut :: "('a => bool) => 'a Seq => 'a Seq" where
    1.33 -  "Cut P s = oraclebuild P$s$(Filter P$s)"
    1.34 -
    1.35 -definition
    1.36 -  LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where
    1.37 -  "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)"
    1.38 -
    1.39 -(* LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
    1.40 -(* LastActExtex_def:
    1.41 -  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
    1.42 -
    1.43 -axiomatization where
    1.44 -  Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
    1.45 -
    1.46 -axiomatization where
    1.47 -  LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
    1.48 -
    1.49 -axiomatization where
    1.50 -  LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
    1.51 -
    1.52 -
    1.53 -ML {*
    1.54 -fun thin_tac' j =
    1.55 -  rotate_tac (j - 1) THEN'
    1.56 -  etac thin_rl THEN'
    1.57 -  rotate_tac (~ (j - 1))
    1.58 -*}
    1.59 -
    1.60 -
    1.61 -subsection "oraclebuild rewrite rules"
    1.62 -
    1.63 -
    1.64 -lemma oraclebuild_unfold:
    1.65 -"oraclebuild P = (LAM s t. case t of
    1.66 -       nil => nil
    1.67 -    | x##xs =>
    1.68 -      (case x of
    1.69 -        UU => UU
    1.70 -      | Def y => (Takewhile (%a.~ P a)$s)
    1.71 -                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))
    1.72 -      )
    1.73 -    )"
    1.74 -apply (rule trans)
    1.75 -apply (rule fix_eq2)
    1.76 -apply (simp only: oraclebuild_def)
    1.77 -apply (rule beta_cfun)
    1.78 -apply simp
    1.79 -done
    1.80 -
    1.81 -lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU"
    1.82 -apply (subst oraclebuild_unfold)
    1.83 -apply simp
    1.84 -done
    1.85 -
    1.86 -lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil"
    1.87 -apply (subst oraclebuild_unfold)
    1.88 -apply simp
    1.89 -done
    1.90 -
    1.91 -lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
    1.92 -          (Takewhile (%a.~ P a)$s)
    1.93 -           @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"
    1.94 -apply (rule trans)
    1.95 -apply (subst oraclebuild_unfold)
    1.96 -apply (simp add: Consq_def)
    1.97 -apply (simp add: Consq_def)
    1.98 -done
    1.99 -
   1.100 -
   1.101 -subsection "Cut rewrite rules"
   1.102 -
   1.103 -lemma Cut_nil:
   1.104 -"[| Forall (%a.~ P a) s; Finite s|]
   1.105 -            ==> Cut P s =nil"
   1.106 -apply (unfold Cut_def)
   1.107 -apply (subgoal_tac "Filter P$s = nil")
   1.108 -apply (simp (no_asm_simp) add: oraclebuild_nil)
   1.109 -apply (rule ForallQFilterPnil)
   1.110 -apply assumption+
   1.111 -done
   1.112 -
   1.113 -lemma Cut_UU:
   1.114 -"[| Forall (%a.~ P a) s; ~Finite s|]
   1.115 -            ==> Cut P s =UU"
   1.116 -apply (unfold Cut_def)
   1.117 -apply (subgoal_tac "Filter P$s= UU")
   1.118 -apply (simp (no_asm_simp) add: oraclebuild_UU)
   1.119 -apply (rule ForallQFilterPUU)
   1.120 -apply assumption+
   1.121 -done
   1.122 -
   1.123 -lemma Cut_Cons:
   1.124 -"[| P t;  Forall (%x.~ P x) ss; Finite ss|]
   1.125 -            ==> Cut P (ss @@ (t>> rs))
   1.126 -                 = ss @@ (t >> Cut P rs)"
   1.127 -apply (unfold Cut_def)
   1.128 -apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
   1.129 -done
   1.130 -
   1.131 -
   1.132 -subsection "Cut lemmas for main theorem"
   1.133 -
   1.134 -lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
   1.135 -apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in take_lemma_induct [THEN mp])
   1.136 -prefer 3 apply (fast)
   1.137 -apply (case_tac "Finite s")
   1.138 -apply (simp add: Cut_nil ForallQFilterPnil)
   1.139 -apply (simp add: Cut_UU ForallQFilterPUU)
   1.140 -(* main case *)
   1.141 -apply (simp add: Cut_Cons ForallQFilterPnil)
   1.142 -done
   1.143 -
   1.144 -
   1.145 -lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
   1.146 -apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in
   1.147 -  take_lemma_less_induct [THEN mp])
   1.148 -prefer 3 apply (fast)
   1.149 -apply (case_tac "Finite s")
   1.150 -apply (simp add: Cut_nil ForallQFilterPnil)
   1.151 -apply (simp add: Cut_UU ForallQFilterPUU)
   1.152 -(* main case *)
   1.153 -apply (simp add: Cut_Cons ForallQFilterPnil)
   1.154 -apply (rule take_reduction)
   1.155 -apply auto
   1.156 -done
   1.157 -
   1.158 -
   1.159 -lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
   1.160 -apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P (f x) " and x1 = "s" in
   1.161 -  take_lemma_less_induct [THEN mp])
   1.162 -prefer 3 apply (fast)
   1.163 -apply (case_tac "Finite s")
   1.164 -apply (simp add: Cut_nil)
   1.165 -apply (rule Cut_nil [symmetric])
   1.166 -apply (simp add: ForallMap o_def)
   1.167 -apply (simp add: Map2Finite)
   1.168 -(* csae ~ Finite s *)
   1.169 -apply (simp add: Cut_UU)
   1.170 -apply (rule Cut_UU)
   1.171 -apply (simp add: ForallMap o_def)
   1.172 -apply (simp add: Map2Finite)
   1.173 -(* main case *)
   1.174 -apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
   1.175 -apply (rule take_reduction)
   1.176 -apply auto
   1.177 -done
   1.178 -
   1.179 -
   1.180 -lemma Cut_prefixcl_nFinite [rule_format (no_asm)]: "~Finite s --> Cut P s << s"
   1.181 -apply (intro strip)
   1.182 -apply (rule take_lemma_less [THEN iffD1])
   1.183 -apply (intro strip)
   1.184 -apply (rule mp)
   1.185 -prefer 2 apply (assumption)
   1.186 -apply (tactic "thin_tac' 1 1")
   1.187 -apply (rule_tac x = "s" in spec)
   1.188 -apply (rule nat_less_induct)
   1.189 -apply (intro strip)
   1.190 -apply (rename_tac na n s)
   1.191 -apply (case_tac "Forall (%x. ~ P x) s")
   1.192 -apply (rule take_lemma_less [THEN iffD2, THEN spec])
   1.193 -apply (simp add: Cut_UU)
   1.194 -(* main case *)
   1.195 -apply (drule divide_Seq3)
   1.196 -apply (erule exE)+
   1.197 -apply (erule conjE)+
   1.198 -apply hypsubst
   1.199 -apply (simp add: Cut_Cons)
   1.200 -apply (rule take_reduction_less)
   1.201 -(* auto makes also reasoning about Finiteness of parts of s ! *)
   1.202 -apply auto
   1.203 -done
   1.204 -
   1.205 -
   1.206 -lemma execThruCut: "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"
   1.207 -apply (case_tac "Finite ex")
   1.208 -apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
   1.209 -apply assumption
   1.210 -apply (erule exE)
   1.211 -apply (rule exec_prefix2closed)
   1.212 -apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
   1.213 -apply assumption
   1.214 -apply (erule exec_prefixclosed)
   1.215 -apply (erule Cut_prefixcl_nFinite)
   1.216 -done
   1.217 -
   1.218 -
   1.219 -subsection "Main Cut Theorem"
   1.220 -
   1.221 -lemma exists_LastActExtsch:
   1.222 - "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
   1.223 -    ==> ? sch. sch : schedules A &
   1.224 -               tr = Filter (%a. a:ext A)$sch &
   1.225 -               LastActExtsch A sch"
   1.226 -
   1.227 -apply (unfold schedules_def has_schedule_def)
   1.228 -apply auto
   1.229 -apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
   1.230 -apply (simp add: executions_def)
   1.231 -apply (tactic {* pair_tac @{context} "ex" 1 *})
   1.232 -apply auto
   1.233 -apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
   1.234 -apply (simp (no_asm_simp))
   1.235 -
   1.236 -(* Subgoal 1: Lemma:  propagation of execution through Cut *)
   1.237 -
   1.238 -apply (simp add: execThruCut)
   1.239 -
   1.240 -(* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
   1.241 -
   1.242 -apply (simp (no_asm) add: filter_act_def)
   1.243 -apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
   1.244 -
   1.245 -apply (rule_tac [2] MapCut [unfolded o_def])
   1.246 -apply (simp add: FilterCut [symmetric])
   1.247 -
   1.248 -(* Subgoal 3: Lemma: Cut idempotent  *)
   1.249 -
   1.250 -apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
   1.251 -apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) y) = Cut (%a. a:ext A) (Map fst$y) ")
   1.252 -apply (rule_tac [2] MapCut [unfolded o_def])
   1.253 -apply (simp add: Cut_idemp)
   1.254 -done
   1.255 -
   1.256 -
   1.257 -subsection "Further Cut lemmas"
   1.258 -
   1.259 -lemma LastActExtimplnil:
   1.260 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
   1.261 -    ==> sch=nil"
   1.262 -apply (unfold LastActExtsch_def)
   1.263 -apply (drule FilternPnilForallP)
   1.264 -apply (erule conjE)
   1.265 -apply (drule Cut_nil)
   1.266 -apply assumption
   1.267 -apply simp
   1.268 -done
   1.269 -
   1.270 -lemma LastActExtimplUU:
   1.271 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
   1.272 -    ==> sch=UU"
   1.273 -apply (unfold LastActExtsch_def)
   1.274 -apply (drule FilternPUUForallP)
   1.275 -apply (erule conjE)
   1.276 -apply (drule Cut_UU)
   1.277 -apply assumption
   1.278 -apply simp
   1.279 -done
   1.280 -
   1.281 -end