diff -r ec2f0dad8b98 -r 7355fd313cf8 src/HOL/HOLCF/IOA/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy	Tue Jan 12 20:05:53 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy	Tue Jan 12 23:40:33 2016 +0100
@@ -13,39 +13,33 @@
   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 oraclebuild :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
+  where "oraclebuild P =
+    (fix $
+      (LAM h s t.
+        case t of
+          nil \<Rightarrow> nil
+        | x ## xs \<Rightarrow>
+            (case x of
+              UU \<Rightarrow> UU
+            | Def y \<Rightarrow>
+                (Takewhile (\<lambda>x. \<not> P x) $ s) @@
+                (y \<leadsto> (h $ (TL $ (Dropwhile (\<lambda>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 Cut :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> '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)" *)
+definition LastActExtsch :: "('a,'s) ioa \<Rightarrow> 'a Seq \<Rightarrow> bool"
+  where "LastActExtsch A sch \<longleftrightarrow> Cut (\<lambda>x. x \<in> ext A) sch = sch"
 
 axiomatization where
-  Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
+  Cut_prefixcl_Finite: "Finite s \<Longrightarrow> \<exists>y. s = Cut P s @@ y"
 
 axiomatization where
-  LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
+  LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL $ (Dropwhile P $ sch))"
 
 axiomatization where
-  LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
-
+  LastActExtsmall2: "Finite sch1 \<Longrightarrow> LastActExtsch A (sch1 @@ sch2) \<Longrightarrow> LastActExtsch A sch2"
 
 ML \<open>
 fun thin_tac' ctxt j =
@@ -55,224 +49,209 @@
 \<close>
 
 
-subsection "oraclebuild rewrite rules"
-
+subsection \<open>\<open>oraclebuild\<close> rewrite rules\<close>
 
 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
+  "oraclebuild P =
+    (LAM s t.
+      case t of
+        nil \<Rightarrow> nil
+      | x ## xs \<Rightarrow>
+          (case x of
+            UU \<Rightarrow> UU
+          | Def y \<Rightarrow>
+            (Takewhile (\<lambda>a. \<not> P a) $ s) @@
+            (y \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>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_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_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
+lemma oraclebuild_cons:
+  "oraclebuild P $ s $ (x \<leadsto> t) =
+    (Takewhile (\<lambda>a. \<not> P a) $ s) @@
+    (x \<leadsto> (oraclebuild P $ (TL $ (Dropwhile (\<lambda>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"
+subsection \<open>Cut rewrite rules\<close>
 
-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_nil: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> Finite s \<Longrightarrow> Cut P s = nil"
+  apply (unfold Cut_def)
+  apply (subgoal_tac "Filter P $ s = nil")
+  apply (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_UU: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> \<not> Finite s \<Longrightarrow> Cut P s = UU"
+  apply (unfold Cut_def)
+  apply (subgoal_tac "Filter P $ s = UU")
+  apply (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
+  "P t \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ss \<Longrightarrow> Finite ss \<Longrightarrow>
+    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"
+subsection \<open>Cut lemmas for main theorem\<close>
 
-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 FilterCut: "Filter P $ s = Filter P $ (Cut P s)"
+  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>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)
+  text \<open>main case\<close>
+  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
-
+  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>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)
+  text \<open>main case\<close>
+  apply (simp add: Cut_Cons ForallQFilterPnil)
+  apply (rule take_reduction)
+  apply auto
+  done
 
 lemma MapCut: "Map f$(Cut (P \<circ> 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
-
+  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>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)
+  text \<open>case \<open>\<not> Finite s\<close>\<close>
+  apply (simp add: Cut_UU)
+  apply (rule Cut_UU)
+  apply (simp add: ForallMap o_def)
+  apply (simp add: Map2Finite)
+  text \<open>main case\<close>
+  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 Cut_prefixcl_nFinite [rule_format]: "\<not> Finite s \<longrightarrow> Cut P s \<sqsubseteq> 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 (\<lambda>x. \<not> P x) s")
+  apply (rule take_lemma_less [THEN iffD2, THEN spec])
+  apply (simp add: Cut_UU)
+  text \<open>main case\<close>
+  apply (drule divide_Seq3)
+  apply (erule exE)+
+  apply (erule conjE)+
+  apply hypsubst
+  apply (simp add: Cut_Cons)
+  apply (rule take_reduction_less)
+  text \<open>auto makes also reasoning about Finiteness of parts of \<open>s\<close>!\<close>
+  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
+lemma execThruCut: "is_exec_frag A (s, ex) \<Longrightarrow> 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"
+subsection \<open>Main Cut Theorem\<close>
 
 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 *)
+  "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<Longrightarrow>
+    \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) $ sch \<and> LastActExtsch A sch"
+  apply (unfold schedules_def has_schedule_def [abs_def])
+  apply auto
+  apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> 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 (\<lambda>a. fst a \<in> ext A) x2)" in exI)
+  apply simp
 
-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) ")
+  text \<open>Subgoal 1: Lemma:  propagation of execution through \<open>Cut\<close>\<close>
+  apply (simp add: execThruCut)
 
-apply (rule_tac [2] MapCut [unfolded o_def])
-apply (simp add: FilterCut [symmetric])
-
-(* Subgoal 3: Lemma: Cut idempotent  *)
+  text \<open>Subgoal 2:  Lemma:  \<open>Filter P s = Filter P (Cut P s)\<close>\<close>
+  apply (simp add: filter_act_def)
+  apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+  apply (rule_tac [2] MapCut [unfolded o_def])
+  apply (simp add: FilterCut [symmetric])
 
-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
+  text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close>
+  apply (simp add: LastActExtsch_def filter_act_def)
+  apply (subgoal_tac "Map fst $ (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst $ x2)")
+  apply (rule_tac [2] MapCut [unfolded o_def])
+  apply (simp add: Cut_idemp)
+  done
 
 
-subsection "Further Cut lemmas"
+subsection \<open>Further Cut lemmas\<close>
 
-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 LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = nil \<Longrightarrow> 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
+lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) $ sch = UU \<Longrightarrow> sch = UU"
+  apply (unfold LastActExtsch_def)
+  apply (drule FilternPUUForallP)
+  apply (erule conjE)
+  apply (drule Cut_UU)
+  apply assumption
+  apply simp
+  done
 
 end