--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy Thu Dec 31 12:43:09 2015 +0100
@@ -0,0 +1,278 @@
+(* Title: HOL/HOLCF/IOA/ShortExecutions.thy
+ Author: Olaf Müller
+*)
+
+theory ShortExecutions
+imports Traces
+begin
+
+text \<open>
+ Some properties about \<open>Cut ex\<close>, defined as follows:
+
+ For every execution ex there is another shorter execution \<open>Cut ex\<close>
+ that has the same trace as ex, but its schedule ends with an external action.
+\<close>
+
+definition
+ oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
+ "oraclebuild P = (fix$(LAM h s t. case t of
+ nil => nil
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y => (Takewhile (%x. \<not>P x)$s)
+ @@ (y\<leadsto>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
+ )
+ ))"
+
+definition
+ Cut :: "('a => bool) => 'a Seq => 'a Seq" where
+ "Cut P s = oraclebuild P$s$(Filter P$s)"
+
+definition
+ LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where
+ "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)"
+
+(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*)
+(* LastActExtex_def:
+ "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
+
+axiomatization where
+ Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
+
+axiomatization where
+ LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
+
+axiomatization where
+ LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
+
+
+ML \<open>
+fun thin_tac' ctxt j =
+ rotate_tac (j - 1) THEN'
+ eresolve_tac ctxt [thin_rl] THEN'
+ rotate_tac (~ (j - 1))
+\<close>
+
+
+subsection "oraclebuild rewrite rules"
+
+
+lemma oraclebuild_unfold:
+"oraclebuild P = (LAM s t. case t of
+ nil => nil
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y => (Takewhile (%a. \<not> P a)$s)
+ @@ (y\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs))
+ )
+ )"
+apply (rule trans)
+apply (rule fix_eq2)
+apply (simp only: oraclebuild_def)
+apply (rule beta_cfun)
+apply simp
+done
+
+lemma oraclebuild_UU: "oraclebuild P$sch$UU = UU"
+apply (subst oraclebuild_unfold)
+apply simp
+done
+
+lemma oraclebuild_nil: "oraclebuild P$sch$nil = nil"
+apply (subst oraclebuild_unfold)
+apply simp
+done
+
+lemma oraclebuild_cons: "oraclebuild P$s$(x\<leadsto>t) =
+ (Takewhile (%a. \<not> P a)$s)
+ @@ (x\<leadsto>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))"
+apply (rule trans)
+apply (subst oraclebuild_unfold)
+apply (simp add: Consq_def)
+apply (simp add: Consq_def)
+done
+
+
+subsection "Cut rewrite rules"
+
+lemma Cut_nil:
+"[| Forall (%a. \<not> P a) s; Finite s|]
+ ==> Cut P s =nil"
+apply (unfold Cut_def)
+apply (subgoal_tac "Filter P$s = nil")
+apply (simp (no_asm_simp) add: oraclebuild_nil)
+apply (rule ForallQFilterPnil)
+apply assumption+
+done
+
+lemma Cut_UU:
+"[| Forall (%a. \<not> P a) s; ~Finite s|]
+ ==> Cut P s =UU"
+apply (unfold Cut_def)
+apply (subgoal_tac "Filter P$s= UU")
+apply (simp (no_asm_simp) add: oraclebuild_UU)
+apply (rule ForallQFilterPUU)
+apply assumption+
+done
+
+lemma Cut_Cons:
+"[| P t; Forall (%x. \<not> P x) ss; Finite ss|]
+ ==> Cut P (ss @@ (t\<leadsto> rs))
+ = ss @@ (t \<leadsto> Cut P rs)"
+apply (unfold Cut_def)
+apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
+done
+
+
+subsection "Cut lemmas for main theorem"
+
+lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
+prefer 3 apply (fast)
+apply (case_tac "Finite s")
+apply (simp add: Cut_nil ForallQFilterPnil)
+apply (simp add: Cut_UU ForallQFilterPUU)
+(* main case *)
+apply (simp add: Cut_Cons ForallQFilterPnil)
+done
+
+
+lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in
+ take_lemma_less_induct [THEN mp])
+prefer 3 apply (fast)
+apply (case_tac "Finite s")
+apply (simp add: Cut_nil ForallQFilterPnil)
+apply (simp add: Cut_UU ForallQFilterPUU)
+(* main case *)
+apply (simp add: Cut_Cons ForallQFilterPnil)
+apply (rule take_reduction)
+apply auto
+done
+
+
+lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P (f x) " and x1 = "s" in
+ take_lemma_less_induct [THEN mp])
+prefer 3 apply (fast)
+apply (case_tac "Finite s")
+apply (simp add: Cut_nil)
+apply (rule Cut_nil [symmetric])
+apply (simp add: ForallMap o_def)
+apply (simp add: Map2Finite)
+(* csae ~ Finite s *)
+apply (simp add: Cut_UU)
+apply (rule Cut_UU)
+apply (simp add: ForallMap o_def)
+apply (simp add: Map2Finite)
+(* main case *)
+apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
+apply (rule take_reduction)
+apply auto
+done
+
+
+lemma Cut_prefixcl_nFinite [rule_format (no_asm)]: "~Finite s --> Cut P s << s"
+apply (intro strip)
+apply (rule take_lemma_less [THEN iffD1])
+apply (intro strip)
+apply (rule mp)
+prefer 2 apply (assumption)
+apply (tactic "thin_tac' @{context} 1 1")
+apply (rule_tac x = "s" in spec)
+apply (rule nat_less_induct)
+apply (intro strip)
+apply (rename_tac na n s)
+apply (case_tac "Forall (%x. ~ P x) s")
+apply (rule take_lemma_less [THEN iffD2, THEN spec])
+apply (simp add: Cut_UU)
+(* main case *)
+apply (drule divide_Seq3)
+apply (erule exE)+
+apply (erule conjE)+
+apply hypsubst
+apply (simp add: Cut_Cons)
+apply (rule take_reduction_less)
+(* auto makes also reasoning about Finiteness of parts of s ! *)
+apply auto
+done
+
+
+lemma execThruCut: "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)"
+apply (case_tac "Finite ex")
+apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
+apply assumption
+apply (erule exE)
+apply (rule exec_prefix2closed)
+apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
+apply assumption
+apply (erule exec_prefixclosed)
+apply (erule Cut_prefixcl_nFinite)
+done
+
+
+subsection "Main Cut Theorem"
+
+lemma exists_LastActExtsch:
+ "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
+ ==> ? sch. sch : schedules A &
+ tr = Filter (%a. a:ext A)$sch &
+ LastActExtsch A sch"
+
+apply (unfold schedules_def has_schedule_def [abs_def])
+apply auto
+apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
+apply (simp add: executions_def)
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply auto
+apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
+apply (simp (no_asm_simp))
+
+(* Subgoal 1: Lemma: propagation of execution through Cut *)
+
+apply (simp add: execThruCut)
+
+(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
+
+apply (simp (no_asm) add: filter_act_def)
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
+
+apply (rule_tac [2] MapCut [unfolded o_def])
+apply (simp add: FilterCut [symmetric])
+
+(* Subgoal 3: Lemma: Cut idempotent *)
+
+apply (simp (no_asm) add: LastActExtsch_def filter_act_def)
+apply (subgoal_tac "Map fst$ (Cut (%a. fst a: ext A) x2) = Cut (%a. a:ext A) (Map fst$x2) ")
+apply (rule_tac [2] MapCut [unfolded o_def])
+apply (simp add: Cut_idemp)
+done
+
+
+subsection "Further Cut lemmas"
+
+lemma LastActExtimplnil:
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
+ ==> sch=nil"
+apply (unfold LastActExtsch_def)
+apply (drule FilternPnilForallP)
+apply (erule conjE)
+apply (drule Cut_nil)
+apply assumption
+apply simp
+done
+
+lemma LastActExtimplUU:
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
+ ==> sch=UU"
+apply (unfold LastActExtsch_def)
+apply (drule FilternPUUForallP)
+apply (erule conjE)
+apply (drule Cut_UU)
+apply assumption
+apply simp
+done
+
+end