# HG changeset patch
# User wenzelm
# Date 1452467063 -3600
# Node ID bc178c0fe1a1b13dd17bbe2936797149462a8b5b
# Parent  57895801cb5739a09bbaacff83e10f26490ccfaf
misc tuning and modernization;

diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -22,14 +22,14 @@
 
 definition
  rec :: "'m impl_state => 'm receiver_state" where
- "rec = fst o snd"
+ "rec = fst \<circ> snd"
 
 definition
  srch :: "'m impl_state => 'm packet list" where
- "srch = fst o snd o snd"
+ "srch = fst \<circ> snd \<circ> snd"
 
 definition
  rsch :: "'m impl_state => bool list" where
- "rsch = snd o snd o snd"
+ "rsch = snd \<circ> snd \<circ> snd"
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -24,14 +24,14 @@
 
 definition
   rec_fin :: "'m impl_fin_state => 'm receiver_state" where
-  "rec_fin = fst o snd"
+  "rec_fin = fst \<circ> snd"
 
 definition
   srch_fin :: "'m impl_fin_state => 'm packet list" where
-  "srch_fin = fst o snd o snd"
+  "srch_fin = fst \<circ> snd \<circ> snd"
 
 definition
   rsch_fin :: "'m impl_fin_state => bool list" where
-  "rsch_fin = snd o snd o snd"
+  "rsch_fin = snd \<circ> snd \<circ> snd"
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Asig.thy
--- a/src/HOL/HOLCF/IOA/Asig.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Asig.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -8,94 +8,69 @@
 imports Main
 begin
 
-type_synonym
-  'a signature = "('a set * 'a set * 'a set)"
+type_synonym 'a signature = "'a set \<times> 'a set \<times> 'a set"
 
-definition
-  inputs :: "'action signature => 'action set" where
-  asig_inputs_def: "inputs = fst"
+definition inputs :: "'action signature \<Rightarrow> 'action set"
+  where asig_inputs_def: "inputs = fst"
 
-definition
-  outputs :: "'action signature => 'action set" where
-  asig_outputs_def: "outputs = (fst o snd)"
+definition outputs :: "'action signature \<Rightarrow> 'action set"
+  where asig_outputs_def: "outputs = fst \<circ> snd"
 
-definition
-  internals :: "'action signature => 'action set" where
-  asig_internals_def: "internals = (snd o snd)"
+definition internals :: "'action signature \<Rightarrow> 'action set"
+  where asig_internals_def: "internals = snd \<circ> snd"
 
-definition
-  actions :: "'action signature => 'action set" where
-  "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))"
+definition actions :: "'action signature \<Rightarrow> 'action set"
+  where "actions asig = inputs asig \<union> outputs asig \<union> internals asig"
 
-definition
-  externals :: "'action signature => 'action set" where
-  "externals(asig) = (inputs(asig) Un outputs(asig))"
+definition externals :: "'action signature \<Rightarrow> 'action set"
+  where "externals asig = inputs asig \<union> outputs asig"
 
-definition
-  locals :: "'action signature => 'action set" where
-  "locals asig = ((internals asig) Un (outputs asig))"
+definition locals :: "'action signature \<Rightarrow> 'action set"
+  where "locals asig = internals asig \<union> outputs asig"
 
-definition
-  is_asig :: "'action signature => bool" where
-  "is_asig(triple) =
-     ((inputs(triple) Int outputs(triple) = {}) &
-      (outputs(triple) Int internals(triple) = {}) &
-      (inputs(triple) Int internals(triple) = {}))"
+definition is_asig :: "'action signature \<Rightarrow> bool"
+  where "is_asig triple \<longleftrightarrow>
+    inputs triple \<inter> outputs triple = {} \<and>
+    outputs triple \<inter> internals triple = {} \<and>
+    inputs triple \<inter> internals triple = {}"
 
-definition
-  mk_ext_asig :: "'action signature => 'action signature" where
-  "mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})"
+definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature"
+  where "mk_ext_asig triple = (inputs triple, outputs triple, {})"
 
 
 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
 
 lemma asig_triple_proj:
- "(outputs    (a,b,c) = b)   &
-  (inputs     (a,b,c) = a) &
-  (internals  (a,b,c) = c)"
-  apply (simp add: asig_projections)
-  done
-
-lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
-apply (simp add: externals_def actions_def)
-done
+  "outputs (a, b, c) = b \<and>
+   inputs (a, b, c) = a \<and>
+   internals (a, b, c) = c"
+  by (simp add: asig_projections)
 
-lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
-apply (simp add: externals_def actions_def)
-done
+lemma int_and_ext_is_act: "a \<notin> internals S \<Longrightarrow> a \<notin> externals S \<Longrightarrow> a \<notin> actions S"
+  by (simp add: externals_def actions_def)
 
-lemma int_is_act: "[|a:internals S|] ==> a:actions S"
-apply (simp add: asig_internals_def actions_def)
-done
+lemma ext_is_act: "a \<in> externals S \<Longrightarrow> a \<in> actions S"
+  by (simp add: externals_def actions_def)
 
-lemma inp_is_act: "[|a:inputs S|] ==> a:actions S"
-apply (simp add: asig_inputs_def actions_def)
-done
+lemma int_is_act: "a \<in> internals S \<Longrightarrow> a \<in> actions S"
+  by (simp add: asig_internals_def actions_def)
 
-lemma out_is_act: "[|a:outputs S|] ==> a:actions S"
-apply (simp add: asig_outputs_def actions_def)
-done
+lemma inp_is_act: "a \<in> inputs S \<Longrightarrow> a \<in> actions S"
+  by (simp add: asig_inputs_def actions_def)
 
-lemma ext_and_act: "(x: actions S & x : externals S) = (x: externals S)"
-apply (fast intro!: ext_is_act)
-done
+lemma out_is_act: "a \<in> outputs S \<Longrightarrow> a \<in> actions S"
+  by (simp add: asig_outputs_def actions_def)
 
-lemma not_ext_is_int: "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"
-apply (simp add: actions_def is_asig_def externals_def)
-apply blast
-done
+lemma ext_and_act: "x \<in> actions S \<and> x \<in> externals S \<longleftrightarrow> x \<in> externals S"
+  by (fast intro!: ext_is_act)
 
-lemma not_ext_is_int_or_not_act: "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)"
-apply (simp add: actions_def is_asig_def externals_def)
-apply blast
-done
+lemma not_ext_is_int: "is_asig S \<Longrightarrow> x \<in> actions S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S"
+  by (auto simp add: actions_def is_asig_def externals_def)
 
-lemma int_is_not_ext:
- "[| is_asig (S); x:internals S |] ==> x~:externals S"
-apply (unfold externals_def actions_def is_asig_def)
-apply simp
-apply blast
-done
+lemma not_ext_is_int_or_not_act: "is_asig S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S \<or> x \<notin> actions S"
+  by (auto simp add: actions_def is_asig_def externals_def)
 
+lemma int_is_not_ext:"is_asig S \<Longrightarrow> x \<in> internals S \<Longrightarrow> x \<notin> externals S"
+  by (auto simp add: externals_def actions_def is_asig_def)
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Automata.thy
--- a/src/HOL/HOLCF/IOA/Automata.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Automata.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -10,32 +10,30 @@
 
 default_sort type
 
-type_synonym ('a, 's) transition = "'s * 'a * 's"
+type_synonym ('a, 's) transition = "'s \<times> 'a \<times> 's"
 type_synonym ('a, 's) ioa =
-  "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
+  "'a signature \<times> 's set \<times> ('a, 's)transition set \<times> 'a set set \<times> 'a set set"
 
 
-(* --------------------------------- IOA ---------------------------------*)
+subsection \<open>IO automata\<close>
 
-(* IO automata *)
-
-definition asig_of :: "('a, 's)ioa \<Rightarrow> 'a signature"
+definition asig_of :: "('a, 's) ioa \<Rightarrow> 'a signature"
   where "asig_of = fst"
 
 definition starts_of :: "('a, 's) ioa \<Rightarrow> 's set"
-  where "starts_of = (fst \<circ> snd)"
+  where "starts_of = fst \<circ> snd"
 
 definition trans_of :: "('a, 's) ioa \<Rightarrow> ('a, 's) transition set"
-  where "trans_of = (fst \<circ> snd \<circ> snd)"
+  where "trans_of = fst \<circ> snd \<circ> snd"
 
 abbreviation trans_of_syn  ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81, 81, 81, 81] 100)
   where "s \<midarrow>a\<midarrow>A\<rightarrow> t \<equiv> (s, a, t) \<in> trans_of A"
 
 definition wfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set"
-  where "wfair_of = (fst \<circ> snd \<circ> snd \<circ> snd)"
+  where "wfair_of = fst \<circ> snd \<circ> snd \<circ> snd"
 
 definition sfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set"
-  where "sfair_of = (snd \<circ> snd \<circ> snd \<circ> snd)"
+  where "sfair_of = snd \<circ> snd \<circ> snd \<circ> snd"
 
 definition is_asig_of :: "('a, 's) ioa \<Rightarrow> bool"
   where "is_asig_of A = is_asig (asig_of A)"
@@ -58,121 +56,122 @@
     is_trans_of A \<and>
     input_enabled A"
 
-abbreviation "act A == actions (asig_of A)"
-abbreviation "ext A == externals (asig_of A)"
-abbreviation int where "int A == internals (asig_of A)"
-abbreviation "inp A == inputs (asig_of A)"
-abbreviation "out A == outputs (asig_of A)"
-abbreviation "local A == locals (asig_of A)"
+abbreviation "act A \<equiv> actions (asig_of A)"
+abbreviation "ext A \<equiv> externals (asig_of A)"
+abbreviation int where "int A \<equiv> internals (asig_of A)"
+abbreviation "inp A \<equiv> inputs (asig_of A)"
+abbreviation "out A \<equiv> outputs (asig_of A)"
+abbreviation "local A \<equiv> locals (asig_of A)"
 
-(* invariants *)
-inductive reachable :: "('a, 's) ioa \<Rightarrow> 's \<Rightarrow> bool"
-  for C :: "('a, 's) ioa"
+
+text \<open>invariants\<close>
+
+inductive reachable :: "('a, 's) ioa \<Rightarrow> 's \<Rightarrow> bool" for C :: "('a, 's) ioa"
 where
   reachable_0:  "s \<in> starts_of C \<Longrightarrow> reachable C s"
-| reachable_n:  "\<lbrakk>reachable C s; (s, a, t) \<in> trans_of C\<rbrakk> \<Longrightarrow> reachable C t"
+| reachable_n:  "reachable C s \<Longrightarrow> (s, a, t) \<in> trans_of C \<Longrightarrow> reachable C t"
 
 definition invariant :: "[('a, 's) ioa, 's \<Rightarrow> bool] \<Rightarrow> bool"
   where "invariant A P \<longleftrightarrow> (\<forall>s. reachable A s \<longrightarrow> P s)"
 
 
-(* ------------------------- parallel composition --------------------------*)
+subsection \<open>Parallel composition\<close>
 
-(* binary composition of action signatures and automata *)
+subsubsection \<open>Binary composition of action signatures and automata\<close>
 
-definition compatible :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> bool"
-where
-  "compatible A B \<longleftrightarrow>
-  (((out A \<inter> out B) = {}) \<and>
-   ((int A \<inter> act B) = {}) \<and>
-   ((int B \<inter> act A) = {}))"
+definition compatible :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> bool"
+  where "compatible A B \<longleftrightarrow>
+    out A \<inter> out B = {} \<and>
+    int A \<inter> act B = {} \<and>
+    int B \<inter> act A = {}"
+
+definition asig_comp :: "'a signature \<Rightarrow> 'a signature \<Rightarrow> 'a signature"
+  where "asig_comp a1 a2 =
+     (((inputs a1 \<union> inputs a2) - (outputs a1 \<union> outputs a2),
+       (outputs a1 \<union> outputs a2),
+       (internals a1 \<union> internals a2)))"
 
-definition asig_comp :: "['a signature, 'a signature] \<Rightarrow> 'a signature"
-where
-  "asig_comp a1 a2 =
-     (((inputs(a1) \<union> inputs(a2)) - (outputs(a1) \<union> outputs(a2)),
-       (outputs(a1) \<union> outputs(a2)),
-       (internals(a1) \<union> internals(a2))))"
-
-definition par :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> ('a, 's * 't) ioa"  (infixr "\<parallel>" 10)
-where
-  "(A \<parallel> B) =
-      (asig_comp (asig_of A) (asig_of B),
-       {pr. fst(pr) \<in> starts_of(A) \<and> snd(pr) \<in> starts_of(B)},
-       {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
-            in (a \<in> act A | a:act B) \<and>
-               (if a \<in> act A then
-                  (fst(s), a, fst(t)) \<in> trans_of(A)
-                else fst(t) = fst(s))
-               &
-               (if a \<in> act B then
-                  (snd(s), a, snd(t)) \<in> trans_of(B)
-                else snd(t) = snd(s))},
-        wfair_of A \<union> wfair_of B,
-        sfair_of A \<union> sfair_of B)"
+definition par :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> ('a, 's * 't) ioa"  (infixr "\<parallel>" 10)
+  where "(A \<parallel> B) =
+    (asig_comp (asig_of A) (asig_of B),
+     {pr. fst pr \<in> starts_of A \<and> snd pr \<in> starts_of B},
+     {tr.
+        let
+          s = fst tr;
+          a = fst (snd tr);
+          t = snd (snd tr)
+        in
+          (a \<in> act A \<or> a \<in> act B) \<and>
+          (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A
+           else fst t = fst s) \<and>
+          (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B
+           else snd t = snd s)},
+      wfair_of A \<union> wfair_of B,
+      sfair_of A \<union> sfair_of B)"
 
 
-(* ------------------------ hiding -------------------------------------------- *)
+subsection \<open>Hiding\<close>
 
-(* hiding and restricting *)
+subsubsection \<open>Hiding and restricting\<close>
 
-definition restrict_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature"
-where
-  "restrict_asig asig actns =
-    (inputs(asig) Int actns,
-     outputs(asig) Int actns,
-     internals(asig) Un (externals(asig) - actns))"
+definition restrict_asig :: "'a signature \<Rightarrow> 'a set \<Rightarrow> 'a signature"
+  where "restrict_asig asig actns =
+    (inputs asig \<inter> actns,
+     outputs asig \<inter> actns,
+     internals asig \<union> (externals asig - actns))"
 
-(* Notice that for wfair_of and sfair_of nothing has to be changed, as
-   changes from the outputs to the internals does not touch the locals as
-   a whole, which is of importance for fairness only *)
-definition restrict :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa"
-where
-  "restrict A actns =
+text \<open>
+  Notice that for \<open>wfair_of\<close> and \<open>sfair_of\<close> nothing has to be changed, as
+  changes from the outputs to the internals does not touch the locals as a
+  whole, which is of importance for fairness only.
+\<close>
+definition restrict :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa"
+  where "restrict A actns =
     (restrict_asig (asig_of A) actns,
      starts_of A,
      trans_of A,
      wfair_of A,
      sfair_of A)"
 
-definition hide_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature"
-where
-  "hide_asig asig actns =
-    (inputs(asig) - actns,
-     outputs(asig) - actns,
-     internals(asig) \<union> actns)"
+definition hide_asig :: "'a signature \<Rightarrow> 'a set \<Rightarrow> 'a signature"
+  where "hide_asig asig actns =
+    (inputs asig - actns,
+     outputs asig - actns,
+     internals asig \<union> actns)"
 
-definition hide :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa"
-where
-  "hide A actns =
+definition hide :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa"
+  where "hide A actns =
     (hide_asig (asig_of A) actns,
      starts_of A,
      trans_of A,
      wfair_of A,
      sfair_of A)"
 
-(* ------------------------- renaming ------------------------------------------- *)
+
+subsection \<open>Renaming\<close>
 
 definition rename_set :: "'a set \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> 'c set"
   where "rename_set A ren = {b. \<exists>x. Some x = ren b \<and> x \<in> A}"
 
 definition rename :: "('a, 'b) ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c, 'b) ioa"
-where
-  "rename ioa ren =
+  where "rename ioa ren =
     ((rename_set (inp ioa) ren,
       rename_set (out ioa) ren,
       rename_set (int ioa) ren),
      starts_of ioa,
-     {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))
-          in
-          \<exists>x. Some(x) = ren(a) \<and> (s,x,t):trans_of ioa},
+     {tr.
+        let
+          s = fst tr;
+          a = fst (snd tr);
+          t = snd (snd tr)
+        in \<exists>x. Some x = ren a \<and> s \<midarrow>x\<midarrow>ioa\<rightarrow> t},
      {rename_set s ren | s. s \<in> wfair_of ioa},
      {rename_set s ren | s. s \<in> sfair_of ioa})"
 
 
-(* ------------------------- fairness ----------------------------- *)
+subsection \<open>Fairness\<close>
 
-(* enabledness of actions and action sets *)
+subsubsection \<open>Enabledness of actions and action sets\<close>
 
 definition enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
   where "enabled A a s \<longleftrightarrow> (\<exists>t. s \<midarrow>a\<midarrow>A\<rightarrow> t)"
@@ -181,15 +180,14 @@
   where "Enabled A W s \<longleftrightarrow> (\<exists>w \<in> W. enabled A w s)"
 
 
-(* action set keeps enabled until probably disabled by itself *)
+text \<open>Action set keeps enabled until probably disabled by itself.\<close>
 
 definition en_persistent :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> bool"
-where
-  "en_persistent A W \<longleftrightarrow>
+  where "en_persistent A W \<longleftrightarrow>
     (\<forall>s a t. Enabled A W s \<and> a \<notin> W \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"
 
 
-(* post_conditions for actions and action sets *)
+text \<open>Post conditions for actions and action sets.\<close>
 
 definition was_enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
   where "was_enabled A a t \<longleftrightarrow> (\<exists>s. s \<midarrow>a\<midarrow>A\<rightarrow> t)"
@@ -198,14 +196,13 @@
   where "set_was_enabled A W t \<longleftrightarrow> (\<exists>w \<in> W. was_enabled A w t)"
 
 
-(* constraints for fair IOA *)
+text \<open>Constraints for fair IOA.\<close>
 
 definition fairIOA :: "('a, 's) ioa \<Rightarrow> bool"
   where "fairIOA A \<longleftrightarrow> (\<forall>S \<in> wfair_of A. S \<subseteq> local A) \<and> (\<forall>S \<in> sfair_of A. S \<subseteq> local A)"
 
 definition input_resistant :: "('a, 's) ioa \<Rightarrow> bool"
-where
-  "input_resistant A \<longleftrightarrow>
+  where "input_resistant A \<longleftrightarrow>
     (\<forall>W \<in> sfair_of A. \<forall>s a t.
       reachable A s \<and> reachable A t \<and> a \<in> inp A \<and>
       Enabled A W s \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"
@@ -216,142 +213,116 @@
 lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def
 
 
-subsection "asig_of, starts_of, trans_of"
+subsection "\<open>asig_of\<close>, \<open>starts_of\<close>, \<open>trans_of\<close>"
 
 lemma ioa_triple_proj:
- "((asig_of (x,y,z,w,s)) = x)   &
-  ((starts_of (x,y,z,w,s)) = y) &
-  ((trans_of (x,y,z,w,s)) = z)  &
-  ((wfair_of (x,y,z,w,s)) = w) &
-  ((sfair_of (x,y,z,w,s)) = s)"
-  apply (simp add: ioa_projections)
-  done
+  "asig_of (x, y, z, w, s) = x \<and>
+   starts_of (x, y, z, w, s) = y \<and>
+   trans_of (x, y, z, w, s) = z \<and>
+   wfair_of (x, y, z, w, s) = w \<and>
+   sfair_of (x, y, z, w, s) = s"
+  by (simp add: ioa_projections)
 
-lemma trans_in_actions:
-  "[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A"
-  apply (unfold is_trans_of_def actions_def is_asig_def)
-    apply (erule allE, erule impE, assumption)
-    apply simp
-  done
+lemma trans_in_actions: "is_trans_of A \<Longrightarrow> s1 \<midarrow>a\<midarrow>A\<rightarrow> s2 \<Longrightarrow> a \<in> act A"
+  by (auto simp add: is_trans_of_def actions_def is_asig_def)
 
-lemma starts_of_par: "starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
+lemma starts_of_par: "starts_of (A \<parallel> B) = {p. fst p \<in> starts_of A \<and> snd p \<in> starts_of B}"
   by (simp add: par_def ioa_projections)
 
 lemma trans_of_par:
-"trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
-             in (a:act A | a:act B) &
-                (if a:act A then
-                   (fst(s),a,fst(t)):trans_of(A)
-                 else fst(t) = fst(s))
-                &
-                (if a:act B then
-                   (snd(s),a,snd(t)):trans_of(B)
-                 else snd(t) = snd(s))}"
+  "trans_of(A \<parallel> B) =
+    {tr.
+      let
+        s = fst tr;
+        a = fst (snd tr);
+        t = snd (snd tr)
+      in
+        (a \<in> act A \<or> a \<in> act B) \<and>
+        (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A
+         else fst t = fst s) \<and>
+        (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B
+         else snd t = snd s)}"
   by (simp add: par_def ioa_projections)
 
 
-subsection "actions and par"
+subsection \<open>\<open>actions\<close> and \<open>par\<close>\<close>
 
-lemma actions_asig_comp: "actions(asig_comp a b) = actions(a) Un actions(b)"
+lemma actions_asig_comp: "actions (asig_comp a b) = actions a \<union> actions b"
   by (auto simp add: actions_def asig_comp_def asig_projections)
 
 lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)"
   by (simp add: par_def ioa_projections)
 
-
-lemma externals_of_par: "ext (A1\<parallel>A2) = (ext A1) Un (ext A2)"
-  apply (simp add: externals_def asig_of_par asig_comp_def
+lemma externals_of_par: "ext (A1 \<parallel> A2) = ext A1 \<union> ext A2"
+  by (auto simp add: externals_def asig_of_par asig_comp_def
     asig_inputs_def asig_outputs_def Un_def set_diff_eq)
-  apply blast
-  done
 
-lemma actions_of_par: "act (A1\<parallel>A2) = (act A1) Un (act A2)"
-  apply (simp add: actions_def asig_of_par asig_comp_def
+lemma actions_of_par: "act (A1 \<parallel> A2) = act A1 \<union> act A2"
+  by (auto simp add: actions_def asig_of_par asig_comp_def
     asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
-  apply blast
-  done
 
-lemma inputs_of_par: "inp (A1\<parallel>A2) = ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
+lemma inputs_of_par: "inp (A1 \<parallel> A2) = (inp A1 \<union> inp A2) - (out A1 \<union> out A2)"
   by (simp add: actions_def asig_of_par asig_comp_def
     asig_inputs_def asig_outputs_def Un_def set_diff_eq)
 
-lemma outputs_of_par: "out (A1\<parallel>A2) = (out A1) Un (out A2)"
+lemma outputs_of_par: "out (A1 \<parallel> A2) = out A1 \<union> out A2"
   by (simp add: actions_def asig_of_par asig_comp_def
     asig_outputs_def Un_def set_diff_eq)
 
-lemma internals_of_par: "int (A1\<parallel>A2) = (int A1) Un (int A2)"
+lemma internals_of_par: "int (A1 \<parallel> A2) = int A1 \<union> int A2"
   by (simp add: actions_def asig_of_par asig_comp_def
     asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
 
 
-subsection "actions and compatibility"
+subsection \<open>Actions and compatibility\<close>
 
 lemma compat_commute: "compatible A B = compatible B A"
   by (auto simp add: compatible_def Int_commute)
 
-lemma ext1_is_not_int2: "[| compatible A1 A2; a:ext A1|] ==> a~:int A2"
-  apply (unfold externals_def actions_def compatible_def)
-  apply simp
-  apply blast
-  done
+lemma ext1_is_not_int2: "compatible A1 A2 \<Longrightarrow> a \<in> ext A1 \<Longrightarrow> a \<notin> int A2"
+  by (auto simp add: externals_def actions_def compatible_def)
 
-(* just commuting the previous one: better commute compatible *)
-lemma ext2_is_not_int1: "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2"
-  apply (unfold externals_def actions_def compatible_def)
-  apply simp
-  apply blast
-  done
+(*just commuting the previous one: better commute compatible*)
+lemma ext2_is_not_int1: "compatible A2 A1 \<Longrightarrow> a \<in> ext A1 \<Longrightarrow> a \<notin> int A2"
+  by (auto simp add: externals_def actions_def compatible_def)
 
 lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
 lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
 
-lemma intA_is_not_extB: "[| compatible A B; x:int A |] ==> x~:ext B"
-  apply (unfold externals_def actions_def compatible_def)
-  apply simp
-  apply blast
-  done
+lemma intA_is_not_extB: "compatible A B \<Longrightarrow> x \<in> int A \<Longrightarrow> x \<notin> ext B"
+  by (auto simp add: externals_def actions_def compatible_def)
 
-lemma intA_is_not_actB: "[| compatible A B; a:int A |] ==> a ~: act B"
-  apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def)
-  apply simp
-  apply blast
-  done
+lemma intA_is_not_actB: "compatible A B \<Longrightarrow> a \<in> int A \<Longrightarrow> a \<notin> act B"
+  by (auto simp add: externals_def actions_def compatible_def is_asig_def asig_of_def)
 
-(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
-lemma outAactB_is_inpB: "[| compatible A B; a:out A ;a:act B|] ==> a : inp B"
-  apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
+(*the only one that needs disjointness of outputs and of internals and _all_ acts*)
+lemma outAactB_is_inpB: "compatible A B \<Longrightarrow> a \<in> out A \<Longrightarrow> a \<in> act B \<Longrightarrow> a \<in> inp B"
+  by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def
       compatible_def is_asig_def asig_of_def)
-  apply simp
-  apply blast
-  done
 
-(* needed for propagation of input_enabledness from A,B to A\<parallel>B *)
+(*needed for propagation of input_enabledness from A, B to A \<parallel> B*)
 lemma inpAAactB_is_inpBoroutB:
-  "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"
-  apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
+  "compatible A B \<Longrightarrow> a \<in> inp A \<Longrightarrow> a \<in> act B \<Longrightarrow> a \<in> inp B \<or> a \<in> out B"
+  by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def
       compatible_def is_asig_def asig_of_def)
-  apply simp
-  apply blast
-  done
 
 
-subsection "input_enabledness and par"
+subsection \<open>Input enabledness and par\<close>
 
-(* ugly case distinctions. Heart of proof:
-     1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
-     2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
+(*ugly case distinctions. Heart of proof:
+    1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
+    2. inputs_of_par: outputs are no longer inputs of par. This is important here.*)
 lemma input_enabled_par:
-  "[| compatible A B; input_enabled A; input_enabled B|]
-        ==> input_enabled (A\<parallel>B)"
+  "compatible A B \<Longrightarrow> input_enabled A \<Longrightarrow> input_enabled B \<Longrightarrow> input_enabled (A \<parallel> B)"
   apply (unfold input_enabled_def)
   apply (simp add: Let_def inputs_of_par trans_of_par)
   apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
   apply (simp add: inp_is_act)
   prefer 2
   apply (simp add: inp_is_act)
-  (* a: inp A *)
-  apply (case_tac "a:act B")
-  (* a:act B *)
+  text \<open>\<open>a \<in> inp A\<close>\<close>
+  apply (case_tac "a \<in> act B")
+  text \<open>\<open>a \<in> inp B\<close>\<close>
   apply (erule_tac x = "a" in allE)
   apply simp
   apply (drule inpAAactB_is_inpBoroutB)
@@ -363,9 +334,9 @@
   apply (erule_tac x = "b" in allE)
   apply (erule exE)
   apply (erule exE)
-  apply (rule_tac x = " (s2,s2a) " in exI)
+  apply (rule_tac x = "(s2, s2a)" in exI)
   apply (simp add: inp_is_act)
-  (* a~: act B*)
+  text \<open>\<open>a \<notin> act B\<close>\<close>
   apply (simp add: inp_is_act)
   apply (erule_tac x = "a" in allE)
   apply simp
@@ -373,10 +344,10 @@
   apply (erule exE)
   apply (rule_tac x = " (s2,b) " in exI)
   apply simp
-  
-  (* a:inp B *)
-  apply (case_tac "a:act A")
-  (* a:act A *)
+
+  text \<open>\<open>a \<in> inp B\<close>\<close>
+  apply (case_tac "a \<in> act A")
+  text \<open>\<open>a \<in> act A\<close>\<close>
   apply (erule_tac x = "a" in allE)
   apply (erule_tac x = "a" in allE)
   apply (simp add: inp_is_act)
@@ -390,26 +361,27 @@
   apply (erule_tac x = "b" in allE)
   apply (erule exE)
   apply (erule exE)
-  apply (rule_tac x = " (s2,s2a) " in exI)
+  apply (rule_tac x = "(s2, s2a)" in exI)
   apply (simp add: inp_is_act)
-  (* a~: act B*)
+  text \<open>\<open>a \<notin> act B\<close>\<close>
   apply (simp add: inp_is_act)
   apply (erule_tac x = "a" in allE)
   apply (erule_tac x = "a" in allE)
   apply simp
   apply (erule_tac x = "b" in allE)
   apply (erule exE)
-  apply (rule_tac x = " (aa,s2) " in exI)
+  apply (rule_tac x = "(aa, s2)" in exI)
   apply simp
   done
 
 
-subsection "invariants"
+subsection \<open>Invariants\<close>
 
 lemma invariantI:
-  "[| !!s. s:starts_of(A) ==> P(s);
-      !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |]
-   ==> invariant A P"
+  assumes "\<And>s. s \<in> starts_of A \<Longrightarrow> P s"
+    and "\<And>s t a. reachable A s \<Longrightarrow> P s \<Longrightarrow> (s, a, t) \<in> trans_of A \<longrightarrow> P t"
+  shows "invariant A P"
+  using assms
   apply (unfold invariant_def)
   apply (rule allI)
   apply (rule impI)
@@ -420,26 +392,23 @@
   done
 
 lemma invariantI1:
- "[| !!s. s : starts_of(A) ==> P(s);
-     !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)
-  |] ==> invariant A P"
-  apply (blast intro: invariantI)
-  done
+  assumes "\<And>s. s \<in> starts_of A \<Longrightarrow> P s"
+    and "\<And>s t a. reachable A s \<Longrightarrow> P s \<longrightarrow> (s, a, t) \<in> trans_of A \<longrightarrow> P t"
+  shows "invariant A P"
+  using assms by (blast intro: invariantI)
 
-lemma invariantE: "[| invariant A P; reachable A s |] ==> P(s)"
-  apply (unfold invariant_def)
-  apply blast
-  done
+lemma invariantE: "invariant A P \<Longrightarrow> reachable A s \<Longrightarrow> P s"
+  unfolding invariant_def by blast
 
 
-subsection "restrict"
-
+subsection \<open>\<open>restrict\<close>\<close>
 
 lemmas reachable_0 = reachable.reachable_0
   and reachable_n = reachable.reachable_n
 
-lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) &
-          trans_of(restrict ioa acts) = trans_of(ioa)"
+lemma cancel_restrict_a:
+  "starts_of (restrict ioa acts) = starts_of ioa \<and>
+   trans_of (restrict ioa acts) = trans_of ioa"
   by (simp add: restrict_def ioa_projections)
 
 lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s"
@@ -448,7 +417,7 @@
   apply (simp add: cancel_restrict_a reachable_0)
   apply (erule reachable_n)
   apply (simp add: cancel_restrict_a)
-  (* <--  *)
+  text \<open>\<open>\<longleftarrow>\<close>\<close>
   apply (erule reachable.induct)
   apply (rule reachable_0)
   apply (simp add: cancel_restrict_a)
@@ -457,25 +426,23 @@
   done
 
 lemma acts_restrict: "act (restrict A acts) = act A"
-  apply (simp (no_asm) add: actions_def asig_internals_def
+  by (auto simp add: actions_def asig_internals_def
     asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def)
-  apply auto
-  done
 
-lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
-          trans_of(restrict ioa acts) = trans_of(ioa) &
-          reachable (restrict ioa acts) s = reachable ioa s &
-          act (restrict A acts) = act A"
+lemma cancel_restrict:
+  "starts_of (restrict ioa acts) = starts_of ioa \<and>
+   trans_of (restrict ioa acts) = trans_of ioa \<and>
+   reachable (restrict ioa acts) s = reachable ioa s \<and>
+   act (restrict A acts) = act A"
   by (simp add: cancel_restrict_a cancel_restrict_b acts_restrict)
 
 
-subsection "rename"
+subsection \<open>\<open>rename\<close>\<close>
 
-lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)"
+lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t \<Longrightarrow> (\<exists>x. Some x = f a \<and> s \<midarrow>x\<midarrow>C\<rightarrow> t)"
   by (simp add: Let_def rename_def trans_of_def)
 
-
-lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s"
+lemma reachable_rename: "reachable (rename C g) s \<Longrightarrow> reachable C s"
   apply (erule reachable.induct)
   apply (rule reachable_0)
   apply (simp add: rename_def ioa_projections)
@@ -487,41 +454,44 @@
   done
 
 
-subsection "trans_of(A\<parallel>B)"
+subsection \<open>\<open>trans_of (A \<parallel> B)\<close>\<close>
 
-lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|]
-              ==> (fst s,a,fst t):trans_of A"
+lemma trans_A_proj:
+  "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act A \<Longrightarrow> (fst s, a, fst t) \<in> trans_of A"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|]
-              ==> (snd s,a,snd t):trans_of B"
+lemma trans_B_proj:
+  "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act B \<Longrightarrow> (snd s, a, snd t) \<in> trans_of B"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|]
-              ==> fst s = fst t"
+lemma trans_A_proj2: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<notin> act A \<Longrightarrow> fst s = fst t"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|]
-              ==> snd s = snd t"
+lemma trans_B_proj2: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<notin> act B \<Longrightarrow> snd s = snd t"
+  by (simp add: Let_def par_def trans_of_def)
+
+lemma trans_AB_proj: "(s, a, t) \<in> trans_of (A \<parallel> B) \<Longrightarrow> a \<in> act A \<or> a \<in> act B"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B)
-               ==> a :act A | a :act B"
-  by (simp add: Let_def par_def trans_of_def)
-
-lemma trans_AB: "[|a:act A;a:act B;
-       (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]
-   ==> (s,a,t):trans_of (A\<parallel>B)"
+lemma trans_AB:
+  "a \<in> act A \<Longrightarrow> a \<in> act B \<Longrightarrow>
+  (fst s, a, fst t) \<in> trans_of A \<Longrightarrow>
+  (snd s, a, snd t) \<in> trans_of B \<Longrightarrow>
+  (s, a, t) \<in> trans_of (A \<parallel> B)"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_A_notB: "[|a:act A;a~:act B;
-       (fst s,a,fst t):trans_of A;snd s=snd t|]
-   ==> (s,a,t):trans_of (A\<parallel>B)"
+lemma trans_A_notB:
+  "a \<in> act A \<Longrightarrow> a \<notin> act B \<Longrightarrow>
+  (fst s, a, fst t) \<in> trans_of A \<Longrightarrow>
+  snd s = snd t \<Longrightarrow>
+  (s, a, t) \<in> trans_of (A \<parallel> B)"
   by (simp add: Let_def par_def trans_of_def)
 
-lemma trans_notA_B: "[|a~:act A;a:act B;
-       (snd s,a,snd t):trans_of B;fst s=fst t|]
-   ==> (s,a,t):trans_of (A\<parallel>B)"
+lemma trans_notA_B:
+  "a \<notin> act A \<Longrightarrow> a \<in> act B \<Longrightarrow>
+  (snd s, a, snd t) \<in> trans_of B \<Longrightarrow>
+  fst s = fst t \<Longrightarrow>
+  (s, a, t) \<in> trans_of (A \<parallel> B)"
   by (simp add: Let_def par_def trans_of_def)
 
 lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B
@@ -529,54 +499,55 @@
 
 
 lemma trans_of_par4:
-"((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) =
-  ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |
-    a:actions(asig_of(D))) &
-   (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)
-    else fst t=fst s) &
-   (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)
-    else fst(snd(t))=fst(snd(s))) &
-   (if a:actions(asig_of(C)) then
-      (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)
-    else fst(snd(snd(t)))=fst(snd(snd(s)))) &
-   (if a:actions(asig_of(D)) then
-      (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
-    else snd(snd(snd(t)))=snd(snd(snd(s)))))"
+  "(s, a, t) \<in> trans_of (A \<parallel> B \<parallel> C \<parallel> D) \<longleftrightarrow>
+    ((a \<in> actions (asig_of A) \<or> a \<in> actions (asig_of B) \<or> a \<in> actions (asig_of C) \<or>
+      a \<in> actions (asig_of D)) \<and>
+     (if a \<in> actions (asig_of A)
+      then (fst s, a, fst t) \<in> trans_of A
+      else fst t = fst s) \<and>
+     (if a \<in> actions (asig_of B)
+      then (fst (snd s), a, fst (snd t)) \<in> trans_of B
+      else fst (snd t) = fst (snd s)) \<and>
+     (if a \<in> actions (asig_of C)
+      then (fst (snd (snd s)), a, fst (snd (snd t))) \<in> trans_of C
+      else fst (snd (snd t)) = fst (snd (snd s))) \<and>
+     (if a \<in> actions (asig_of D)
+      then (snd (snd (snd s)), a, snd (snd (snd t))) \<in> trans_of D
+      else snd (snd (snd t)) = snd (snd (snd s))))"
   by (simp add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
 
 
-subsection "proof obligation generator for IOA requirements"
+subsection \<open>Proof obligation generator for IOA requirements\<close>
 
-(* without assumptions on A and B because is_trans_of is also incorporated in \<parallel>def *)
-lemma is_trans_of_par: "is_trans_of (A\<parallel>B)"
+(*without assumptions on A and B because is_trans_of is also incorporated in par_def*)
+lemma is_trans_of_par: "is_trans_of (A \<parallel> B)"
   by (simp add: is_trans_of_def Let_def actions_of_par trans_of_par)
 
-lemma is_trans_of_restrict: "is_trans_of A ==> is_trans_of (restrict A acts)"
+lemma is_trans_of_restrict: "is_trans_of A \<Longrightarrow> is_trans_of (restrict A acts)"
   by (simp add: is_trans_of_def cancel_restrict acts_restrict)
 
-lemma is_trans_of_rename: "is_trans_of A ==> is_trans_of (rename A f)"
+lemma is_trans_of_rename: "is_trans_of A \<Longrightarrow> is_trans_of (rename A f)"
   apply (unfold is_trans_of_def restrict_def restrict_asig_def)
   apply (simp add: Let_def actions_def trans_of_def asig_internals_def
     asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def)
   apply blast
   done
 
-lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|]
-          ==> is_asig_of (A\<parallel>B)"
+lemma is_asig_of_par: "is_asig_of A \<Longrightarrow> is_asig_of B \<Longrightarrow> compatible A B \<Longrightarrow> is_asig_of (A \<parallel> B)"
   apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
     asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
   apply (simp add: asig_of_def)
   apply auto
   done
 
-lemma is_asig_of_restrict: "is_asig_of A ==> is_asig_of (restrict A f)"
+lemma is_asig_of_restrict: "is_asig_of A \<Longrightarrow> is_asig_of (restrict A f)"
   apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def
-             asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
+    asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
   apply simp
   apply auto
   done
 
-lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)"
+lemma is_asig_of_rename: "is_asig_of A \<Longrightarrow> is_asig_of (rename A f)"
   apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
     asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
   apply auto
@@ -588,27 +559,17 @@
   is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename
 
 
-lemma compatible_par: "[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)"
-  apply (unfold compatible_def)
-  apply (simp add: internals_of_par outputs_of_par actions_of_par)
-  apply auto
-  done
+lemma compatible_par: "compatible A B \<Longrightarrow> compatible A C \<Longrightarrow> compatible A (B \<parallel> C)"
+  by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par)
 
-(*  better derive by previous one and compat_commute *)
-lemma compatible_par2: "[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C"
-  apply (unfold compatible_def)
-  apply (simp add: internals_of_par outputs_of_par actions_of_par)
-  apply auto
-  done
+(*better derive by previous one and compat_commute*)
+lemma compatible_par2: "compatible A C \<Longrightarrow> compatible B C \<Longrightarrow> compatible (A \<parallel> B) C"
+  by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par)
 
 lemma compatible_restrict:
-  "[| compatible A B; (ext B - S) Int ext A = {}|]
-        ==> compatible A (restrict B S)"
-  apply (unfold compatible_def)
-  apply (simp add: ioa_triple_proj asig_triple_proj externals_def
+  "compatible A B \<Longrightarrow> (ext B - S) \<inter> ext A = {} \<Longrightarrow> compatible A (restrict B S)"
+  by (auto simp add: compatible_def ioa_triple_proj asig_triple_proj externals_def
     restrict_def restrict_asig_def actions_def)
-  apply auto
-  done
 
 declare split_paired_Ex [simp]
 
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/CompoExecs.thy
--- a/src/HOL/HOLCF/IOA/CompoExecs.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoExecs.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -8,187 +8,154 @@
 imports Traces
 begin
 
-definition
-  ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where
-  "ProjA2 = Map (%x.(fst x,fst(snd x)))"
+definition ProjA2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 's) pairs"
+  where "ProjA2 = Map (\<lambda>x. (fst x, fst (snd x)))"
 
-definition
-  ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where
-  "ProjA ex = (fst (fst ex), ProjA2$(snd ex))"
+definition ProjA :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 's) execution"
+  where "ProjA ex = (fst (fst ex), ProjA2 $ (snd ex))"
 
-definition
-  ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where
-  "ProjB2 = Map (%x.(fst x,snd(snd x)))"
+definition ProjB2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 't) pairs"
+  where "ProjB2 = Map (\<lambda>x. (fst x, snd (snd x)))"
 
-definition
-  ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where
-  "ProjB ex = (snd (fst ex), ProjB2$(snd ex))"
+definition ProjB :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 't) execution"
+  where "ProjB ex = (snd (fst ex), ProjB2 $ (snd ex))"
 
-definition
-  Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where
-  "Filter_ex2 sig = Filter (%x. fst x:actions sig)"
+definition Filter_ex2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('a, 's) pairs"
+  where "Filter_ex2 sig = Filter (\<lambda>x. fst x \<in> actions sig)"
 
-definition
-  Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where
-  "Filter_ex sig ex = (fst ex,Filter_ex2 sig$(snd ex))"
+definition Filter_ex :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> ('a, 's) execution"
+  where "Filter_ex sig ex = (fst ex, Filter_ex2 sig $ (snd ex))"
 
-definition
-  stutter2 :: "'a signature => ('a,'s)pairs -> ('s => tr)" where
-  "stutter2 sig = (fix$(LAM h ex. (%s. case ex of
-      nil => TT
-    | x##xs => (flift1
-            (%p.(If Def ((fst p)~:actions sig)
-                 then Def (s=(snd p))
-                 else TT)
-                andalso (h$xs) (snd p))
-             $x)
-   )))"
+definition stutter2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('s \<Rightarrow> tr)"
+  where "stutter2 sig =
+    (fix $
+      (LAM h ex.
+        (\<lambda>s.
+          case ex of
+            nil \<Rightarrow> TT
+          | x ## xs \<Rightarrow>
+              (flift1
+                (\<lambda>p.
+                  (If Def (fst p \<notin> actions sig) then Def (s = snd p) else TT)
+                  andalso (h$xs) (snd p)) $ x))))"
 
-definition
-  stutter :: "'a signature => ('a,'s)execution => bool" where
-  "stutter sig ex = ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
+definition stutter :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+  where "stutter sig ex \<longleftrightarrow> (stutter2 sig $ (snd ex)) (fst ex) \<noteq> FF"
 
-definition
-  par_execs :: "[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" where
-  "par_execs ExecsA ExecsB =
-      (let exA = fst ExecsA; sigA = snd ExecsA;
-           exB = fst ExecsB; sigB = snd ExecsB
-       in
-       (    {ex. Filter_ex sigA (ProjA ex) : exA}
-        Int {ex. Filter_ex sigB (ProjB ex) : exB}
-        Int {ex. stutter sigA (ProjA ex)}
-        Int {ex. stutter sigB (ProjB ex)}
-        Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
+definition par_execs ::
+  "('a, 's) execution_module \<Rightarrow> ('a, 't) execution_module \<Rightarrow> ('a, 's \<times> 't) execution_module"
+  where "par_execs ExecsA ExecsB =
+    (let
+      exA = fst ExecsA; sigA = snd ExecsA;
+      exB = fst ExecsB; sigB = snd ExecsB
+     in
+       ({ex. Filter_ex sigA (ProjA ex) \<in> exA} \<inter>
+        {ex. Filter_ex sigB (ProjB ex) \<in> exB} \<inter>
+        {ex. stutter sigA (ProjA ex)} \<inter>
+        {ex. stutter sigB (ProjB ex)} \<inter>
+        {ex. Forall (\<lambda>x. fst x \<in> actions sigA \<union> actions sigB) (snd ex)},
         asig_comp sigA sigB))"
 
 
 lemmas [simp del] = split_paired_All
 
 
-section "recursive equations of operators"
-
+section \<open>Recursive equations of operators\<close>
 
-(* ---------------------------------------------------------------- *)
-(*                               ProjA2                             *)
-(* ---------------------------------------------------------------- *)
-
+subsection \<open>\<open>ProjA2\<close>\<close>
 
-lemma ProjA2_UU: "ProjA2$UU = UU"
-apply (simp add: ProjA2_def)
-done
+lemma ProjA2_UU: "ProjA2 $ UU = UU"
+  by (simp add: ProjA2_def)
 
-lemma ProjA2_nil: "ProjA2$nil = nil"
-apply (simp add: ProjA2_def)
-done
+lemma ProjA2_nil: "ProjA2 $ nil = nil"
+  by (simp add: ProjA2_def)
 
-lemma ProjA2_cons: "ProjA2$((a,t)\<leadsto>xs) = (a,fst t) \<leadsto> ProjA2$xs"
-apply (simp add: ProjA2_def)
-done
+lemma ProjA2_cons: "ProjA2 $ ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 $ xs"
+  by (simp add: ProjA2_def)
 
 
-(* ---------------------------------------------------------------- *)
-(*                               ProjB2                             *)
-(* ---------------------------------------------------------------- *)
+subsection \<open>\<open>ProjB2\<close>\<close>
 
-
-lemma ProjB2_UU: "ProjB2$UU = UU"
-apply (simp add: ProjB2_def)
-done
+lemma ProjB2_UU: "ProjB2 $ UU = UU"
+  by (simp add: ProjB2_def)
 
-lemma ProjB2_nil: "ProjB2$nil = nil"
-apply (simp add: ProjB2_def)
-done
+lemma ProjB2_nil: "ProjB2 $ nil = nil"
+  by (simp add: ProjB2_def)
 
-lemma ProjB2_cons: "ProjB2$((a,t)\<leadsto>xs) = (a,snd t) \<leadsto> ProjB2$xs"
-apply (simp add: ProjB2_def)
-done
-
-
-
-(* ---------------------------------------------------------------- *)
-(*                             Filter_ex2                           *)
-(* ---------------------------------------------------------------- *)
+lemma ProjB2_cons: "ProjB2 $ ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 $ xs"
+  by (simp add: ProjB2_def)
 
 
-lemma Filter_ex2_UU: "Filter_ex2 sig$UU=UU"
-apply (simp add: Filter_ex2_def)
-done
+subsection \<open>\<open>Filter_ex2\<close>\<close>
 
-lemma Filter_ex2_nil: "Filter_ex2 sig$nil=nil"
-apply (simp add: Filter_ex2_def)
-done
+lemma Filter_ex2_UU: "Filter_ex2 sig $ UU = UU"
+  by (simp add: Filter_ex2_def)
 
-lemma Filter_ex2_cons: "Filter_ex2 sig$(at \<leadsto> xs) =
-             (if (fst at:actions sig)
-                  then at \<leadsto> (Filter_ex2 sig$xs)
-                  else        Filter_ex2 sig$xs)"
+lemma Filter_ex2_nil: "Filter_ex2 sig $ nil = nil"
+  by (simp add: Filter_ex2_def)
 
-apply (simp add: Filter_ex2_def)
-done
-
-
-(* ---------------------------------------------------------------- *)
-(*                             stutter2                             *)
-(* ---------------------------------------------------------------- *)
+lemma Filter_ex2_cons:
+  "Filter_ex2 sig $ (at \<leadsto> xs) =
+    (if fst at \<in> actions sig
+     then at \<leadsto> (Filter_ex2 sig $ xs)
+     else Filter_ex2 sig $ xs)"
+  by (simp add: Filter_ex2_def)
 
 
-lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of
-       nil => TT
-     | x##xs => (flift1
-             (%p.(If Def ((fst p)~:actions sig)
-                  then Def (s=(snd p))
-                  else TT)
-                 andalso (stutter2 sig$xs) (snd p))
-              $x)
-            ))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (simp only: stutter2_def)
-apply (rule beta_cfun)
-apply (simp add: flift1_def)
-done
+subsection \<open>\<open>stutter2\<close>\<close>
+
+lemma stutter2_unfold:
+  "stutter2 sig =
+    (LAM ex.
+      (\<lambda>s.
+        case ex of
+          nil \<Rightarrow> TT
+        | x ## xs \<Rightarrow>
+            (flift1
+              (\<lambda>p.
+                (If Def (fst p \<notin> actions sig) then Def (s= snd p) else TT)
+                andalso (stutter2 sig$xs) (snd p)) $ x)))"
+  apply (rule trans)
+  apply (rule fix_eq2)
+  apply (simp only: stutter2_def)
+  apply (rule beta_cfun)
+  apply (simp add: flift1_def)
+  done
 
-lemma stutter2_UU: "(stutter2 sig$UU) s=UU"
-apply (subst stutter2_unfold)
-apply simp
-done
+lemma stutter2_UU: "(stutter2 sig $ UU) s = UU"
+  apply (subst stutter2_unfold)
+  apply simp
+  done
 
-lemma stutter2_nil: "(stutter2 sig$nil) s = TT"
-apply (subst stutter2_unfold)
-apply simp
-done
+lemma stutter2_nil: "(stutter2 sig $ nil) s = TT"
+  apply (subst stutter2_unfold)
+  apply simp
+  done
 
-lemma stutter2_cons: "(stutter2 sig$(at\<leadsto>xs)) s =
-               ((if (fst at)~:actions sig then Def (s=snd at) else TT)
-                 andalso (stutter2 sig$xs) (snd at))"
-apply (rule trans)
-apply (subst stutter2_unfold)
-apply (simp add: Consq_def flift1_def If_and_if)
-apply simp
-done
-
+lemma stutter2_cons:
+  "(stutter2 sig $ (at \<leadsto> xs)) s =
+    ((if fst at \<notin> actions sig then Def (s = snd at) else TT)
+      andalso (stutter2 sig $ xs) (snd at))"
+  apply (rule trans)
+  apply (subst stutter2_unfold)
+  apply (simp add: Consq_def flift1_def If_and_if)
+  apply simp
+  done
 
 declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp]
 
 
-(* ---------------------------------------------------------------- *)
-(*                             stutter                              *)
-(* ---------------------------------------------------------------- *)
+subsection \<open>\<open>stutter\<close>\<close>
 
 lemma stutter_UU: "stutter sig (s, UU)"
-apply (simp add: stutter_def)
-done
+  by (simp add: stutter_def)
 
 lemma stutter_nil: "stutter sig (s, nil)"
-apply (simp add: stutter_def)
-done
+  by (simp add: stutter_def)
 
-lemma stutter_cons: "stutter sig (s, (a,t)\<leadsto>ex) =
-      ((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
-apply (simp add: stutter_def)
-done
-
-(* ----------------------------------------------------------------------------------- *)
+lemma stutter_cons:
+  "stutter sig (s, (a, t) \<leadsto> ex) \<longleftrightarrow> (a \<notin> actions sig \<longrightarrow> (s = t)) \<and> stutter sig (t, ex)"
+  by (simp add: stutter_def)
 
 declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del]
 
@@ -200,104 +167,75 @@
 declare compoex_simps [simp]
 
 
-
-(* ------------------------------------------------------------------ *)
-(*                      The following lemmata aim for                 *)
-(*             COMPOSITIONALITY   on    EXECUTION     Level           *)
-(* ------------------------------------------------------------------ *)
-
-
-(* --------------------------------------------------------------------- *)
-(*  Lemma_1_1a : is_ex_fr propagates from A\<parallel>B to Projections A and B    *)
-(* --------------------------------------------------------------------- *)
+section \<open>Compositionality on execution level\<close>
 
-lemma lemma_1_1a: "!s. is_exec_frag (A\<parallel>B) (s,xs)
-       -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
-            is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
-(* main case *)
-apply (auto simp add: trans_of_defs2)
-done
-
-
-(* --------------------------------------------------------------------- *)
-(*  Lemma_1_1b : is_ex_fr (A\<parallel>B) implies stuttering on Projections       *)
-(* --------------------------------------------------------------------- *)
+lemma lemma_1_1a:
+  \<comment> \<open>\<open>is_ex_fr\<close> propagates from \<open>A \<parallel> B\<close> to projections \<open>A\<close> and \<open>B\<close>\<close>
+  "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
+    is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and>
+    is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs))"
+  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  text \<open>main case\<close>
+  apply (auto simp add: trans_of_defs2)
+  done
 
-lemma lemma_1_1b: "!s. is_exec_frag (A\<parallel>B) (s,xs)
-       --> stutter (asig_of A) (fst s,ProjA2$xs)  &
-           stutter (asig_of B) (snd s,ProjB2$xs)"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs"
-  [@{thm stutter_def}, @{thm is_exec_frag_def}] 1\<close>)
-(* main case *)
-apply (auto simp add: trans_of_defs2)
-done
-
-
-(* --------------------------------------------------------------------- *)
-(*  Lemma_1_1c : Executions of A\<parallel>B have only  A- or B-actions           *)
-(* --------------------------------------------------------------------- *)
+lemma lemma_1_1b:
+  \<comment> \<open>\<open>is_ex_fr (A \<parallel> B)\<close> implies stuttering on projections\<close>
+  "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
+    stutter (asig_of A) (fst s, ProjA2 $ xs) \<and>
+    stutter (asig_of B) (snd s, ProjB2 $ xs)"
+  apply (tactic \<open>pair_induct_tac @{context} "xs" @{thms stutter_def is_exec_frag_def} 1\<close>)
+  text \<open>main case\<close>
+  apply (auto simp add: trans_of_defs2)
+  done
 
-lemma lemma_1_1c: "!s. (is_exec_frag (A\<parallel>B) (s,xs)
-   --> Forall (%x. fst x:act (A\<parallel>B)) xs)"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
-  @{thm is_exec_frag_def}] 1\<close>)
-(* main case *)
-apply auto
-apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
-done
-
-
-(* ----------------------------------------------------------------------- *)
-(*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A\<parallel>B)   *)
-(* ----------------------------------------------------------------------- *)
+lemma lemma_1_1c:
+  \<comment> \<open>Executions of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions\<close>
+  "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs"
+  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+    @{thm is_exec_frag_def}] 1\<close>)
+  text \<open>main case\<close>
+  apply auto
+  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
+  done
 
 lemma lemma_1_2:
-"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &
-     is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
-     stutter (asig_of A) (fst s,(ProjA2$xs)) &
-     stutter (asig_of B) (snd s,(ProjB2$xs)) &
-     Forall (%x. fst x:act (A\<parallel>B)) xs
-     --> is_exec_frag (A\<parallel>B) (s,xs)"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
-  @{thm is_exec_frag_def}, @{thm stutter_def}] 1\<close>)
-apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
-done
-
-
-subsection \<open>COMPOSITIONALITY on EXECUTION Level -- Main Theorem\<close>
-
-lemma compositionality_ex:
-"(ex:executions(A\<parallel>B)) =
- (Filter_ex (asig_of A) (ProjA ex) : executions A &
-  Filter_ex (asig_of B) (ProjB ex) : executions B &
-  stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
-  Forall (%x. fst x:act (A\<parallel>B)) (snd ex))"
+  \<comment> \<open>\<open>ex A\<close>, \<open>exB\<close>, stuttering and forall \<open>a \<in> A \<parallel> B\<close> implies \<open>ex (A \<parallel> B)\<close>\<close>
+  "\<forall>s.
+    is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and>
+    is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs)) \<and>
+    stutter (asig_of A) (fst s, ProjA2 $ xs) \<and>
+    stutter (asig_of B) (snd s, ProjB2 $ xs) \<and>
+    Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow>
+    is_exec_frag (A \<parallel> B) (s, xs)"
+  apply (tactic \<open>pair_induct_tac @{context} "xs"
+    @{thms Forall_def sforall_def is_exec_frag_def stutter_def} 1\<close>)
+  apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
+  done
 
-apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (rule iffI)
-(* ==>  *)
-apply (erule conjE)+
-apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c)
-(* <==  *)
-apply (erule conjE)+
-apply (simp add: lemma_1_2)
-done
+theorem compositionality_ex:
+  "ex \<in> executions (A \<parallel> B) \<longleftrightarrow>
+    Filter_ex (asig_of A) (ProjA ex) : executions A \<and>
+    Filter_ex (asig_of B) (ProjB ex) : executions B \<and>
+    stutter (asig_of A) (ProjA ex) \<and>
+    stutter (asig_of B) (ProjB ex) \<and>
+    Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd ex)"
+  apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (rule iffI)
+  text \<open>\<open>\<Longrightarrow>\<close>\<close>
+  apply (erule conjE)+
+  apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c)
+  text \<open>\<open>\<Longleftarrow>\<close>\<close>
+  apply (erule conjE)+
+  apply (simp add: lemma_1_2)
+  done
 
-
-subsection \<open>COMPOSITIONALITY on EXECUTION Level -- for Modules\<close>
-
-lemma compositionality_ex_modules:
-  "Execs (A\<parallel>B) = par_execs (Execs A) (Execs B)"
-apply (unfold Execs_def par_execs_def)
-apply (simp add: asig_of_par)
-apply (rule set_eqI)
-apply (simp add: compositionality_ex actions_of_par)
-done
+theorem compositionality_ex_modules: "Execs (A \<parallel> B) = par_execs (Execs A) (Execs B)"
+  apply (unfold Execs_def par_execs_def)
+  apply (simp add: asig_of_par)
+  apply (rule set_eqI)
+  apply (simp add: compositionality_ex actions_of_par)
+  done
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -8,180 +8,173 @@
 imports CompoExecs
 begin
 
-definition
-  mkex2 :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
-              ('a,'s)pairs -> ('a,'t)pairs ->
-              ('s => 't => ('a,'s*'t)pairs)" where
-  "mkex2 A B = (fix$(LAM h sch exA exB. (%s t. case sch of
-       nil => nil
-    | x##xs =>
-      (case x of
-        UU => UU
-      | Def y =>
-         (if y:act A then
-             (if y:act B then
-                (case HD$exA of
-                   UU => UU
-                 | Def a => (case HD$exB of
-                              UU => UU
-                            | Def b =>
-                   (y,(snd a,snd b))\<leadsto>
-                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
-              else
-                (case HD$exA of
-                   UU => UU
-                 | Def a =>
-                   (y,(snd a,t))\<leadsto>(h$xs$(TL$exA)$exB) (snd a) t)
-              )
-          else
-             (if y:act B then
-                (case HD$exB of
-                   UU => UU
-                 | Def b =>
-                   (y,(s,snd b))\<leadsto>(h$xs$exA$(TL$exB)) s (snd b))
-             else
-               UU
-             )
-         )
-       ))))"
+definition mkex2 :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow>
+  ('a, 's) pairs \<rightarrow> ('a, 't) pairs \<rightarrow> ('s \<Rightarrow> 't \<Rightarrow> ('a, 's \<times> 't) pairs)"
+  where "mkex2 A B =
+    (fix $
+      (LAM h sch exA exB.
+        (\<lambda>s t.
+          case sch of
+            nil \<Rightarrow> nil
+        | x ## xs \<Rightarrow>
+            (case x of
+              UU \<Rightarrow> UU
+            | Def y \<Rightarrow>
+               (if y \<in> act A then
+                 (if y \<in> act B then
+                    (case HD $ exA of
+                      UU \<Rightarrow> UU
+                    | Def a \<Rightarrow>
+                        (case HD $ exB of
+                          UU \<Rightarrow> UU
+                        | Def b \<Rightarrow>
+                           (y, (snd a, snd b)) \<leadsto>
+                            (h $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)))
+                  else
+                    (case HD $ exA of
+                      UU \<Rightarrow> UU
+                    | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h $ xs $ (TL $ exA) $ exB) (snd a) t))
+                else
+                  (if y \<in> act B then
+                    (case HD $ exB of
+                      UU \<Rightarrow> UU
+                    | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h $ xs $ exA $ (TL $ exB)) s (snd b))
+                   else UU))))))"
 
-definition
-  mkex :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
-              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" where
-  "mkex A B sch exA exB =
-       ((fst exA,fst exB),
-        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
+definition mkex :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<Rightarrow>
+    ('a, 's) execution \<Rightarrow> ('a, 't) execution \<Rightarrow> ('a, 's \<times> 't) execution"
+  where "mkex A B sch exA exB =
+    ((fst exA, fst exB), (mkex2 A B $ sch $ (snd exA) $ (snd exB)) (fst exA) (fst exB))"
 
-definition
-  par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" where
-  "par_scheds SchedsA SchedsB =
-      (let schA = fst SchedsA; sigA = snd SchedsA;
-           schB = fst SchedsB; sigB = snd SchedsB
-       in
-       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
-        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
-        Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
+definition par_scheds :: "'a schedule_module \<Rightarrow> 'a schedule_module \<Rightarrow> 'a schedule_module"
+  where "par_scheds SchedsA SchedsB =
+    (let
+      schA = fst SchedsA; sigA = snd SchedsA;
+      schB = fst SchedsB; sigB = snd SchedsB
+     in
+      ({sch. Filter (%a. a:actions sigA)$sch : schA} \<inter>
+       {sch. Filter (%a. a:actions sigB)$sch : schB} \<inter>
+       {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
         asig_comp sigA sigB))"
 
 
-subsection "mkex rewrite rules"
-
+subsection \<open>\<open>mkex\<close> rewrite rules\<close>
 
 lemma mkex2_unfold:
-"mkex2 A B = (LAM sch exA exB. (%s t. case sch of
-      nil => nil
-   | x##xs =>
-     (case x of
-       UU => UU
-     | Def y =>
-        (if y:act A then
-            (if y:act B then
-               (case HD$exA of
-                  UU => UU
-                | Def a => (case HD$exB of
-                             UU => UU
-                           | Def b =>
-                  (y,(snd a,snd b))\<leadsto>
-                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
-             else
-               (case HD$exA of
-                  UU => UU
-                | Def a =>
-                  (y,(snd a,t))\<leadsto>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)
-             )
-         else
-            (if y:act B then
-               (case HD$exB of
-                  UU => UU
-                | Def b =>
-                  (y,(s,snd b))\<leadsto>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))
-            else
-              UU
-            )
-        )
-      )))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (simp only: mkex2_def)
-apply (rule beta_cfun)
-apply simp
-done
+  "mkex2 A B =
+    (LAM sch exA exB.
+      (\<lambda>s t.
+        case sch of
+          nil \<Rightarrow> nil
+        | x ## xs \<Rightarrow>
+            (case x of
+              UU \<Rightarrow> UU
+            | Def y \<Rightarrow>
+                (if y \<in> act A then
+                  (if y \<in> act B then
+                    (case HD $ exA of
+                      UU \<Rightarrow> UU
+                    | Def a \<Rightarrow>
+                        (case HD $ exB of
+                          UU \<Rightarrow> UU
+                        | Def b \<Rightarrow>
+                            (y, (snd a, snd b)) \<leadsto>
+                              (mkex2 A B $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)))
+                   else
+                     (case HD $ exA of
+                       UU \<Rightarrow> UU
+                     | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B $ xs $ (TL $ exA) $ exB) (snd a) t))
+                 else
+                   (if y \<in> act B then
+                     (case HD $ exB of
+                       UU \<Rightarrow> UU
+                     | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B $ xs $ exA $ (TL $ exB)) s (snd b))
+                    else UU)))))"
+  apply (rule trans)
+  apply (rule fix_eq2)
+  apply (simp only: mkex2_def)
+  apply (rule beta_cfun)
+  apply simp
+  done
 
-lemma mkex2_UU: "(mkex2 A B$UU$exA$exB) s t = UU"
-apply (subst mkex2_unfold)
-apply simp
-done
+lemma mkex2_UU: "(mkex2 A B $ UU $ exA $ exB) s t = UU"
+  apply (subst mkex2_unfold)
+  apply simp
+  done
+
+lemma mkex2_nil: "(mkex2 A B $ nil $ exA $ exB) s t = nil"
+  apply (subst mkex2_unfold)
+  apply simp
+  done
 
-lemma mkex2_nil: "(mkex2 A B$nil$exA$exB) s t= nil"
-apply (subst mkex2_unfold)
-apply simp
-done
-
-lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|]
-    ==> (mkex2 A B$(x\<leadsto>sch)$exA$exB) s t =
-        (x,snd a,t) \<leadsto> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t"
-apply (rule trans)
-apply (subst mkex2_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mkex2_cons_1:
+  "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow>
+    (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
+      (x, snd a,t) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ exB) (snd a) t"
+  apply (rule trans)
+  apply (subst mkex2_unfold)
+  apply (simp add: Consq_def If_and_if)
+  apply (simp add: Consq_def)
+  done
 
-lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|]
-    ==> (mkex2 A B$(x\<leadsto>sch)$exA$exB) s t =
-        (x,s,snd b) \<leadsto> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)"
-apply (rule trans)
-apply (subst mkex2_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mkex2_cons_2:
+  "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exB = Def b \<Longrightarrow>
+    (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
+      (x, s, snd b) \<leadsto> (mkex2 A B $ sch $ exA $ (TL $ exB)) s (snd b)"
+  apply (rule trans)
+  apply (subst mkex2_unfold)
+  apply (simp add: Consq_def If_and_if)
+  apply (simp add: Consq_def)
+  done
 
-lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|]
-    ==> (mkex2 A B$(x\<leadsto>sch)$exA$exB) s t =
-         (x,snd a,snd b) \<leadsto>
-            (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"
-apply (rule trans)
-apply (subst mkex2_unfold)
-apply (simp add: Consq_def If_and_if)
-apply (simp add: Consq_def)
-done
+lemma mkex2_cons_3:
+  "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow> HD $ exB = Def b \<Longrightarrow>
+    (mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t =
+      (x, snd a,snd b) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)"
+  apply (rule trans)
+  apply (subst mkex2_unfold)
+  apply (simp add: Consq_def If_and_if)
+  apply (simp add: Consq_def)
+  done
 
 declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp]
   mkex2_cons_2 [simp] mkex2_cons_3 [simp]
 
 
-subsection \<open>mkex\<close>
+subsection \<open>\<open>mkex\<close>\<close>
 
 lemma mkex_UU: "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)"
-apply (simp add: mkex_def)
-done
+  by (simp add: mkex_def)
 
 lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"
-apply (simp add: mkex_def)
-done
+  by (simp add: mkex_def)
 
-lemma mkex_cons_1: "[| x:act A; x~:act B |]
-    ==> mkex A B (x\<leadsto>sch) (s,a\<leadsto>exA) (t,exB)  =
-        ((s,t), (x,snd a,t) \<leadsto> snd (mkex A B sch (snd a,exA) (t,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exA = "a\<leadsto>exA" in mkex2_cons_1)
-apply auto
-done
+lemma mkex_cons_1:
+  "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow>
+    mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, exB) =
+      ((s, t), (x, snd a, t) \<leadsto> snd (mkex A B sch (snd a, exA) (t, exB)))"
+  apply (unfold mkex_def)
+  apply (cut_tac exA = "a \<leadsto> exA" in mkex2_cons_1)
+  apply auto
+  done
 
-lemma mkex_cons_2: "[| x~:act A; x:act B |]
-    ==> mkex A B (x\<leadsto>sch) (s,exA) (t,b\<leadsto>exB) =
-        ((s,t), (x,s,snd b) \<leadsto> snd (mkex A B sch (s,exA) (snd b,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2)
-apply auto
-done
+lemma mkex_cons_2:
+  "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
+    mkex A B (x \<leadsto> sch) (s, exA) (t, b \<leadsto> exB) =
+      ((s, t), (x, s, snd b) \<leadsto> snd (mkex A B sch (s, exA) (snd b, exB)))"
+  apply (unfold mkex_def)
+  apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2)
+  apply auto
+  done
 
-lemma mkex_cons_3: "[| x:act A; x:act B |]
-    ==>  mkex A B (x\<leadsto>sch) (s,a\<leadsto>exA) (t,b\<leadsto>exB) =
-         ((s,t), (x,snd a,snd b) \<leadsto> snd (mkex A B sch (snd a,exA) (snd b,exB)))"
-apply (simp (no_asm) add: mkex_def)
-apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>exA" in mkex2_cons_3)
-apply auto
-done
+lemma mkex_cons_3:
+  "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
+    mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, b \<leadsto> exB) =
+      ((s, t), (x, snd a, snd b) \<leadsto> snd (mkex A B sch (snd a, exA) (snd b, exB)))"
+  apply (unfold mkex_def)
+  apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>exA" in mkex2_cons_3)
+  apply auto
+  done
 
 declare mkex2_UU [simp del] mkex2_nil [simp del]
   mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del]
@@ -191,349 +184,322 @@
 declare composch_simps [simp]
 
 
-subsection \<open>COMPOSITIONALITY on SCHEDULE Level\<close>
-
-subsubsection "Lemmas for ==>"
+subsection \<open>Compositionality on schedule level\<close>
 
-(* --------------------------------------------------------------------- *)
-(*    Lemma_2_1 :  tfilter(ex) and filter_act are commutative            *)
-(* --------------------------------------------------------------------- *)
+subsubsection \<open>Lemmas for \<open>\<Longrightarrow>\<close>\<close>
 
 lemma lemma_2_1a:
-   "filter_act$(Filter_ex2 (asig_of A)$xs)=
-    Filter (%a. a:act A)$(filter_act$xs)"
-
-apply (unfold filter_act_def Filter_ex2_def)
-apply (simp (no_asm) add: MapFilter o_def)
-done
-
-
-(* --------------------------------------------------------------------- *)
-(*    Lemma_2_2 : State-projections do not affect filter_act             *)
-(* --------------------------------------------------------------------- *)
+  \<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close>
+  "filter_act $ (Filter_ex2 (asig_of A) $ xs) =
+    Filter (\<lambda>a. a \<in> act A) $ (filter_act $ xs)"
+  apply (unfold filter_act_def Filter_ex2_def)
+  apply (simp add: MapFilter o_def)
+  done
 
 lemma lemma_2_1b:
-   "filter_act$(ProjA2$xs) =filter_act$xs &
-    filter_act$(ProjB2$xs) =filter_act$xs"
-apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
-done
+  \<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close>
+  "filter_act $ (ProjA2 $ xs) = filter_act $ xs \<and>
+    filter_act $ (ProjB2 $ xs) = filter_act $ xs"
+  by (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
 
 
-(* --------------------------------------------------------------------- *)
-(*             Schedules of A\<parallel>B have only  A- or B-actions              *)
-(* --------------------------------------------------------------------- *)
+text \<open>
+  Schedules of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions.
 
-(* very similar to lemma_1_1c, but it is not checking if every action element of
-   an ex is in A or B, but after projecting it onto the action schedule. Of course, this
-   is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
+  Very similar to \<open>lemma_1_1c\<close>, but it is not checking if every action element
+  of an \<open>ex\<close> is in \<open>A\<close> or \<open>B\<close>, but after projecting it onto the action
+  schedule. Of course, this is the same proposition, but we cannot change this
+  one, when then rather \<open>lemma_1_1c\<close>.
+\<close>
 
-lemma sch_actions_in_AorB: "!s. is_exec_frag (A\<parallel>B) (s,xs)
-   --> Forall (%x. x:act (A\<parallel>B)) (filter_act$xs)"
-
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
-  @{thm sforall_def}] 1\<close>)
-(* main case *)
-apply auto
-apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
-done
+lemma sch_actions_in_AorB:
+  "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act $ xs)"
+  apply (tactic \<open>pair_induct_tac @{context} "xs"
+    @{thms is_exec_frag_def Forall_def sforall_def} 1\<close>)
+  text \<open>main case\<close>
+  apply auto
+  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
+  done
 
 
-subsubsection "Lemmas for <=="
+subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close>
 
-(*---------------------------------------------------------------------------
-    Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
-                             structural induction
-  --------------------------------------------------------------------------- *)
+text \<open>
+  Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close>
+  structural induction.
+\<close>
 
-lemma Mapfst_mkex_is_sch: "! exA exB s t.
-  Forall (%x. x:act (A\<parallel>B)) sch  &
-  Filter (%a. a:act A)$sch << filter_act$exA &
-  Filter (%a. a:act B)$sch << filter_act$exB
-  --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
+lemma Mapfst_mkex_is_sch:
+  "\<forall>exA exB s t.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch"
+  apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+    @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
 
-apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
-  @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
-
-(* main case *)
-(* splitting into 4 cases according to a:A, a:B *)
-apply auto
+  text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
+  apply auto
 
-(* Case y:A, y:B *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
-(* Case exA=UU, Case exA=nil*)
-(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
-   is used! --> to generate a contradiction using  ~a\<leadsto>ss<< UU(nil), using theorems
-   Cons_not_less_UU and Cons_not_less_nil  *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
-(* Case exA=a\<leadsto>x, exB=b\<leadsto>y *)
-(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
-   as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic
-   would not be generally applicable *)
-apply simp
+  text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close>
+  apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
+  text \<open>Case \<open>exA = UU\<close>, Case \<open>exA = nil\<close>\<close>
+  text \<open>
+    These \<open>UU\<close> and \<open>nil\<close> cases are the only places where the assumption
+    \<open>filter A sch \<sqsubseteq> f_act exA\<close> is used!
+    \<open>\<longrightarrow>\<close> to generate a contradiction using \<open>\<not> a \<leadsto> ss \<sqsubseteq> UU nil\<close>,
+    using theorems \<open>Cons_not_less_UU\<close> and \<open>Cons_not_less_nil\<close>.\<close>
+  apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
+  text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close>
+  text \<open>
+    Here it is important that \<open>Seq_case_simp_tac\<close> uses no \<open>!full!_simp_tac\<close>
+    for the cons case, as otherwise \<open>mkex_cons_3\<close> would not be rewritten
+    without use of \<open>rotate_tac\<close>: then tactic would not be generally
+    applicable.\<close>
+  apply simp
 
-(* Case y:A, y~:B *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
-apply simp
+  text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close>
+  apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
+  apply simp
 
-(* Case y~:A, y:B *)
-apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
-apply simp
+  text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close>
+  apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
+  apply simp
 
-(* Case y~:A, y~:B *)
-apply (simp add: asig_of_par actions_asig_comp)
-done
+  text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close>
+  apply (simp add: asig_of_par actions_asig_comp)
+  done
 
 
-(* generalizing the proof above to a proof method *)
-
+text \<open>Generalizing the proof above to a proof method:\<close>
 ML \<open>
 fun mkex_induct_tac ctxt sch exA exB =
-  EVERY'[Seq_induct_tac ctxt sch @{thms Filter_def Forall_def sforall_def mkex_def stutter_def},
-         asm_full_simp_tac ctxt,
-         SELECT_GOAL
-          (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
-         Seq_case_simp_tac ctxt exA,
-         Seq_case_simp_tac ctxt exB,
-         asm_full_simp_tac ctxt,
-         Seq_case_simp_tac ctxt exA,
-         asm_full_simp_tac ctxt,
-         Seq_case_simp_tac ctxt exB,
-         asm_full_simp_tac ctxt,
-         asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})
-        ]
+  EVERY' [
+    Seq_induct_tac ctxt sch
+      @{thms Filter_def Forall_def sforall_def mkex_def stutter_def},
+    asm_full_simp_tac ctxt,
+    SELECT_GOAL
+      (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
+    Seq_case_simp_tac ctxt exA,
+    Seq_case_simp_tac ctxt exB,
+    asm_full_simp_tac ctxt,
+    Seq_case_simp_tac ctxt exA,
+    asm_full_simp_tac ctxt,
+    Seq_case_simp_tac ctxt exB,
+    asm_full_simp_tac ctxt,
+    asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})]
 \<close>
 
 method_setup mkex_induct = \<open>
   Scan.lift (Args.name -- Args.name -- Args.name)
-    >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
+    >> (fn ((sch, exA), exB) => fn ctxt =>
+      SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
 \<close>
 
 
-(*---------------------------------------------------------------------------
-               Projection of mkex(sch,exA,exB) onto A stutters on A
-                             structural induction
-  --------------------------------------------------------------------------- *)
+text \<open>
+  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close>
+  structural induction.
+\<close>
 
-lemma stutterA_mkex: "! exA exB s t.
-  Forall (%x. x:act (A\<parallel>B)) sch &
-  Filter (%a. a:act A)$sch << filter_act$exA &
-  Filter (%a. a:act B)$sch << filter_act$exB
-  --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
+lemma stutterA_mkex:
+  "\<forall>exA exB s t.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    stutter (asig_of A) (s, ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB))))"
   by (mkex_induct sch exA exB)
 
-lemma stutter_mkex_on_A: "[|
-  Forall (%x. x:act (A\<parallel>B)) sch ;
-  Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
-  Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
-  ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
-
-apply (cut_tac stutterA_mkex)
-apply (simp add: stutter_def ProjA_def mkex_def)
-apply (erule allE)+
-apply (drule mp)
-prefer 2 apply (assumption)
-apply simp
-done
+lemma stutter_mkex_on_A:
+  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow>
+    stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
+  apply (cut_tac stutterA_mkex)
+  apply (simp add: stutter_def ProjA_def mkex_def)
+  apply (erule allE)+
+  apply (drule mp)
+  prefer 2 apply (assumption)
+  apply simp
+  done
 
 
-(*---------------------------------------------------------------------------
-               Projection of mkex(sch,exA,exB) onto B stutters on B
-                             structural induction
-  --------------------------------------------------------------------------- *)
+text \<open>
+  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close>
+  structural induction.
+\<close>
 
-lemma stutterB_mkex: "! exA exB s t.
-  Forall (%x. x:act (A\<parallel>B)) sch &
-  Filter (%a. a:act A)$sch << filter_act$exA &
-  Filter (%a. a:act B)$sch << filter_act$exB
-  --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
+lemma stutterB_mkex:
+  "\<forall>exA exB s t.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    stutter (asig_of B) (t, ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB))))"
   by (mkex_induct sch exA exB)
 
 
-lemma stutter_mkex_on_B: "[|
-  Forall (%x. x:act (A\<parallel>B)) sch ;
-  Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
-  Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
-  ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
-apply (cut_tac stutterB_mkex)
-apply (simp add: stutter_def ProjB_def mkex_def)
-apply (erule allE)+
-apply (drule mp)
-prefer 2 apply (assumption)
-apply simp
-done
+lemma stutter_mkex_on_B:
+  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
+   Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow>
+   Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow>
+   stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
+  apply (cut_tac stutterB_mkex)
+  apply (simp add: stutter_def ProjB_def mkex_def)
+  apply (erule allE)+
+  apply (drule mp)
+  prefer 2 apply (assumption)
+  apply simp
+  done
 
 
-(*---------------------------------------------------------------------------
-     Filter of mkex(sch,exA,exB) to A after projection onto A is exA
-        --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
-        --           because of admissibility problems          --
-                             structural induction
-  --------------------------------------------------------------------------- *)
+text \<open>
+  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>,
+  using \<open>zip $ (proj1 $ exA) $ (proj2 $ exA)\<close> instead of \<open>exA\<close>,
+  because of admissibility problems structural induction.
+\<close>
 
-lemma filter_mkex_is_exA_tmp: "! exA exB s t.
-  Forall (%x. x:act (A\<parallel>B)) sch &
-  Filter (%a. a:act A)$sch << filter_act$exA  &
-  Filter (%a. a:act B)$sch << filter_act$exB
-  --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
-      Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
+lemma filter_mkex_is_exA_tmp:
+  "\<forall>exA exB s t.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    Filter_ex2 (asig_of A) $ (ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB)))) =
+      Zip $ (Filter (\<lambda>a. a \<in> act A) $ sch) $ (Map snd $ exA)"
   by (mkex_induct sch exB exA)
 
-(*---------------------------------------------------------------------------
-                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
-                    lemma for admissibility problems
-  --------------------------------------------------------------------------- *)
+text \<open>
+  \<open>zip $ (proj1 $ y) $ (proj2 $ y) = y\<close>  (using the lift operations)
+  lemma for admissibility problems
+\<close>
 
-lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
-apply (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
-done
+lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y"
+  by (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
 
 
-(*---------------------------------------------------------------------------
-      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex
-         lemma for eliminating non admissible equations in assumptions
-  --------------------------------------------------------------------------- *)
+text \<open>
+  \<open>filter A $ sch = proj1 $ ex \<longrightarrow> zip $ (filter A $ sch) $ (proj2 $ ex) = ex\<close>
+  lemma for eliminating non admissible equations in assumptions
+\<close>
+
+lemma trick_against_eq_in_ass:
+  "Filter (\<lambda>a. a \<in> act AB) $ sch = filter_act $ ex \<Longrightarrow>
+    ex = Zip $ (Filter (\<lambda>a. a \<in> act AB) $ sch) $ (Map snd $ ex)"
+  apply (simp add: filter_act_def)
+  apply (rule Zip_Map_fst_snd [symmetric])
+  done
+
+text \<open>
+  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>
+  using the above trick.
+\<close>
 
-lemma trick_against_eq_in_ass: "!! sch ex.
-  Filter (%a. a:act AB)$sch = filter_act$ex
-  ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
-apply (simp add: filter_act_def)
-apply (rule Zip_Map_fst_snd [symmetric])
-done
+lemma filter_mkex_is_exA:
+  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
+  Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
+  apply (simp add: ProjA_def Filter_ex_def)
+  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (rule conjI)
+  apply (simp (no_asm) add: mkex_def)
+  apply (simplesubst trick_against_eq_in_ass)
+  back
+  apply assumption
+  apply (simp add: filter_mkex_is_exA_tmp)
+  done
 
-(*---------------------------------------------------------------------------
-     Filter of mkex(sch,exA,exB) to A after projection onto A is exA
-                       using the above trick
-  --------------------------------------------------------------------------- *)
-
+text \<open>
+  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close>
+  using \<open>zip $ (proj1 $ exB) $ (proj2 $ exB)\<close> instead of \<open>exB\<close>
+  because of admissibility problems structural induction.
+\<close>
 
-lemma filter_mkex_is_exA: "!!sch exA exB.
-  [| Forall (%a. a:act (A\<parallel>B)) sch ;
-  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
-  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
-  ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
-apply (simp add: ProjA_def Filter_ex_def)
-apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-apply (rule conjI)
-apply (simp (no_asm) add: mkex_def)
-apply (simplesubst trick_against_eq_in_ass)
-back
-apply assumption
-apply (simp add: filter_mkex_is_exA_tmp)
-done
+lemma filter_mkex_is_exB_tmp:
+  "\<forall>exA exB s t.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    Filter_ex2 (asig_of B) $ (ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB)))) =
+      Zip $ (Filter (\<lambda>a. a \<in> act B) $ sch) $ (Map snd $ exB)"
+  (*notice necessary change of arguments exA and exB*)
+  by (mkex_induct sch exA exB)
+
+text \<open>
+  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>B\<close> is \<open>exB\<close>
+  using the above trick.
+\<close>
 
-
-(*---------------------------------------------------------------------------
-     Filter of mkex(sch,exA,exB) to B after projection onto B is exB
-        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
-        --           because of admissibility problems          --
-                             structural induction
-  --------------------------------------------------------------------------- *)
+lemma filter_mkex_is_exB:
+  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
+    Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
+  apply (simp add: ProjB_def Filter_ex_def)
+  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (rule conjI)
+  apply (simp (no_asm) add: mkex_def)
+  apply (simplesubst trick_against_eq_in_ass)
+  back
+  apply assumption
+  apply (simp add: filter_mkex_is_exB_tmp)
+  done
 
-lemma filter_mkex_is_exB_tmp: "! exA exB s t.
-  Forall (%x. x:act (A\<parallel>B)) sch &
-  Filter (%a. a:act A)$sch << filter_act$exA  &
-  Filter (%a. a:act B)$sch << filter_act$exB
-  --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
-      Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
-
-(* notice necessary change of arguments exA and exB *)
+lemma mkex_actions_in_AorB:
+  \<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close>
+  "\<forall>s t exA exB.
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch &
+    Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
+    Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))"
   by (mkex_induct sch exA exB)
 
 
-(*---------------------------------------------------------------------------
-     Filter of mkex(sch,exA,exB) to A after projection onto B is exB
-                       using the above trick
-  --------------------------------------------------------------------------- *)
-
-
-lemma filter_mkex_is_exB: "!!sch exA exB.
-  [| Forall (%a. a:act (A\<parallel>B)) sch ;
-  Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
-  Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
-  ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
-apply (simp add: ProjB_def Filter_ex_def)
-apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-apply (rule conjI)
-apply (simp (no_asm) add: mkex_def)
-apply (simplesubst trick_against_eq_in_ass)
-back
-apply assumption
-apply (simp add: filter_mkex_is_exB_tmp)
-done
-
-(* --------------------------------------------------------------------- *)
-(*                    mkex has only  A- or B-actions                    *)
-(* --------------------------------------------------------------------- *)
-
-
-lemma mkex_actions_in_AorB: "!s t exA exB.
-  Forall (%x. x : act (A \<parallel> B)) sch &
-  Filter (%a. a:act A)$sch << filter_act$exA  &
-  Filter (%a. a:act B)$sch << filter_act$exB
-   --> Forall (%x. fst x : act (A \<parallel>B))
-         (snd (mkex A B sch (s,exA) (t,exB)))"
-  by (mkex_induct sch exA exB)
-
-
-(* ------------------------------------------------------------------ *)
-(*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
-(*                          Main Theorem                              *)
-(* ------------------------------------------------------------------ *)
+theorem compositionality_sch:
+  "sch \<in> schedules (A \<parallel> B) \<longleftrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ sch \<in> schedules A \<and>
+    Filter (\<lambda>a. a \<in> act B) $ sch \<in> schedules B \<and>
+    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch"
+  apply (simp add: schedules_def has_schedule_def)
+  apply auto
+  text \<open>\<open>\<Longrightarrow>\<close>\<close>
+  apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI)
+  prefer 2
+  apply (simp add: compositionality_ex)
+  apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
+  apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI)
+  prefer 2
+  apply (simp add: compositionality_ex)
+  apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
+  apply (simp add: executions_def)
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (erule conjE)
+  apply (simp add: sch_actions_in_AorB)
+  text \<open>\<open>\<Longleftarrow>\<close>\<close>
+  text \<open>\<open>mkex\<close> is exactly the construction of \<open>exA\<parallel>B\<close> out of \<open>exA\<close>, \<open>exB\<close>,
+    and the oracle \<open>sch\<close>, we need here\<close>
+  apply (rename_tac exA exB)
+  apply (rule_tac x = "mkex A B sch exA exB" in bexI)
+  text \<open>\<open>mkex\<close> actions are just the oracle\<close>
+  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (simp add: Mapfst_mkex_is_sch)
+  text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close>
+  apply (simp add: compositionality_ex)
+  apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
+  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (simp add: mkex_actions_in_AorB)
+  done
 
-lemma compositionality_sch:
-"(sch : schedules (A\<parallel>B)) =
-  (Filter (%a. a:act A)$sch : schedules A &
-   Filter (%a. a:act B)$sch : schedules B &
-   Forall (%x. x:act (A\<parallel>B)) sch)"
-apply (simp add: schedules_def has_schedule_def)
-apply auto
-(* ==> *)
-apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
-prefer 2
-apply (simp add: compositionality_ex)
-apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
-apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
-prefer 2
-apply (simp add: compositionality_ex)
-apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
-apply (simp add: executions_def)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (erule conjE)
-apply (simp add: sch_actions_in_AorB)
-
-(* <== *)
-
-(* mkex is exactly the construction of exA\<parallel>B out of exA, exB, and the oracle sch,
-   we need here *)
-apply (rename_tac exA exB)
-apply (rule_tac x = "mkex A B sch exA exB" in bexI)
-(* mkex actions are just the oracle *)
-apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-apply (simp add: Mapfst_mkex_is_sch)
-
-(* mkex is an execution -- use compositionality on ex-level *)
-apply (simp add: compositionality_ex)
-apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
-apply (simp add: mkex_actions_in_AorB)
-done
-
-
-subsection \<open>COMPOSITIONALITY on SCHEDULE Level -- for Modules\<close>
-
-lemma compositionality_sch_modules:
-  "Scheds (A\<parallel>B) = par_scheds (Scheds A) (Scheds B)"
-
-apply (unfold Scheds_def par_scheds_def)
-apply (simp add: asig_of_par)
-apply (rule set_eqI)
-apply (simp add: compositionality_sch actions_of_par)
-done
-
+theorem compositionality_sch_modules:
+  "Scheds (A \<parallel> B) = par_scheds (Scheds A) (Scheds B)"
+  apply (unfold Scheds_def par_scheds_def)
+  apply (simp add: asig_of_par)
+  apply (rule set_eqI)
+  apply (simp add: compositionality_sch actions_of_par)
+  done
 
 declare compoex_simps [simp del]
 declare composch_simps [simp del]
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -18,9 +18,9 @@
   impl_def: "impl_ioa == (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
 
 definition sen :: "'m impl_state => 'm sender_state" where "sen = fst"
-definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd"
-definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst o snd o snd"
-definition rsch :: "'m impl_state => bool multiset" where "rsch = snd o snd o snd"
+definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst \<circ> snd"
+definition srch :: "'m impl_state => 'm packet multiset" where "srch = fst \<circ> snd \<circ> snd"
+definition rsch :: "'m impl_state => bool multiset" where "rsch = snd \<circ> snd \<circ> snd"
 
 definition
   hdr_sum :: "'m packet multiset => bool => nat" where
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -15,10 +15,10 @@
 (* messages  #replies        #received            header mode *)
 
 definition rq :: "'m receiver_state => 'm list" where "rq == fst"
-definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd"
-definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd"
-definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd"
-definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd"
+definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst \<circ> snd"
+definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst \<circ> snd \<circ> snd"
+definition rbit :: "'m receiver_state => bool" where "rbit == fst \<circ> snd \<circ> snd \<circ> snd"
+definition rsending :: "'m receiver_state => bool" where "rsending == snd \<circ> snd \<circ> snd \<circ> snd"
 
 definition
   receiver_asig :: "'m action signature" where
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -13,10 +13,10 @@
 (*                messages   #sent           #received      header  mode *)
 
 definition sq :: "'m sender_state => 'm list" where "sq = fst"
-definition ssent :: "'m sender_state => bool multiset" where "ssent = fst o snd"
-definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst o snd o snd"
-definition sbit :: "'m sender_state => bool" where "sbit = fst o snd o snd o snd"
-definition ssending :: "'m sender_state => bool" where "ssending = snd o snd o snd o snd"
+definition ssent :: "'m sender_state => bool multiset" where "ssent = fst \<circ> snd"
+definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst \<circ> snd \<circ> snd"
+definition sbit :: "'m sender_state => bool" where "sbit = fst \<circ> snd \<circ> snd \<circ> snd"
+definition ssending :: "'m sender_state => bool" where "ssending = snd \<circ> snd \<circ> snd \<circ> snd"
 
 definition
   sender_asig :: "'m action signature" where
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Pred.thy
--- a/src/HOL/HOLCF/IOA/Pred.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Pred.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -12,14 +12,14 @@
 
 type_synonym 'a predicate = "'a \<Rightarrow> bool"
 
-definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  ("_ \<Turnstile> _" [100,9] 8)
+definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  ("_ \<Turnstile> _" [100, 9] 8)
   where "(s \<Turnstile> P) \<longleftrightarrow> P s"
 
 definition valid :: "'a predicate \<Rightarrow> bool"  (*  ("|-") *)
   where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
 
 definition NOT :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
-  where "NOT P s \<longleftrightarrow> ~ (P s)"
+  where "NOT P s \<longleftrightarrow> \<not> P s"
 
 definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate"  (infixr "\<^bold>\<and>" 35)
   where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/RefMappings.thy
--- a/src/HOL/HOLCF/IOA/RefMappings.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/RefMappings.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -10,118 +10,103 @@
 
 default_sort type
 
-definition
-  move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
-  "move ioa ex s a t =
-    (is_exec_frag ioa (s,ex) &  Finite ex &
-     laststate (s,ex)=t  &
-     mk_trace ioa$ex = (if a:ext(ioa) then a\<leadsto>nil else nil))"
-
-definition
-  is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_ref_map f C A =
-   ((!s:starts_of(C). f(s):starts_of(A)) &
-   (!s t a. reachable C s &
-            s \<midarrow>a\<midarrow>C\<rightarrow> t
-            --> (? ex. move A ex (f s) a (f t))))"
+definition move :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<Rightarrow> 's \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
+  where "move ioa ex s a t \<longleftrightarrow>
+    is_exec_frag ioa (s, ex) \<and> Finite ex \<and>
+    laststate (s, ex) = t \<and>
+    mk_trace ioa $ ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)"
 
-definition
-  is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_weak_ref_map f C A =
-   ((!s:starts_of(C). f(s):starts_of(A)) &
-   (!s t a. reachable C s &
-            s \<midarrow>a\<midarrow>C\<rightarrow> t
-            --> (if a:ext(C)
-                 then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)
-                 else (f s)=(f t))))"
+definition is_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_ref_map f C A \<longleftrightarrow>
+   ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
+     (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> (\<exists>ex. move A ex (f s) a (f t))))"
 
-
-subsection "transitions and moves"
-
-
-lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t"
-apply (rule_tac x = " (a,t) \<leadsto>nil" in exI)
-apply (simp add: move_def)
-done
+definition is_weak_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_weak_ref_map f C A \<longleftrightarrow>
+    ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
+      (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow>
+        (if a \<in> ext C then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) else f s = f t)))"
 
 
-lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t"
-apply (rule_tac x = "nil" in exI)
-apply (simp add: move_def)
-done
+subsection \<open>Transitions and moves\<close>
 
+lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t \<Longrightarrow> \<exists>ex. move A ex s a t"
+  apply (rule_tac x = " (a, t) \<leadsto> nil" in exI)
+  apply (simp add: move_def)
+  done
+
+lemma nothing_is_ex: "a \<notin> ext A \<and> s = t \<Longrightarrow> \<exists>ex. move A ex s a t"
+  apply (rule_tac x = "nil" in exI)
+  apply (simp add: move_def)
+  done
 
-lemma ei_transitions_are_ex: "(s \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A)  
-         ==> ? ex. move A ex s a s''"
-apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
-apply (simp add: move_def)
-done
+lemma ei_transitions_are_ex:
+  "s \<midarrow>a\<midarrow>A\<rightarrow> s' \<and> s' \<midarrow>a'\<midarrow>A\<rightarrow> s'' \<and> a' \<notin> ext A \<Longrightarrow> \<exists>ex. move A ex s a s''"
+  apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
+  apply (simp add: move_def)
+  done
+
+lemma eii_transitions_are_ex:
+  "s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2 \<and> s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3 \<and> s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4 \<and> a2 \<notin> ext A \<and> a3 \<notin> ext A \<Longrightarrow>
+    \<exists>ex. move A ex s1 a1 s4"
+  apply (rule_tac x = "(a1, s2) \<leadsto> (a2, s3) \<leadsto> (a3, s4) \<leadsto> nil" in exI)
+  apply (simp add: move_def)
+  done
 
 
-lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) & 
-      (~a2:ext A) & (~a3:ext A) ==>  
-      ? ex. move A ex s1 a1 s4"
-apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI)
-apply (simp add: move_def)
-done
-
-
-subsection "weak_ref_map and ref_map"
+subsection \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close>
 
-lemma weak_ref_map2ref_map:
-  "[| ext C = ext A;  
-     is_weak_ref_map f C A |] ==> is_ref_map f C A"
-apply (unfold is_weak_ref_map_def is_ref_map_def)
-apply auto
-apply (case_tac "a:ext A")
-apply (auto intro: transition_is_ex nothing_is_ex)
-done
+lemma weak_ref_map2ref_map: "ext C = ext A \<Longrightarrow> is_weak_ref_map f C A \<Longrightarrow> is_ref_map f C A"
+  apply (unfold is_weak_ref_map_def is_ref_map_def)
+  apply auto
+  apply (case_tac "a \<in> ext A")
+  apply (auto intro: transition_is_ex nothing_is_ex)
+  done
 
-
-lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
+lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
   by blast
 
 declare split_if [split del]
 declare if_weak_cong [cong del]
 
-lemma rename_through_pmap: "[| is_weak_ref_map f C A |]  
-      ==> (is_weak_ref_map f (rename C g) (rename A g))"
-apply (simp add: is_weak_ref_map_def)
-apply (rule conjI)
-(* 1: start states *)
-apply (simp add: rename_def rename_set_def starts_of_def)
-(* 2: reachable transitions *)
-apply (rule allI)+
-apply (rule imp_conj_lemma)
-apply (simp (no_asm) add: rename_def rename_set_def)
-apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
-apply safe
-apply (simplesubst split_if)
- apply (rule conjI)
- apply (rule impI)
- apply (erule disjE)
- apply (erule exE)
-apply (erule conjE)
-(* x is input *)
- apply (drule sym)
- apply (drule sym)
-apply simp
-apply hypsubst+
-apply (frule reachable_rename)
-apply simp
-(* x is output *)
- apply (erule exE)
-apply (erule conjE)
- apply (drule sym)
- apply (drule sym)
-apply simp
-apply hypsubst+
-apply (frule reachable_rename)
-apply simp
-(* x is internal *)
-apply (frule reachable_rename)
-apply auto
-done
+lemma rename_through_pmap:
+  "is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)"
+  apply (simp add: is_weak_ref_map_def)
+  apply (rule conjI)
+  text \<open>1: start states\<close>
+  apply (simp add: rename_def rename_set_def starts_of_def)
+  text \<open>1: start states\<close>
+  apply (rule allI)+
+  apply (rule imp_conj_lemma)
+  apply (simp (no_asm) add: rename_def rename_set_def)
+  apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
+  apply safe
+  apply (simplesubst split_if)
+   apply (rule conjI)
+   apply (rule impI)
+   apply (erule disjE)
+   apply (erule exE)
+  apply (erule conjE)
+  text \<open>\<open>x\<close> is input\<close>
+   apply (drule sym)
+   apply (drule sym)
+  apply simp
+  apply hypsubst+
+  apply (frule reachable_rename)
+  apply simp
+  text \<open>\<open>x\<close> is output\<close>
+   apply (erule exE)
+  apply (erule conjE)
+   apply (drule sym)
+   apply (drule sym)
+  apply simp
+  apply hypsubst+
+  apply (frule reachable_rename)
+  apply simp
+  text \<open>\<open>x\<close> is internal\<close>
+  apply (frule reachable_rename)
+  apply auto
+  done
 
 declare split_if [split]
 declare if_weak_cong [cong]
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Seq.thy
--- a/src/HOL/HOLCF/IOA/Seq.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Seq.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -12,317 +12,273 @@
 
 domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
-(*
-   sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
-   smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
-   sforall       :: "('a -> tr) => 'a seq => bool"
-   sforall2      :: "('a -> tr) -> 'a seq -> tr"
-   slast         :: "'a seq     -> 'a"
-   sconc         :: "'a seq     -> 'a seq -> 'a seq"
-   sdropwhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
-   stakewhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
-   szip          :: "'a seq      -> 'b seq -> ('a*'b) seq"
-   sflat        :: "('a seq) seq  -> 'a seq"
-
-   sfinite       :: "'a seq set"
-   Partial       :: "'a seq => bool"
-   Infinite      :: "'a seq => bool"
-
-   nproj        :: "nat => 'a seq => 'a"
-   sproj        :: "nat => 'a seq => 'a seq"
-*)
-
-inductive
-  Finite :: "'a seq => bool"
-  where
-    sfinite_0:  "Finite nil"
-  | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
+inductive Finite :: "'a seq \<Rightarrow> bool"
+where
+  sfinite_0: "Finite nil"
+| sfinite_n: "Finite tr \<Longrightarrow> a \<noteq> UU \<Longrightarrow> Finite (a ## tr)"
 
 declare Finite.intros [simp]
 
-definition
-  Partial :: "'a seq => bool"
+definition Partial :: "'a seq \<Rightarrow> bool"
+  where "Partial x \<longleftrightarrow> seq_finite x \<and> \<not> Finite x"
+
+definition Infinite :: "'a seq \<Rightarrow> bool"
+  where "Infinite x \<longleftrightarrow> \<not> seq_finite x"
+
+
+subsection \<open>Recursive equations of operators\<close>
+
+subsubsection \<open>\<open>smap\<close>\<close>
+
+fixrec smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a seq \<rightarrow> 'b seq"
 where
-  "Partial x  == (seq_finite x) & ~(Finite x)"
+  smap_nil: "smap $ f $ nil = nil"
+| smap_cons: "x \<noteq> UU \<Longrightarrow> smap $ f $ (x ## xs) = (f $ x) ## smap $ f $ xs"
+
+lemma smap_UU [simp]: "smap $ f $ UU = UU"
+  by fixrec_simp
+
+
+subsubsection \<open>\<open>sfilter\<close>\<close>
 
-definition
-  Infinite :: "'a seq => bool"
+fixrec sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
 where
-  "Infinite x == ~(seq_finite x)"
+  sfilter_nil: "sfilter $ P $ nil = nil"
+| sfilter_cons:
+    "x \<noteq> UU \<Longrightarrow>
+      sfilter $ P $ (x ## xs) =
+      (If P $ x then x ## (sfilter $ P $ xs) else sfilter $ P $ xs)"
+
+lemma sfilter_UU [simp]: "sfilter $ P $ UU = UU"
+  by fixrec_simp
+
+
+subsubsection \<open>\<open>sforall2\<close>\<close>
+
+fixrec sforall2 :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> tr"
+where
+  sforall2_nil: "sforall2 $ P $ nil = TT"
+| sforall2_cons: "x \<noteq> UU \<Longrightarrow> sforall2 $ P $ (x ## xs) = ((P $ x) andalso sforall2 $ P $ xs)"
+
+lemma sforall2_UU [simp]: "sforall2 $ P $ UU = UU"
+  by fixrec_simp
+
+definition "sforall P t = (sforall2 $ P $ t \<noteq> FF)"
 
 
-subsection \<open>recursive equations of operators\<close>
-
-subsubsection \<open>smap\<close>
-
-fixrec
-  smap :: "('a -> 'b) -> 'a seq -> 'b seq"
-where
-  smap_nil: "smap$f$nil=nil"
-| smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
-
-lemma smap_UU [simp]: "smap$f$UU=UU"
-by fixrec_simp
-
-subsubsection \<open>sfilter\<close>
-
-fixrec
-   sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
-where
-  sfilter_nil: "sfilter$P$nil=nil"
-| sfilter_cons:
-    "x~=UU ==> sfilter$P$(x##xs)=
-              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"
+subsubsection \<open>\<open>stakewhile\<close>\<close>
 
-lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
-by fixrec_simp
-
-subsubsection \<open>sforall2\<close>
-
-fixrec
-  sforall2 :: "('a -> tr) -> 'a seq -> tr"
+fixrec stakewhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
 where
-  sforall2_nil: "sforall2$P$nil=TT"
-| sforall2_cons:
-    "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
-
-lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
-by fixrec_simp
-
-definition
-  sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
-
-subsubsection \<open>stakewhile\<close>
-
-fixrec
-  stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"
-where
-  stakewhile_nil: "stakewhile$P$nil=nil"
+  stakewhile_nil: "stakewhile $ P $ nil = nil"
 | stakewhile_cons:
-    "x~=UU ==> stakewhile$P$(x##xs) =
-              (If P$x then x##(stakewhile$P$xs) else nil)"
+    "x \<noteq> UU \<Longrightarrow> stakewhile $ P $ (x ## xs) = (If P $ x then x ## (stakewhile $ P $ xs) else nil)"
+
+lemma stakewhile_UU [simp]: "stakewhile $ P $ UU = UU"
+  by fixrec_simp
 
-lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
-by fixrec_simp
 
-subsubsection \<open>sdropwhile\<close>
+subsubsection \<open>\<open>sdropwhile\<close>\<close>
 
-fixrec
-  sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
+fixrec sdropwhile :: "('a \<rightarrow> tr) \<rightarrow> 'a seq \<rightarrow> 'a seq"
 where
-  sdropwhile_nil: "sdropwhile$P$nil=nil"
+  sdropwhile_nil: "sdropwhile $ P $ nil = nil"
 | sdropwhile_cons:
-    "x~=UU ==> sdropwhile$P$(x##xs) =
-              (If P$x then sdropwhile$P$xs else x##xs)"
+    "x \<noteq> UU \<Longrightarrow> sdropwhile $ P $ (x ## xs) = (If P $ x then sdropwhile $ P $ xs else x ## xs)"
 
-lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
-by fixrec_simp
+lemma sdropwhile_UU [simp]: "sdropwhile $ P $ UU = UU"
+  by fixrec_simp
+
 
-subsubsection \<open>slast\<close>
+subsubsection \<open>\<open>slast\<close>\<close>
 
-fixrec
-  slast :: "'a seq -> 'a"
+fixrec slast :: "'a seq \<rightarrow> 'a"
 where
-  slast_nil: "slast$nil=UU"
-| slast_cons:
-    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"
+  slast_nil: "slast $ nil = UU"
+| slast_cons: "x \<noteq> UU \<Longrightarrow> slast $ (x ## xs) = (If is_nil $ xs then x else slast $ xs)"
 
-lemma slast_UU [simp]: "slast$UU=UU"
-by fixrec_simp
+lemma slast_UU [simp]: "slast $ UU = UU"
+  by fixrec_simp
+
 
-subsubsection \<open>sconc\<close>
+subsubsection \<open>\<open>sconc\<close>\<close>
 
-fixrec
-  sconc :: "'a seq -> 'a seq -> 'a seq"
+fixrec sconc :: "'a seq \<rightarrow> 'a seq \<rightarrow> 'a seq"
 where
-  sconc_nil: "sconc$nil$y = y"
-| sconc_cons':
-    "x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)"
+  sconc_nil: "sconc $ nil $ y = y"
+| sconc_cons': "x \<noteq> UU \<Longrightarrow> sconc $ (x ## xs) $ y = x ## (sconc $ xs $ y)"
 
-abbreviation
-  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
-  "xs @@ ys == sconc $ xs $ ys"
+abbreviation sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65)
+  where "xs @@ ys \<equiv> sconc $ xs $ ys"
 
-lemma sconc_UU [simp]: "UU @@ y=UU"
-by fixrec_simp
+lemma sconc_UU [simp]: "UU @@ y = UU"
+  by fixrec_simp
 
-lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
-apply (cases "x=UU")
-apply simp_all
-done
+lemma sconc_cons [simp]: "(x ## xs) @@ y = x ## (xs @@ y)"
+  by (cases "x = UU") simp_all
 
 declare sconc_cons' [simp del]
 
-subsubsection \<open>sflat\<close>
 
-fixrec
-  sflat :: "('a seq) seq -> 'a seq"
+subsubsection \<open>\<open>sflat\<close>\<close>
+
+fixrec sflat :: "'a seq seq \<rightarrow> 'a seq"
 where
-  sflat_nil: "sflat$nil=nil"
-| sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)"
+  sflat_nil: "sflat $ nil = nil"
+| sflat_cons': "x \<noteq> UU \<Longrightarrow> sflat $ (x ## xs) = x @@ (sflat $ xs)"
 
-lemma sflat_UU [simp]: "sflat$UU=UU"
-by fixrec_simp
+lemma sflat_UU [simp]: "sflat $ UU = UU"
+  by fixrec_simp
 
-lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
-by (cases "x=UU", simp_all)
+lemma sflat_cons [simp]: "sflat $ (x ## xs) = x @@ (sflat $ xs)"
+  by (cases "x = UU") simp_all
 
 declare sflat_cons' [simp del]
 
-subsubsection \<open>szip\<close>
 
-fixrec
-  szip :: "'a seq -> 'b seq -> ('a*'b) seq"
+subsubsection \<open>\<open>szip\<close>\<close>
+
+fixrec szip :: "'a seq \<rightarrow> 'b seq \<rightarrow> ('a \<times> 'b) seq"
 where
-  szip_nil: "szip$nil$y=nil"
-| szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"
-| szip_cons:
-    "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys"
+  szip_nil: "szip $ nil $ y = nil"
+| szip_cons_nil: "x \<noteq> UU \<Longrightarrow> szip $ (x ## xs) $ nil = UU"
+| szip_cons: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> szip $ (x ## xs) $ (y ## ys) = (x, y) ## szip $ xs $ ys"
 
-lemma szip_UU1 [simp]: "szip$UU$y=UU"
-by fixrec_simp
+lemma szip_UU1 [simp]: "szip $ UU $ y = UU"
+  by fixrec_simp
 
-lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
-by (cases x, simp_all, fixrec_simp)
+lemma szip_UU2 [simp]: "x \<noteq> nil \<Longrightarrow> szip $ x $ UU = UU"
+  by (cases x) (simp_all, fixrec_simp)
 
 
-subsection "scons, nil"
-
-lemma scons_inject_eq:
- "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
-by simp
+subsection \<open>\<open>scons\<close>, \<open>nil\<close>\<close>
 
-lemma nil_less_is_nil: "nil<<x ==> nil=x"
-apply (cases x)
-apply simp
-apply simp
-apply simp
-done
+lemma scons_inject_eq: "x \<noteq> UU \<Longrightarrow> y \<noteq> UU \<Longrightarrow> x ## xs = y ## ys \<longleftrightarrow> x = y \<and> xs = ys"
+  by simp
 
-subsection "sfilter, sforall, sconc"
-
-lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr
-        = (if b then tr1 @@ tr else tr2 @@ tr)"
-by simp
+lemma nil_less_is_nil: "nil \<sqsubseteq> x \<Longrightarrow> nil = x"
+  by (cases x) simp_all
 
 
-lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"
-apply (induct x)
-(* adm *)
-apply simp
-(* base cases *)
-apply simp
-apply simp
-(* main case *)
-apply (rule_tac p="P$a" in trE)
-apply simp
-apply simp
-apply simp
-done
+subsection \<open>\<open>sfilter\<close>, \<open>sforall\<close>, \<open>sconc\<close>\<close>
+
+lemma if_and_sconc [simp]:
+  "(if b then tr1 else tr2) @@ tr = (if b then tr1 @@ tr else tr2 @@ tr)"
+  by simp
+
+lemma sfiltersconc: "sfilter $ P $ (x @@ y) = (sfilter $ P $ x @@ sfilter $ P $ y)"
+  apply (induct x)
+  text \<open>adm\<close>
+  apply simp
+  text \<open>base cases\<close>
+  apply simp
+  apply simp
+  text \<open>main case\<close>
+  apply (rule_tac p = "P$a" in trE)
+  apply simp
+  apply simp
+  apply simp
+  done
 
-lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"
-apply (simp add: sforall_def)
-apply (induct x)
-(* adm *)
-apply simp
-(* base cases *)
-apply simp
-apply simp
-(* main case *)
-apply (rule_tac p="P$a" in trE)
-apply simp
-apply simp
-apply simp
-done
+lemma sforallPstakewhileP: "sforall P (stakewhile $ P $ x)"
+  apply (simp add: sforall_def)
+  apply (induct x)
+  text \<open>adm\<close>
+  apply simp
+  text \<open>base cases\<close>
+  apply simp
+  apply simp
+  text \<open>main case\<close>
+  apply (rule_tac p = "P$a" in trE)
+  apply simp
+  apply simp
+  apply simp
+  done
 
-lemma forallPsfilterP: "sforall P (sfilter$P$x)"
-apply (simp add: sforall_def)
-apply (induct x)
-(* adm *)
-apply simp
-(* base cases *)
-apply simp
-apply simp
-(* main case *)
-apply (rule_tac p="P$a" in trE)
-apply simp
-apply simp
-apply simp
-done
+lemma forallPsfilterP: "sforall P (sfilter $ P $ x)"
+  apply (simp add: sforall_def)
+  apply (induct x)
+  text \<open>adm\<close>
+  apply simp
+  text \<open>base cases\<close>
+  apply simp
+  apply simp
+  text \<open>main case\<close>
+  apply (rule_tac p="P$a" in trE)
+  apply simp
+  apply simp
+  apply simp
+  done
 
 
-subsection "Finite"
+subsection \<open>Finite\<close>
 
-(* ----------------------------------------------------  *)
-(* Proofs of rewrite rules for Finite:                  *)
-(* 1. Finite(nil),   (by definition)                    *)
-(* 2. ~Finite(UU),                                      *)
-(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
-(* ----------------------------------------------------  *)
+(*
+  Proofs of rewrite rules for Finite:
+    1. Finite nil    (by definition)
+    2. \<not> Finite UU
+    3. a \<noteq> UU \<Longrightarrow> Finite (a ## x) = Finite x
+*)
 
-lemma Finite_UU_a: "Finite x --> x~=UU"
-apply (rule impI)
-apply (erule Finite.induct)
- apply simp
-apply simp
-done
+lemma Finite_UU_a: "Finite x \<longrightarrow> x \<noteq> UU"
+  apply (rule impI)
+  apply (erule Finite.induct)
+   apply simp
+  apply simp
+  done
 
-lemma Finite_UU [simp]: "~(Finite UU)"
-apply (cut_tac x="UU" in Finite_UU_a)
-apply fast
-done
+lemma Finite_UU [simp]: "\<not> Finite UU"
+  using Finite_UU_a [where x = UU] by fast
 
-lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
-apply (intro strip)
-apply (erule Finite.cases)
-apply fastforce
-apply simp
-done
+lemma Finite_cons_a: "Finite x \<longrightarrow> a \<noteq> UU \<longrightarrow> x = a ## xs \<longrightarrow> Finite xs"
+  apply (intro strip)
+  apply (erule Finite.cases)
+  apply fastforce
+  apply simp
+  done
 
-lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
-apply (rule iffI)
-apply (erule (1) Finite_cons_a [rule_format])
-apply fast
-apply simp
-done
+lemma Finite_cons: "a \<noteq> UU \<Longrightarrow> Finite (a##x) \<longleftrightarrow> Finite x"
+  apply (rule iffI)
+  apply (erule (1) Finite_cons_a [rule_format])
+  apply fast
+  apply simp
+  done
 
-lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
-apply (induct arbitrary: y set: Finite)
-apply (case_tac y, simp, simp, simp)
-apply (case_tac y, simp, simp)
-apply simp
-done
+lemma Finite_upward: "Finite x \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> Finite y"
+  apply (induct arbitrary: y set: Finite)
+  apply (case_tac y, simp, simp, simp)
+  apply (case_tac y, simp, simp)
+  apply simp
+  done
 
 lemma adm_Finite [simp]: "adm Finite"
-by (rule adm_upward, rule Finite_upward)
+  by (rule adm_upward) (rule Finite_upward)
 
 
-subsection "induction"
-
+subsection \<open>Induction\<close>
 
-(*--------------------------------   *)
-(* Extensions to Induction Theorems  *)
-(*--------------------------------   *)
-
+text \<open>Extensions to Induction Theorems.\<close>
 
 lemma seq_finite_ind_lemma:
-  assumes "(!!n. P(seq_take n$s))"
-  shows "seq_finite(s) -->P(s)"
-apply (unfold seq.finite_def)
-apply (intro strip)
-apply (erule exE)
-apply (erule subst)
-apply (rule assms)
-done
+  assumes "\<And>n. P (seq_take n $ s)"
+  shows "seq_finite s \<longrightarrow> P s"
+  apply (unfold seq.finite_def)
+  apply (intro strip)
+  apply (erule exE)
+  apply (erule subst)
+  apply (rule assms)
+  done
 
-
-lemma seq_finite_ind: "!!P.[|P(UU);P(nil);
-   !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)
-   |] ==> seq_finite(s) --> P(s)"
-apply (rule seq_finite_ind_lemma)
-apply (erule seq.finite_induct)
- apply assumption
-apply simp
-done
+lemma seq_finite_ind:
+  assumes "P UU"
+    and "P nil"
+    and "\<And>x s1. x \<noteq> UU \<Longrightarrow> P s1 \<Longrightarrow> P (x ## s1)"
+  shows "seq_finite s \<longrightarrow> P s"
+  apply (insert assms)
+  apply (rule seq_finite_ind_lemma)
+  apply (erule seq.finite_induct)
+   apply assumption
+  apply simp
+  done
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -1,8 +1,8 @@
 (*  Title:      HOL/HOLCF/IOA/Sequence.thy
     Author:     Olaf Müller
+*)
 
-Sequences over flat domains with lifted elements.
-*)
+section \<open>Sequences over flat domains with lifted elements\<close>
 
 theory Sequence
 imports Seq
@@ -34,71 +34,78 @@
   where "Takewhile P = stakewhile $ (flift2 P)"
 
 definition Zip :: "'a Seq \<rightarrow> 'b Seq \<rightarrow> ('a * 'b) Seq"
-where
-  "Zip = (fix$(LAM h t1 t2. case t1 of
-               nil   => nil
-             | x##xs => (case t2 of
-                          nil => UU
-                        | y##ys => (case x of
-                                      UU  => UU
-                                    | Def a => (case y of
-                                                  UU => UU
-                                                | Def b => Def (a,b)##(h$xs$ys))))))"
+  where "Zip =
+    (fix $ (LAM h t1 t2.
+      case t1 of
+        nil \<Rightarrow> nil
+      | x ## xs \<Rightarrow>
+          (case t2 of
+            nil \<Rightarrow> UU
+          | y ## ys \<Rightarrow>
+              (case x of
+                UU \<Rightarrow> UU
+              | Def a \<Rightarrow>
+                  (case y of
+                    UU \<Rightarrow> UU
+                  | Def b \<Rightarrow> Def (a, b) ## (h $ xs $ ys))))))"
 
 definition Flat :: "'a Seq seq \<rightarrow> 'a Seq"
   where "Flat = sflat"
 
 definition Filter2 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
-where
-  "Filter2 P = (fix $ (LAM h t. case t of
-            nil \<Rightarrow> nil
-          | x##xs \<Rightarrow> (case x of UU \<Rightarrow> UU | Def y \<Rightarrow> (if P y
-                     then x##(h$xs)
-                     else     h$xs))))"
+  where "Filter2 P =
+    (fix $
+      (LAM h t.
+        case t of
+          nil \<Rightarrow> nil
+        | x ## xs \<Rightarrow>
+            (case x of
+              UU \<Rightarrow> UU
+            | Def y \<Rightarrow> (if P y then x ## (h $ xs) else h $ xs))))"
 
-abbreviation Consq_syn  ("(_/\<leadsto>_)" [66,65] 65)
-  where "a\<leadsto>s \<equiv> Consq a $ s"
+abbreviation Consq_syn  ("(_/\<leadsto>_)" [66, 65] 65)
+  where "a \<leadsto> s \<equiv> Consq a $ s"
 
 
-text \<open>List enumeration\<close>
+subsection \<open>List enumeration\<close>
+
 syntax
-  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
-  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
+  "_totlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)!]")
+  "_partlist" :: "args \<Rightarrow> 'a Seq"  ("[(_)?]")
 translations
-  "[x, xs!]"     == "x\<leadsto>[xs!]"
-  "[x!]"         == "x\<leadsto>nil"
-  "[x, xs?]"     == "x\<leadsto>[xs?]"
-  "[x?]"         == "x\<leadsto>CONST bottom"
+  "[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
+  "[x!]" \<rightleftharpoons> "x\<leadsto>nil"
+  "[x, xs?]" \<rightleftharpoons> "x \<leadsto> [xs?]"
+  "[x?]" \<rightleftharpoons> "x \<leadsto> CONST bottom"
 
 
 declare andalso_and [simp]
 declare andalso_or [simp]
 
 
-subsection "recursive equations of operators"
+subsection \<open>Recursive equations of operators\<close>
 
-subsubsection "Map"
+subsubsection \<open>Map\<close>
 
-lemma Map_UU: "Map f$UU =UU"
+lemma Map_UU: "Map f $ UU = UU"
   by (simp add: Map_def)
 
-lemma Map_nil: "Map f$nil =nil"
+lemma Map_nil: "Map f $ nil = nil"
   by (simp add: Map_def)
 
-lemma Map_cons: "Map f$(x\<leadsto>xs)=(f x) \<leadsto> Map f$xs"
+lemma Map_cons: "Map f $ (x \<leadsto> xs) = (f x) \<leadsto> Map f $ xs"
   by (simp add: Map_def Consq_def flift2_def)
 
 
 subsubsection \<open>Filter\<close>
 
-lemma Filter_UU: "Filter P$UU =UU"
+lemma Filter_UU: "Filter P $ UU = UU"
   by (simp add: Filter_def)
 
-lemma Filter_nil: "Filter P$nil =nil"
+lemma Filter_nil: "Filter P $ nil = nil"
   by (simp add: Filter_def)
 
-lemma Filter_cons:
-  "Filter P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Filter P$xs) else Filter P$xs)"
+lemma Filter_cons: "Filter P $ (x \<leadsto> xs) = (if P x then x \<leadsto> (Filter P $ xs) else Filter P $ xs)"
   by (simp add: Filter_def Consq_def flift2_def If_and_if)
 
 
@@ -110,81 +117,82 @@
 lemma Forall_nil: "Forall P nil"
   by (simp add: Forall_def sforall_def)
 
-lemma Forall_cons: "Forall P (x\<leadsto>xs)= (P x & Forall P xs)"
+lemma Forall_cons: "Forall P (x \<leadsto> xs) = (P x \<and> Forall P xs)"
   by (simp add: Forall_def sforall_def Consq_def flift2_def)
 
 
 subsubsection \<open>Conc\<close>
 
-lemma Conc_cons: "(x\<leadsto>xs) @@ y = x\<leadsto>(xs @@y)"
+lemma Conc_cons: "(x \<leadsto> xs) @@ y = x \<leadsto> (xs @@ y)"
   by (simp add: Consq_def)
 
 
 subsubsection \<open>Takewhile\<close>
 
-lemma Takewhile_UU: "Takewhile P$UU =UU"
+lemma Takewhile_UU: "Takewhile P $ UU = UU"
   by (simp add: Takewhile_def)
 
-lemma Takewhile_nil: "Takewhile P$nil =nil"
+lemma Takewhile_nil: "Takewhile P $ nil = nil"
   by (simp add: Takewhile_def)
 
 lemma Takewhile_cons:
-  "Takewhile P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Takewhile P$xs) else nil)"
+  "Takewhile P $ (x \<leadsto> xs) = (if P x then x \<leadsto> (Takewhile P $ xs) else nil)"
   by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
 
 
 subsubsection \<open>DropWhile\<close>
 
-lemma Dropwhile_UU: "Dropwhile P$UU =UU"
+lemma Dropwhile_UU: "Dropwhile P $ UU = UU"
   by (simp add: Dropwhile_def)
 
-lemma Dropwhile_nil: "Dropwhile P$nil =nil"
+lemma Dropwhile_nil: "Dropwhile P $ nil = nil"
   by (simp add: Dropwhile_def)
 
-lemma Dropwhile_cons:
-  "Dropwhile P$(x\<leadsto>xs)= (if P x then Dropwhile P$xs else x\<leadsto>xs)"
+lemma Dropwhile_cons: "Dropwhile P $ (x \<leadsto> xs) = (if P x then Dropwhile P $ xs else x \<leadsto> xs)"
   by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
 
 
 subsubsection \<open>Last\<close>
 
-lemma Last_UU: "Last$UU =UU"
-  by (simp add: Last_def)
-
-lemma Last_nil: "Last$nil =UU"
+lemma Last_UU: "Last $ UU =UU"
   by (simp add: Last_def)
 
-lemma Last_cons: "Last$(x\<leadsto>xs)= (if xs=nil then Def x else Last$xs)"
-  apply (simp add: Last_def Consq_def)
-  apply (cases xs)
-  apply simp_all
-  done
+lemma Last_nil: "Last $ nil =UU"
+  by (simp add: Last_def)
+
+lemma Last_cons: "Last $ (x \<leadsto> xs) = (if xs = nil then Def x else Last $ xs)"
+  by (cases xs) (simp_all add: Last_def Consq_def)
 
 
 subsubsection \<open>Flat\<close>
 
-lemma Flat_UU: "Flat$UU =UU"
+lemma Flat_UU: "Flat $ UU = UU"
   by (simp add: Flat_def)
 
-lemma Flat_nil: "Flat$nil =nil"
+lemma Flat_nil: "Flat $ nil = nil"
   by (simp add: Flat_def)
 
-lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
+lemma Flat_cons: "Flat $ (x ## xs) = x @@ (Flat $ xs)"
   by (simp add: Flat_def Consq_def)
 
 
 subsubsection \<open>Zip\<close>
 
 lemma Zip_unfold:
-  "Zip = (LAM t1 t2. case t1 of
-                  nil   => nil
-                | x##xs => (case t2 of
-                             nil => UU
-                           | y##ys => (case x of
-                                         UU  => UU
-                                       | Def a => (case y of
-                                                     UU => UU
-                                                   | Def b => Def (a,b)##(Zip$xs$ys)))))"
+  "Zip =
+    (LAM t1 t2.
+      case t1 of
+        nil \<Rightarrow> nil
+      | x ## xs \<Rightarrow>
+          (case t2 of
+            nil \<Rightarrow> UU
+          | y ## ys \<Rightarrow>
+              (case x of
+                UU \<Rightarrow> UU
+              | Def a \<Rightarrow>
+                  (case y of
+                    UU \<Rightarrow> UU
+                  | Def b \<Rightarrow> Def (a, b) ## (Zip $ xs $ ys)))))"
   apply (rule trans)
   apply (rule fix_eq4)
   apply (rule Zip_def)
@@ -192,29 +200,29 @@
   apply simp
   done
 
-lemma Zip_UU1: "Zip$UU$y =UU"
+lemma Zip_UU1: "Zip $ UU $ y = UU"
   apply (subst Zip_unfold)
   apply simp
   done
 
-lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
+lemma Zip_UU2: "x \<noteq> nil \<Longrightarrow> Zip $ x $ UU = UU"
   apply (subst Zip_unfold)
   apply simp
   apply (cases x)
   apply simp_all
   done
 
-lemma Zip_nil: "Zip$nil$y =nil"
+lemma Zip_nil: "Zip $ nil $ y = nil"
   apply (subst Zip_unfold)
   apply simp
   done
 
-lemma Zip_cons_nil: "Zip$(x\<leadsto>xs)$nil= UU"
+lemma Zip_cons_nil: "Zip $ (x \<leadsto> xs) $ nil = UU"
   apply (subst Zip_unfold)
   apply (simp add: Consq_def)
   done
 
-lemma Zip_cons: "Zip$(x\<leadsto>xs)$(y\<leadsto>ys)= (x,y) \<leadsto> Zip$xs$ys"
+lemma Zip_cons: "Zip $ (x \<leadsto> xs) $ (y \<leadsto> ys) = (x, y) \<leadsto> Zip $ xs $ ys"
   apply (rule trans)
   apply (subst Zip_unfold)
   apply simp
@@ -242,20 +250,18 @@
   Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons
 
 
+subsection \<open>Cons\<close>
 
-section "Cons"
-
-lemma Consq_def2: "a\<leadsto>s = (Def a)##s"
+lemma Consq_def2: "a \<leadsto> s = Def a ## s"
   by (simp add: Consq_def)
 
-lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a \<leadsto> s)"
+lemma Seq_exhaust: "x = UU \<or> x = nil \<or> (\<exists>a s. x = a \<leadsto> s)"
   apply (simp add: Consq_def2)
   apply (cut_tac seq.nchotomy)
   apply (fast dest: not_Undef_is_Def [THEN iffD1])
   done
 
-
-lemma Seq_cases: "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a \<leadsto> s  ==> P |] ==> P"
+lemma Seq_cases: obtains "x = UU" | "x = nil" | a s where "x = a \<leadsto> s"
   apply (cut_tac x="x" in Seq_exhaust)
   apply (erule disjE)
   apply simp
@@ -265,48 +271,34 @@
   apply simp
   done
 
-(*
-fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
-          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
-*)
-(* on a\<leadsto>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
-(*
-fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
-                                             THEN Asm_full_simp_tac (i+1)
-                                             THEN Asm_full_simp_tac i;
-*)
-
-lemma Cons_not_UU: "a\<leadsto>s ~= UU"
+lemma Cons_not_UU: "a \<leadsto> s \<noteq> UU"
   apply (subst Consq_def2)
   apply simp
   done
 
-
-lemma Cons_not_less_UU: "~(a\<leadsto>x) << UU"
+lemma Cons_not_less_UU: "\<not> (a \<leadsto> x) \<sqsubseteq> UU"
   apply (rule notI)
   apply (drule below_antisym)
   apply simp
   apply (simp add: Cons_not_UU)
   done
 
-lemma Cons_not_less_nil: "~a\<leadsto>s << nil"
+lemma Cons_not_less_nil: "\<not> a \<leadsto> s \<sqsubseteq> nil"
   by (simp add: Consq_def2)
 
-lemma Cons_not_nil: "a\<leadsto>s ~= nil"
-  by (simp add: Consq_def2)
-
-lemma Cons_not_nil2: "nil ~= a\<leadsto>s"
+lemma Cons_not_nil: "a \<leadsto> s \<noteq> nil"
   by (simp add: Consq_def2)
 
-lemma Cons_inject_eq: "(a\<leadsto>s = b\<leadsto>t) = (a = b & s = t)"
-  apply (simp only: Consq_def2)
-  apply (simp add: scons_inject_eq)
-  done
-
-lemma Cons_inject_less_eq: "(a\<leadsto>s<<b\<leadsto>t) = (a = b & s<<t)"
+lemma Cons_not_nil2: "nil \<noteq> a \<leadsto> s"
   by (simp add: Consq_def2)
 
-lemma seq_take_Cons: "seq_take (Suc n)$(a\<leadsto>x) = a\<leadsto> (seq_take n$x)"
+lemma Cons_inject_eq: "a \<leadsto> s = b \<leadsto> t \<longleftrightarrow> a = b \<and> s = t"
+  by (simp add: Consq_def2 scons_inject_eq)
+
+lemma Cons_inject_less_eq: "a \<leadsto> s \<sqsubseteq> b \<leadsto> t \<longleftrightarrow> a = b \<and> s \<sqsubseteq> t"
+  by (simp add: Consq_def2)
+
+lemma seq_take_Cons: "seq_take (Suc n) $ (a \<leadsto> x) = a \<leadsto> (seq_take n $ x)"
   by (simp add: Consq_def)
 
 lemmas [simp] =
@@ -314,86 +306,74 @@
   Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil
 
 
-subsection "induction"
+subsection \<open>Induction\<close>
 
-lemma Seq_induct: "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a\<leadsto>s)|] ==> P x"
+lemma Seq_induct:
+  assumes "adm P"
+    and "P UU"
+    and "P nil"
+    and "\<And>a s. P s \<Longrightarrow> P (a \<leadsto> s)"
+  shows "P x"
+  apply (insert assms)
   apply (erule (2) seq.induct)
   apply defined
   apply (simp add: Consq_def)
   done
 
 lemma Seq_FinitePartial_ind:
-  "!! P.[|P UU;P nil; !! a s. P s ==> P(a\<leadsto>s) |]
-                  ==> seq_finite x --> P x"
+  assumes "P UU"
+    and "P nil"
+    and "\<And>a s. P s \<Longrightarrow> P (a \<leadsto> s)"
+  shows "seq_finite x \<longrightarrow> P x"
+  apply (insert assms)
   apply (erule (1) seq_finite_ind)
   apply defined
   apply (simp add: Consq_def)
   done
 
 lemma Seq_Finite_ind:
-  "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a\<leadsto>s) |] ==> P x"
+  assumes "Finite x"
+    and "P nil"
+    and "\<And>a s. Finite s \<Longrightarrow> P s \<Longrightarrow> P (a \<leadsto> s)"
+  shows "P x"
+  apply (insert assms)
   apply (erule (1) Finite.induct)
   apply defined
   apply (simp add: Consq_def)
   done
 
 
-(* rws are definitions to be unfolded for admissibility check *)
-(*
-fun Seq_induct_tac s rws i = rule_tac x",s)] Seq_induct i
-                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
-                         THEN simp add: rws) i;
-
-fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
-                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
+subsection \<open>\<open>HD\<close> and \<open>TL\<close>\<close>
 
-fun pair_tac s = rule_tac p",s)] prod.exhaust
-                          THEN' hyp_subst_tac THEN' Simp_tac;
-*)
-(* induction on a sequence of pairs with pairsplitting and simplification *)
-(*
-fun pair_induct_tac s rws i =
-           rule_tac x",s)] Seq_induct i
-           THEN pair_tac "a" (i+3)
-           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
-           THEN simp add: rws) i;
-*)
+lemma HD_Cons [simp]: "HD $ (x \<leadsto> y) = Def x"
+  by (simp add: Consq_def)
+
+lemma TL_Cons [simp]: "TL $ (x \<leadsto> y) = y"
+  by (simp add: Consq_def)
 
 
-(* ------------------------------------------------------------------------------------ *)
-
-subsection "HD,TL"
-
-lemma HD_Cons [simp]: "HD$(x\<leadsto>y) = Def x"
-  by (simp add: Consq_def)
+subsection \<open>\<open>Finite\<close>, \<open>Partial\<close>, \<open>Infinite\<close>\<close>
 
-lemma TL_Cons [simp]: "TL$(x\<leadsto>y) = y"
-  by (simp add: Consq_def)
-
-(* ------------------------------------------------------------------------------------ *)
-
-subsection "Finite, Partial, Infinite"
-
-lemma Finite_Cons [simp]: "Finite (a\<leadsto>xs) = Finite xs"
+lemma Finite_Cons [simp]: "Finite (a \<leadsto> xs) = Finite xs"
   by (simp add: Consq_def2 Finite_cons)
 
-lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
+lemma FiniteConc_1: "Finite (x::'a Seq) \<Longrightarrow> Finite y \<longrightarrow> Finite (x @@ y)"
   apply (erule Seq_Finite_ind)
   apply simp_all
   done
 
-lemma FiniteConc_2: "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
+lemma FiniteConc_2: "Finite (z::'a Seq) \<Longrightarrow> \<forall>x y. z = x @@ y \<longrightarrow> Finite x \<and> Finite y"
   apply (erule Seq_Finite_ind)
-  (* nil*)
+  text \<open>\<open>nil\<close>\<close>
   apply (intro strip)
   apply (rule_tac x="x" in Seq_cases, simp_all)
-  (* cons *)
+  text \<open>\<open>cons\<close>\<close>
   apply (intro strip)
   apply (rule_tac x="x" in Seq_cases, simp_all)
   apply (rule_tac x="y" in Seq_cases, simp_all)
   done
 
-lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
+lemma FiniteConc [simp]: "Finite (x @@ y) \<longleftrightarrow> Finite (x::'a Seq) \<and> Finite y"
   apply (rule iffI)
   apply (erule FiniteConc_2 [rule_format])
   apply (rule refl)
@@ -402,21 +382,21 @@
   done
 
 
-lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
+lemma FiniteMap1: "Finite s \<Longrightarrow> Finite (Map f $ s)"
   apply (erule Seq_Finite_ind)
   apply simp_all
   done
 
-lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
+lemma FiniteMap2: "Finite s \<Longrightarrow> \<forall>t. s = Map f $ t \<longrightarrow> Finite t"
   apply (erule Seq_Finite_ind)
   apply (intro strip)
   apply (rule_tac x="t" in Seq_cases, simp_all)
-  (* main case *)
+  text \<open>\<open>main case\<close>\<close>
   apply auto
   apply (rule_tac x="t" in Seq_cases, simp_all)
   done
 
-lemma Map2Finite: "Finite (Map f$s) = Finite s"
+lemma Map2Finite: "Finite (Map f $ s) = Finite s"
   apply auto
   apply (erule FiniteMap2 [rule_format])
   apply (rule refl)
@@ -424,17 +404,15 @@
   done
 
 
-lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
+lemma FiniteFilter: "Finite s \<Longrightarrow> Finite (Filter P $ s)"
   apply (erule Seq_Finite_ind)
   apply simp_all
   done
 
 
-(* ----------------------------------------------------------------------------------- *)
+subsection \<open>\<open>Conc\<close>\<close>
 
-subsection "Conc"
-
-lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
+lemma Conc_cong: "\<And>x::'a Seq. Finite x \<Longrightarrow> (x @@ y) = (x @@ z) \<longleftrightarrow> y = z"
   apply (erule Seq_Finite_ind)
   apply simp_all
   done
@@ -453,81 +431,60 @@
   done
 
 
-(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
-lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
+(*Should be same as nil_is_Conc2 when all nils are turned to right side!*)
+lemma nil_is_Conc: "nil = x @@ y \<longleftrightarrow> (x::'a Seq) = nil \<and> y = nil"
   apply (rule_tac x="x" in Seq_cases)
   apply auto
   done
 
-lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
+lemma nil_is_Conc2: "x @@ y = nil \<longleftrightarrow> (x::'a Seq) = nil \<and> y = nil"
   apply (rule_tac x="x" in Seq_cases)
   apply auto
   done
 
 
-(* ------------------------------------------------------------------------------------ *)
-
-subsection "Last"
-
-lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+subsection \<open>Last\<close>
 
-lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
-  apply (erule Seq_Finite_ind, simp_all)
-  apply fast
-  done
+lemma Finite_Last1: "Finite s \<Longrightarrow> s \<noteq> nil \<longrightarrow> Last $ s \<noteq> UU"
+  by (erule Seq_Finite_ind) simp_all
 
-
-(* ------------------------------------------------------------------------------------ *)
-
-
-subsection "Filter, Conc"
+lemma Finite_Last2: "Finite s \<Longrightarrow> Last $ s = UU \<longrightarrow> s = nil"
+  by (erule Seq_Finite_ind) auto
 
 
-lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
-  apply (rule_tac x="s" in Seq_induct, simp_all)
-  done
-
-lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
-  apply (simp add: Filter_def sfiltersconc)
-  done
-
-(* ------------------------------------------------------------------------------------ *)
-
-subsection "Map"
+subsection \<open>Filter, Conc\<close>
 
-lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
-  apply (rule_tac x="s" in Seq_induct, simp_all)
-  done
-
-lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
-  apply (rule_tac x="x" in Seq_induct, simp_all)
-  done
+lemma FilterPQ: "Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
+  by (rule_tac x="s" in Seq_induct) simp_all
 
-lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
-  apply (rule_tac x="x" in Seq_induct, simp_all)
-  done
-
-lemma nilMap: "nil = (Map f$s) --> s= nil"
-  apply (rule_tac x="s" in Seq_cases, simp_all)
-  done
+lemma FilterConc: "Filter P $ (x @@ y) = (Filter P $ x @@ Filter P $ y)"
+  by (simp add: Filter_def sfiltersconc)
 
 
-lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
+subsection \<open>Map\<close>
+
+lemma MapMap: "Map f $ (Map g $ s) = Map (f \<circ> g) $ s"
+  by (rule_tac x="s" in Seq_induct) simp_all
+
+lemma MapConc: "Map f $ (x @@ y) = (Map f $ x) @@ (Map f $ y)"
+  by (rule_tac x="x" in Seq_induct) simp_all
+
+lemma MapFilter: "Filter P $ (Map f $ x) = Map f $ (Filter (P \<circ> f) $ x)"
+  by (rule_tac x="x" in Seq_induct) simp_all
+
+lemma nilMap: "nil = (Map f $ s) \<longrightarrow> s = nil"
+  by (rule_tac x="s" in Seq_cases) simp_all
+
+lemma ForallMap: "Forall P (Map f $ s) = Forall (P \<circ> f) s"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
 
-
-
-(* ------------------------------------------------------------------------------------ *)
+subsection \<open>Forall\<close>
 
-subsection "Forall"
-
-lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x) --> Forall Q ys"
+lemma ForallPForallQ1: "Forall P ys \<and> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> Forall Q ys"
   apply (rule_tac x="ys" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -536,18 +493,16 @@
 lemmas ForallPForallQ =
   ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
 
-lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
+lemma Forall_Conc_impl: "Forall P x \<and> Forall P y \<longrightarrow> Forall P (x @@ y)"
   apply (rule_tac x="x" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
-lemma Forall_Conc [simp]:
-  "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+lemma Forall_Conc [simp]: "Finite x \<Longrightarrow> Forall P (x @@ y) \<longleftrightarrow> Forall P x \<and> Forall P y"
+  by (erule Seq_Finite_ind) simp_all
 
-lemma ForallTL1: "Forall P s  --> Forall P (TL$s)"
+lemma ForallTL1: "Forall P s \<longrightarrow> Forall P (TL $ s)"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -555,7 +510,7 @@
 
 lemmas ForallTL = ForallTL1 [THEN mp]
 
-lemma ForallDropwhile1: "Forall P s  --> Forall P (Dropwhile Q$s)"
+lemma ForallDropwhile1: "Forall P s \<longrightarrow> Forall P (Dropwhile Q $ s)"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -564,9 +519,8 @@
 lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
 
 
-(* only admissible in t, not if done in s *)
-
-lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
+(*only admissible in t, not if done in s*)
+lemma Forall_prefix: "\<forall>s. Forall P s \<longrightarrow> t \<sqsubseteq> s \<longrightarrow> Forall P t"
   apply (rule_tac x="t" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -578,12 +532,12 @@
 
 lemmas Forall_prefixclosed = Forall_prefix [rule_format]
 
-lemma Forall_postfixclosed: "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
+lemma Forall_postfixclosed: "Finite h \<Longrightarrow> Forall P s \<Longrightarrow> s= h @@ t \<Longrightarrow> Forall P t"
   by auto
 
 
 lemma ForallPFilterQR1:
-  "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
+  "(\<forall>x. P x \<longrightarrow> Q x = R x) \<and> Forall P tr \<longrightarrow> Filter Q $ tr = Filter R $ tr"
   apply (rule_tac x="tr" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -592,16 +546,13 @@
 lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
 
 
-(* ------------------------------------------------------------------------------------- *)
+subsection \<open>Forall, Filter\<close>
 
-subsection "Forall, Filter"
-
-
-lemma ForallPFilterP: "Forall P (Filter P$x)"
+lemma ForallPFilterP: "Forall P (Filter P $ x)"
   by (simp add: Filter_def Forall_def forallPsfilterP)
 
-(* holds also in other direction, then equal to forallPfilterP *)
-lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
+(*holds also in other direction, then equal to forallPfilterP*)
+lemma ForallPFilterPid1: "Forall P x \<longrightarrow> Filter P $ x = x"
   apply (rule_tac x="x" in Seq_induct)
   apply (simp add: Forall_def sforall_def Filter_def)
   apply simp_all
@@ -609,18 +560,15 @@
 
 lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
 
-
-(* holds also in other direction *)
-lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
-   Forall (%x. ~P x) ys --> Filter P$ys = nil "
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+(*holds also in other direction*)
+lemma ForallnPFilterPnil1: "Finite ys \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P $ ys = nil"
+  by (erule Seq_Finite_ind) simp_all
 
 lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
 
 
-(* holds also in other direction *)
-lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys --> Filter P$ys = UU"
+(*holds also in other direction*)
+lemma ForallnPFilterPUU1: "\<not> Finite ys \<and> Forall (\<lambda>x. \<not> P x) ys \<longrightarrow> Filter P $ ys = UU"
   apply (rule_tac x="ys" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -629,31 +577,27 @@
 lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
 
 
-(* inverse of ForallnPFilterPnil *)
-
-lemma FilternPnilForallP [rule_format]: "Filter P$ys = nil -->
-   (Forall (%x. ~P x) ys & Finite ys)"
+(*inverse of ForallnPFilterPnil*)
+lemma FilternPnilForallP [rule_format]: "Filter P $ ys = nil \<longrightarrow> Forall (\<lambda>x. \<not> P x) ys \<and> Finite ys"
   apply (rule_tac x="ys" in Seq_induct)
-  (* adm *)
+  text \<open>adm\<close>
   apply (simp add: Forall_def sforall_def)
-  (* base cases *)
+  text \<open>base cases\<close>
   apply simp
   apply simp
-  (* main case *)
+  text \<open>main case\<close>
   apply simp
   done
 
-
-(* inverse of ForallnPFilterPUU *)
-
+(*inverse of ForallnPFilterPUU*)
 lemma FilternPUUForallP:
-  assumes "Filter P$ys = UU"
-  shows "Forall (%x. ~P x) ys  & ~Finite ys"
+  assumes "Filter P $ ys = UU"
+  shows "Forall (\<lambda>x. \<not> P x) ys \<and> \<not> Finite ys"
 proof
-  show "Forall (%x. ~P x) ys"
+  show "Forall (\<lambda>x. \<not> P x) ys"
   proof (rule classical)
     assume "\<not> ?thesis"
-    then have "Filter P$ys ~= UU"
+    then have "Filter P $ ys \<noteq> UU"
       apply (rule rev_mp)
       apply (induct ys rule: Seq_induct)
       apply (simp add: Forall_def sforall_def)
@@ -661,10 +605,10 @@
       done
     with assms show ?thesis by contradiction
   qed
-  show "~ Finite ys"
+  show "\<not> Finite ys"
   proof
     assume "Finite ys"
-    then have "Filter P$ys ~= UU"
+    then have "Filter P$ys \<noteq> UU"
       by (rule Seq_Finite_ind) simp_all
     with assms show False by contradiction
   qed
@@ -672,33 +616,26 @@
 
 
 lemma ForallQFilterPnil:
-  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
-    ==> Filter P$ys = nil"
+  "Forall Q ys \<Longrightarrow> Finite ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ ys = nil"
   apply (erule ForallnPFilterPnil)
   apply (erule ForallPForallQ)
   apply auto
   done
 
-lemma ForallQFilterPUU:
- "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|]
-    ==> Filter P$ys = UU "
+lemma ForallQFilterPUU: "\<not> Finite ys \<Longrightarrow> Forall Q ys \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ ys = UU"
   apply (erule ForallnPFilterPUU)
   apply (erule ForallPForallQ)
   apply auto
   done
 
 
-
-(* ------------------------------------------------------------------------------------- *)
+subsection \<open>Takewhile, Forall, Filter\<close>
 
-subsection "Takewhile, Forall, Filter"
-
-
-lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
+lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P $ x)"
   by (simp add: Forall_def Takewhile_def sforallPstakewhileP)
 
 
-lemma ForallPTakewhileQ [simp]: "!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
+lemma ForallPTakewhileQ [simp]: "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Forall P (Takewhile Q $ x)"
   apply (rule ForallPForallQ)
   apply (rule ForallPTakewhileP)
   apply auto
@@ -706,8 +643,7 @@
 
 
 lemma FilterPTakewhileQnil [simp]:
-  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |]
-   ==> Filter P$(Takewhile Q$ys) = nil"
+  "Finite (Takewhile Q $ ys) \<Longrightarrow> (\<And>x. Q x \<Longrightarrow> \<not> P x) \<Longrightarrow> Filter P $ (Takewhile Q $ ys) = nil"
   apply (erule ForallnPFilterPnil)
   apply (rule ForallPForallQ)
   apply (rule ForallPTakewhileP)
@@ -715,8 +651,7 @@
   done
 
 lemma FilterPTakewhileQid [simp]:
- "!! Q P. [| !!x. Q x ==> P x |] ==>
-            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
+  "(\<And>x. Q x \<Longrightarrow> P x) \<Longrightarrow> Filter P $ (Takewhile Q $ ys) = Takewhile Q $ ys"
   apply (rule ForallPFilterPid)
   apply (rule ForallPForallQ)
   apply (rule ForallPTakewhileP)
@@ -724,26 +659,28 @@
   done
 
 
-lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
+lemma Takewhile_idempotent: "Takewhile P $ (Takewhile P $ s) = Takewhile P $ s"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
-lemma ForallPTakewhileQnP [simp]: "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
+lemma ForallPTakewhileQnP [simp]:
+  "Forall P s \<longrightarrow> Takewhile (\<lambda>x. Q x \<or> (\<not> P x)) $ s = Takewhile Q $ s"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
-lemma ForallPDropwhileQnP [simp]: "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
+lemma ForallPDropwhileQnP [simp]:
+  "Forall P s \<longrightarrow> Dropwhile (\<lambda>x. Q x \<or> (\<not> P x)) $ s = Dropwhile Q $ s"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
 
-lemma TakewhileConc1: "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
+lemma TakewhileConc1: "Forall P s \<longrightarrow> Takewhile P $ (s @@ t) = s @@ (Takewhile P $ t)"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
@@ -751,22 +688,18 @@
 
 lemmas TakewhileConc = TakewhileConc1 [THEN mp]
 
-lemma DropwhileConc1: "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+lemma DropwhileConc1: "Finite s \<Longrightarrow> Forall P s \<longrightarrow> Dropwhile P $ (s @@ t) = Dropwhile P $ t"
+  by (erule Seq_Finite_ind) simp_all
 
 lemmas DropwhileConc = DropwhileConc1 [THEN mp]
 
 
-
-(* ----------------------------------------------------------------------------------- *)
-
-subsection "coinductive characterizations of Filter"
+subsection \<open>Coinductive characterizations of Filter\<close>
 
 lemma divide_Seq_lemma:
- "HD$(Filter P$y) = Def x
-    --> y = ((Takewhile (%x. ~P x)$y) @@ (x \<leadsto> TL$(Dropwhile (%a. ~P a)$y)))
-             & Finite (Takewhile (%x. ~ P x)$y)  & P x"
+  "HD $ (Filter P $ y) = Def x \<longrightarrow>
+    y = (Takewhile (\<lambda>x. \<not> P x) $ y) @@ (x \<leadsto> TL $ (Dropwhile (\<lambda>a. \<not> P a) $ y)) \<and>
+    Finite (Takewhile (\<lambda>x. \<not> P x) $ y) \<and> P x"
   (* FIX: pay attention: is only admissible with chain-finite package to be added to
           adm test and Finite f x admissibility *)
   apply (rule_tac x="y" in Seq_induct)
@@ -776,20 +709,20 @@
   apply (case_tac "P a")
    apply simp
    apply blast
-  (* ~ P a *)
+  text \<open>\<open>\<not> P a\<close>\<close>
   apply simp
   done
 
-lemma divide_Seq: "(x\<leadsto>xs) << Filter P$y
-   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x \<leadsto> TL$(Dropwhile (%a. ~ P a)$y)))
-      & Finite (Takewhile (%a. ~ P a)$y)  & P x"
+lemma divide_Seq: "(x \<leadsto> xs) \<sqsubseteq> Filter P $ y \<Longrightarrow>
+  y = ((Takewhile (\<lambda>a. \<not> P a) $ y) @@ (x \<leadsto> TL $ (Dropwhile (\<lambda>a. \<not> P a) $ y))) \<and>
+  Finite (Takewhile (\<lambda>a. \<not> P a) $ y) \<and> P x"
   apply (rule divide_Seq_lemma [THEN mp])
-  apply (drule_tac f="HD" and x="x\<leadsto>xs" in  monofun_cfun_arg)
+  apply (drule_tac f="HD" and x="x \<leadsto> xs" in  monofun_cfun_arg)
   apply simp
   done
 
 
-lemma nForall_HDFilter: "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
+lemma nForall_HDFilter: "\<not> Forall P y \<longrightarrow> (\<exists>x. HD $ (Filter (\<lambda>a. \<not> P a) $ y) = Def x)"
   unfolding not_Undef_is_Def [symmetric]
   apply (induct y rule: Seq_induct)
   apply (simp add: Forall_def sforall_def)
@@ -797,19 +730,19 @@
   done
 
 
-lemma divide_Seq2: "~Forall P y
-  ==> ? x. y= (Takewhile P$y @@ (x \<leadsto> TL$(Dropwhile P$y))) &
-      Finite (Takewhile P$y) & (~ P x)"
+lemma divide_Seq2:
+  "\<not> Forall P y \<Longrightarrow>
+    \<exists>x. y = Takewhile P$y @@ (x \<leadsto> TL $ (Dropwhile P $ y)) \<and> Finite (Takewhile P $ y) \<and> \<not> P x"
   apply (drule nForall_HDFilter [THEN mp])
   apply safe
   apply (rule_tac x="x" in exI)
-  apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
+  apply (cut_tac P1="\<lambda>x. \<not> P x" in divide_Seq_lemma [THEN mp])
   apply auto
   done
 
 
-lemma divide_Seq3: "~Forall P y
-  ==> ? x bs rs. y= (bs @@ (x\<leadsto>rs)) & Finite bs & Forall P bs & (~ P x)"
+lemma divide_Seq3:
+  "\<not> Forall P y \<Longrightarrow> \<exists>x bs rs. y = (bs @@ (x\<leadsto>rs)) \<and> Finite bs \<and> Forall P bs \<and> \<not> P x"
   apply (drule divide_Seq2)
   apply fastforce
   done
@@ -817,20 +750,17 @@
 lemmas [simp] = FilterPQ FilterConc Conc_cong
 
 
-(* ------------------------------------------------------------------------------------- *)
-
+subsection \<open>Take-lemma\<close>
 
-subsection "take_lemma"
-
-lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
+lemma seq_take_lemma: "(\<forall>n. seq_take n $ x = seq_take n $ x') \<longleftrightarrow> x = x'"
   apply (rule iffI)
   apply (rule seq.take_lemma)
   apply auto
   done
 
 lemma take_reduction1:
-  "\<forall>n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
-    --> seq_take n$(x @@ (t\<leadsto>y1)) =  seq_take n$(x @@ (t\<leadsto>y2)))"
+  "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k $ y1 = seq_take k $ y2) \<longrightarrow>
+    seq_take n $ (x @@ (t \<leadsto> y1)) =  seq_take n $ (x @@ (t \<leadsto> y2)))"
   apply (rule_tac x="x" in Seq_induct)
   apply simp_all
   apply (intro strip)
@@ -840,19 +770,19 @@
   apply auto
   done
 
-
 lemma take_reduction:
-  "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
-    ==> seq_take n$(x @@ (s\<leadsto>y1)) =  seq_take n$(y @@ (t\<leadsto>y2))"
+  "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k $ y1 = seq_take k $ y2)
+    \<Longrightarrow> seq_take n $ (x @@ (s \<leadsto> y1)) = seq_take n $ (y @@ (t \<leadsto> y2))"
   by (auto intro!: take_reduction1 [rule_format])
 
-(* ------------------------------------------------------------------
-          take-lemma and take_reduction for << instead of =
-   ------------------------------------------------------------------ *)
 
+text \<open>
+  Take-lemma and take-reduction for \<open>\<sqsubseteq>\<close> instead of \<open>=\<close>.
+\<close>
+          
 lemma take_reduction_less1:
-  "\<forall>n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
-    --> seq_take n$(x @@ (t\<leadsto>y1)) <<  seq_take n$(x @@ (t\<leadsto>y2)))"
+  "\<forall>n. ((\<forall>k. k < n \<longrightarrow> seq_take k $ y1 \<sqsubseteq> seq_take k$y2) \<longrightarrow>
+    seq_take n $ (x @@ (t \<leadsto> y1)) \<sqsubseteq> seq_take n $ (x @@ (t \<leadsto> y2)))"
   apply (rule_tac x="x" in Seq_induct)
   apply simp_all
   apply (intro strip)
@@ -862,15 +792,14 @@
   apply auto
   done
 
-
 lemma take_reduction_less:
-  "\<And>n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
-    ==> seq_take n$(x @@ (s\<leadsto>y1)) <<  seq_take n$(y @@ (t\<leadsto>y2))"
+  "x = y \<Longrightarrow> s = t \<Longrightarrow> (\<And>k. k < n \<Longrightarrow> seq_take k $ y1 \<sqsubseteq> seq_take k $ y2) \<Longrightarrow>
+    seq_take n $ (x @@ (s \<leadsto> y1)) \<sqsubseteq> seq_take n $ (y @@ (t \<leadsto> y2))"
   by (auto intro!: take_reduction_less1 [rule_format])
 
 lemma take_lemma_less1:
-  assumes "!! n. seq_take n$s1 << seq_take n$s2"
-  shows "s1<<s2"
+  assumes "\<And>n. seq_take n $ s1 \<sqsubseteq> seq_take n $ s2"
+  shows "s1 \<sqsubseteq> s2"
   apply (rule_tac t="s1" in seq.reach [THEN subst])
   apply (rule_tac t="s2" in seq.reach [THEN subst])
   apply (rule lub_mono)
@@ -879,55 +808,56 @@
   apply (rule assms)
   done
 
-
-lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
+lemma take_lemma_less: "(\<forall>n. seq_take n $ x \<sqsubseteq> seq_take n $ x') \<longleftrightarrow> x \<sqsubseteq> x'"
   apply (rule iffI)
   apply (rule take_lemma_less1)
   apply auto
   apply (erule monofun_cfun_arg)
   done
 
-(* ------------------------------------------------------------------
-          take-lemma proof principles
-   ------------------------------------------------------------------ *)
+
+text \<open>Take-lemma proof principles.\<close>
 
 lemma take_lemma_principle1:
-  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
-            !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\<leadsto>s2)|]
-                          ==> (f (s1 @@ y\<leadsto>s2)) = (g (s1 @@ y\<leadsto>s2)) |]
-               ==> A x --> (f x)=(g x)"
-  apply (case_tac "Forall Q x")
-  apply (auto dest!: divide_Seq3)
-  done
+  assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
+    and "\<And>s1 s2 y. Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow>
+      \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow> f (s1 @@ y \<leadsto> s2) = g (s1 @@ y \<leadsto> s2)"
+  shows "A x \<longrightarrow> f x = g x"
+  using assms by (cases "Forall Q x") (auto dest!: divide_Seq3)
 
 lemma take_lemma_principle2:
-  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
-           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\<leadsto>s2)|]
-                          ==> ! n. seq_take n$(f (s1 @@ y\<leadsto>s2))
-                                 = seq_take n$(g (s1 @@ y\<leadsto>s2)) |]
-               ==> A x --> (f x)=(g x)"
-  apply (case_tac "Forall Q x")
+  assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
+    and "\<And>s1 s2 y. Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
+      \<forall>n. seq_take n $ (f (s1 @@ y \<leadsto> s2)) = seq_take n $ (g (s1 @@ y \<leadsto> s2))"
+  shows "A x \<longrightarrow> f x = g x"
+  using assms
+  apply (cases "Forall Q x")
   apply (auto dest!: divide_Seq3)
   apply (rule seq.take_lemma)
   apply auto
   done
 
 
-(* Note: in the following proofs the ordering of proof steps is very
-         important, as otherwise either (Forall Q s1) would be in the IH as
-         assumption (then rule useless) or it is not possible to strengthen
-         the IH apply doing a forall closure of the sequence t (then rule also useless).
-         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
-         to be imbuilt into the rule, as induction has to be done early and the take lemma
-         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
+text \<open>
+  Note: in the following proofs the ordering of proof steps is very important,
+  as otherwise either \<open>Forall Q s1\<close> would be in the IH as assumption (then
+  rule useless) or it is not possible to strengthen the IH apply doing a
+  forall closure of the sequence \<open>t\<close> (then rule also useless). This is also
+  the reason why the induction rule (\<open>nat_less_induct\<close> or \<open>nat_induct\<close>) has to
+  to be imbuilt into the rule, as induction has to be done early and the take
+  lemma has to be used in the trivial direction afterwards for the
+  \<open>Forall Q x\<close> case.
+\<close>
 
 lemma take_lemma_induct:
-"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
-         !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
-                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\<leadsto>s2) |]
-                          ==>   seq_take (Suc n)$(f (s1 @@ y\<leadsto>s2))
-                              = seq_take (Suc n)$(g (s1 @@ y\<leadsto>s2)) |]
-               ==> A x --> (f x)=(g x)"
+  assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
+    and "\<And>s1 s2 y n.
+      \<forall>t. A t \<longrightarrow> seq_take n $ (f t) = seq_take n $ (g t) \<Longrightarrow>
+      Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
+      seq_take (Suc n) $ (f (s1 @@ y \<leadsto> s2)) =
+      seq_take (Suc n) $ (g (s1 @@ y \<leadsto> s2))"
+  shows "A x \<longrightarrow> f x = g x"
+  apply (insert assms)
   apply (rule impI)
   apply (rule seq.take_lemma)
   apply (rule mp)
@@ -943,12 +873,14 @@
 
 
 lemma take_lemma_less_induct:
-"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
-        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);
-                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\<leadsto>s2) |]
-                          ==>   seq_take n$(f (s1 @@ y\<leadsto>s2))
-                              = seq_take n$(g (s1 @@ y\<leadsto>s2)) |]
-               ==> A x --> (f x)=(g x)"
+  assumes "\<And>s. Forall Q s \<Longrightarrow> A s \<Longrightarrow> f s = g s"
+    and "\<And>s1 s2 y n.
+      \<forall>t m. m < n \<longrightarrow> A t \<longrightarrow> seq_take m $ (f t) = seq_take m $ (g t) \<Longrightarrow>
+      Forall Q s1 \<Longrightarrow> Finite s1 \<Longrightarrow> \<not> Q y \<Longrightarrow> A (s1 @@ y \<leadsto> s2) \<Longrightarrow>
+      seq_take n $ (f (s1 @@ y \<leadsto> s2)) =
+      seq_take n $ (g (s1 @@ y \<leadsto> s2))"
+  shows "A x \<longrightarrow> f x = g x"
+  apply (insert assms)
   apply (rule impI)
   apply (rule seq.take_lemma)
   apply (rule mp)
@@ -964,13 +896,14 @@
 
 
 lemma take_lemma_in_eq_out:
-"!! Q. [| A UU  ==> (f UU) = (g UU) ;
-          A nil ==> (f nil) = (g nil) ;
-          !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
-                     A (y\<leadsto>s) |]
-                     ==>   seq_take (Suc n)$(f (y\<leadsto>s))
-                         = seq_take (Suc n)$(g (y\<leadsto>s)) |]
-               ==> A x --> (f x)=(g x)"
+  assumes "A UU \<Longrightarrow> f UU = g UU"
+    and "A nil \<Longrightarrow> f nil = g nil"
+    and "\<And>s y n.
+      \<forall>t. A t \<longrightarrow> seq_take n $ (f t) = seq_take n $ (g t) \<Longrightarrow> A (y \<leadsto> s) \<Longrightarrow>
+      seq_take (Suc n) $ (f (y \<leadsto> s)) =
+      seq_take (Suc n) $ (g (y \<leadsto> s))"
+  shows "A x \<longrightarrow> f x = g x"
+  apply (insert assms)
   apply (rule impI)
   apply (rule seq.take_lemma)
   apply (rule mp)
@@ -984,47 +917,35 @@
   done
 
 
-(* ------------------------------------------------------------------------------------ *)
-
-subsection "alternative take_lemma proofs"
+subsection \<open>Alternative take_lemma proofs\<close>
 
-
-(* --------------------------------------------------------------- *)
-(*              Alternative Proof of FilterPQ                      *)
-(* --------------------------------------------------------------- *)
+subsubsection \<open>Alternative Proof of FilterPQ\<close>
 
 declare FilterPQ [simp del]
 
 
-(* In general: How to do this case without the same adm problems
-   as for the entire proof ? *)
-lemma Filter_lemma1: "Forall (%x. ~(P x & Q x)) s
-          --> Filter P$(Filter Q$s) =
-              Filter (%x. P x & Q x)$s"
-
+(*In general: How to do this case without the same adm problems
+  as for the entire proof?*)
+lemma Filter_lemma1:
+  "Forall (\<lambda>x. \<not> (P x \<and> Q x)) s \<longrightarrow>
+    Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
   apply (rule_tac x="s" in Seq_induct)
   apply (simp add: Forall_def sforall_def)
   apply simp_all
   done
 
-lemma Filter_lemma2: "Finite s ==>
-          (Forall (%x. (~P x) | (~ Q x)) s
-          --> Filter P$(Filter Q$s) = nil)"
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+lemma Filter_lemma2: "Finite s \<Longrightarrow>
+  Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter P $ (Filter Q $ s) = nil"
+  by (erule Seq_Finite_ind) simp_all
 
-lemma Filter_lemma3: "Finite s ==>
-          Forall (%x. (~P x) | (~ Q x)) s
-          --> Filter (%x. P x & Q x)$s = nil"
-  apply (erule Seq_Finite_ind, simp_all)
-  done
+lemma Filter_lemma3: "Finite s \<Longrightarrow>
+  Forall (\<lambda>x. \<not> P x \<or> \<not> Q x) s \<longrightarrow> Filter (\<lambda>x. P x \<and> Q x) $ s = nil"
+  by (erule Seq_Finite_ind) simp_all
 
-
-lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
-  apply (rule_tac A1="%x. True" and
-                   Q1="%x. ~(P x & Q x)" and x1="s" in
-                   take_lemma_induct [THEN mp])
-  (* better support for A = %x. True *)
+lemma FilterPQ_takelemma: "Filter P $ (Filter Q $ s) = Filter (\<lambda>x. P x \<and> Q x) $ s"
+  apply (rule_tac A1="\<lambda>x. True" and Q1="\<lambda>x. \<not> (P x \<and> Q x)" and x1="s" in
+    take_lemma_induct [THEN mp])
+  (*better support for A = \<lambda>x. True*)
   apply (simp add: Filter_lemma1)
   apply (simp add: Filter_lemma2 Filter_lemma3)
   apply simp
@@ -1033,36 +954,29 @@
 declare FilterPQ [simp]
 
 
-(* --------------------------------------------------------------- *)
-(*              Alternative Proof of MapConc                       *)
-(* --------------------------------------------------------------- *)
-
+subsubsection \<open>Alternative Proof of \<open>MapConc\<close>\<close>
 
-
-lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
-  apply (rule_tac A1="%x. True" and x1="x" in
-      take_lemma_in_eq_out [THEN mp])
+lemma MapConc_takelemma: "Map f $ (x @@ y) = (Map f $ x) @@ (Map f $ y)"
+  apply (rule_tac A1="\<lambda>x. True" and x1="x" in take_lemma_in_eq_out [THEN mp])
   apply auto
   done
 
-
 ML \<open>
-
 fun Seq_case_tac ctxt s i =
   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
-  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
+  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i + 1) THEN hyp_subst_tac ctxt (i + 2);
 
 (* on a\<leadsto>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
 fun Seq_case_simp_tac ctxt s i =
   Seq_case_tac ctxt s i
-  THEN asm_simp_tac ctxt (i+2)
-  THEN asm_full_simp_tac ctxt (i+1)
+  THEN asm_simp_tac ctxt (i + 2)
+  THEN asm_full_simp_tac ctxt (i + 1)
   THEN asm_full_simp_tac ctxt i;
 
 (* rws are definitions to be unfolded for admissibility check *)
 fun Seq_induct_tac ctxt s rws i =
   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
-  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1))))
+  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i + 1))))
   THEN simp_tac (ctxt addsimps rws) i;
 
 fun Seq_Finite_induct_tac ctxt i =
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -153,7 +153,7 @@
 done
 
 
-lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
+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)
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -42,138 +42,109 @@
 
 
 lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"
-apply (rule ext)
-apply (simp add: Diamond_def NOT_def Box_def)
-done
+  by (auto simp add: Diamond_def NOT_def Box_def)
 
 lemma Boxnil: "nil \<Turnstile> \<box>P"
-apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
-done
+  by (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
 
-lemma Diamondnil: "~(nil \<Turnstile> \<diamond>P)"
-apply (simp add: Diamond_def satisfies_def NOT_def)
-apply (cut_tac Boxnil)
-apply (simp add: satisfies_def)
-done
+lemma Diamondnil: "\<not> (nil \<Turnstile> \<diamond>P)"
+  using Boxnil by (simp add: Diamond_def satisfies_def NOT_def)
 
-lemma Diamond_def2: "(\<diamond>F) s = (? s2. tsuffix s2 s & F s2)"
-apply (simp add: Diamond_def NOT_def Box_def)
-done
-
+lemma Diamond_def2: "(\<diamond>F) s \<longleftrightarrow> (\<exists>s2. tsuffix s2 s \<and> F s2)"
+  by (simp add: Diamond_def NOT_def Box_def)
 
 
-subsection "TLA Axiomatization by Merz"
+subsection \<open>TLA Axiomatization by Merz\<close>
 
 lemma suffix_refl: "suffix s s"
-apply (simp add: suffix_def)
-apply (rule_tac x = "nil" in exI)
-apply auto
-done
+  apply (simp add: suffix_def)
+  apply (rule_tac x = "nil" in exI)
+  apply auto
+  done
 
-lemma reflT: "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
-apply (simp add: satisfies_def IMPLIES_def Box_def)
-apply (rule impI)+
-apply (erule_tac x = "s" in allE)
-apply (simp add: tsuffix_def suffix_refl)
-done
-
+lemma reflT: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
+  apply (simp add: satisfies_def IMPLIES_def Box_def)
+  apply (rule impI)+
+  apply (erule_tac x = "s" in allE)
+  apply (simp add: tsuffix_def suffix_refl)
+  done
 
-lemma suffix_trans: "[| suffix y x ; suffix z y |]  ==> suffix z x"
-apply (simp add: suffix_def)
-apply auto
-apply (rule_tac x = "s1 @@ s1a" in exI)
-apply auto
-apply (simp (no_asm) add: Conc_assoc)
-done
+lemma suffix_trans: "suffix y x \<Longrightarrow> suffix z y \<Longrightarrow> suffix z x"
+  apply (simp add: suffix_def)
+  apply auto
+  apply (rule_tac x = "s1 @@ s1a" in exI)
+  apply auto
+  apply (simp add: Conc_assoc)
+  done
 
 lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"
-apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)
-apply auto
-apply (drule suffix_trans)
-apply assumption
-apply (erule_tac x = "s2a" in allE)
-apply auto
-done
-
+  apply (simp add: satisfies_def IMPLIES_def Box_def tsuffix_def)
+  apply auto
+  apply (drule suffix_trans)
+  apply assumption
+  apply (erule_tac x = "s2a" in allE)
+  apply auto
+  done
 
 lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"
-apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)
-done
+  by (simp add: satisfies_def IMPLIES_def Box_def)
 
 
-subsection "TLA Rules by Lamport"
+subsection \<open>TLA Rules by Lamport\<close>
 
-lemma STL1a: "validT P ==> validT (\<box>P)"
-apply (simp add: validT_def satisfies_def Box_def tsuffix_def)
-done
+lemma STL1a: "validT P \<Longrightarrow> validT (\<box>P)"
+  by (simp add: validT_def satisfies_def Box_def tsuffix_def)
 
-lemma STL1b: "valid P ==> validT (Init P)"
-apply (simp add: valid_def validT_def satisfies_def Init_def)
-done
+lemma STL1b: "valid P \<Longrightarrow> validT (Init P)"
+  by (simp add: valid_def validT_def satisfies_def Init_def)
 
-lemma STL1: "valid P ==> validT (\<box>(Init P))"
-apply (rule STL1a)
-apply (erule STL1b)
-done
+lemma STL1: "valid P \<Longrightarrow> validT (\<box>(Init P))"
+  apply (rule STL1a)
+  apply (erule STL1b)
+  done
 
-(* Note that unlift and HD is not at all used !!! *)
-lemma STL4: "valid (P \<^bold>\<longrightarrow> Q)  ==> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
-apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
-done
+(*Note that unlift and HD is not at all used!*)
+lemma STL4: "valid (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
+  by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
 
 
-subsection "LTL Axioms by Manna/Pnueli"
+subsection \<open>LTL Axioms by Manna/Pnueli\<close>
 
-lemma tsuffix_TL [rule_format (no_asm)]:
-"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
-apply (unfold tsuffix_def suffix_def)
-apply auto
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (rule_tac x = "a\<leadsto>s1" in exI)
-apply auto
-done
+lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL $ s) \<longrightarrow> tsuffix s2 s"
+  apply (unfold tsuffix_def suffix_def)
+  apply auto
+  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  apply (rule_tac x = "a \<leadsto> s1" in exI)
+  apply auto
+  done
 
 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
 
-declare split_if [split del]
-lemma LTL1:
-   "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
-apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
-apply auto
-(* \<box>F \<^bold>\<longrightarrow> F *)
-apply (erule_tac x = "s" in allE)
-apply (simp add: tsuffix_def suffix_refl)
-(* \<box>F \<^bold>\<longrightarrow> Next \<box>F *)
-apply (simp split add: split_if)
-apply auto
-apply (drule tsuffix_TL2)
-apply assumption+
-apply auto
-done
-declare split_if [split]
-
+lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
+  supply split_if [split del] 
+  apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
+  apply auto
+  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close>
+  apply (erule_tac x = "s" in allE)
+  apply (simp add: tsuffix_def suffix_refl)
+  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> Next \<box>F\<close>\<close>
+  apply (simp split add: split_if)
+  apply auto
+  apply (drule tsuffix_TL2)
+  apply assumption+
+  apply auto
+  done
 
-lemma LTL2a:
-    "s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
-apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
-apply simp
-done
+lemma LTL2a: "s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
+  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
+
+lemma LTL2b: "s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"
+  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
 
-lemma LTL2b:
-    "s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"
-apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
-apply simp
-done
+lemma LTL3: "ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
+  by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
 
-lemma LTL3:
-"ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
-apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
-apply simp
-done
-
-
-lemma ModusPonens: "[| validT (P \<^bold>\<longrightarrow> Q); validT P |] ==> validT Q"
-apply (simp add: validT_def satisfies_def IMPLIES_def)
-done
+lemma ModusPonens: "validT (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> validT P \<Longrightarrow> validT Q"
+  by (simp add: validT_def satisfies_def IMPLIES_def)
 
 end
diff -r 57895801cb57 -r bc178c0fe1a1 src/HOL/HOLCF/IOA/Traces.thy
--- a/src/HOL/HOLCF/IOA/Traces.thy	Sun Jan 10 23:25:11 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Traces.thy	Mon Jan 11 00:04:23 2016 +0100
@@ -10,48 +10,48 @@
 
 default_sort type
 
-type_synonym ('a, 's) pairs = "('a * 's) Seq"
-type_synonym ('a, 's) execution = "'s * ('a, 's) pairs"
+type_synonym ('a, 's) pairs = "('a \<times> 's) Seq"
+type_synonym ('a, 's) execution = "'s \<times> ('a, 's) pairs"
 type_synonym 'a trace = "'a Seq"
-type_synonym ('a, 's) execution_module = "('a, 's) execution set * 'a signature"
-type_synonym 'a schedule_module = "'a trace set * 'a signature"
-type_synonym 'a trace_module = "'a trace set * 'a signature"
+type_synonym ('a, 's) execution_module = "('a, 's) execution set \<times> 'a signature"
+type_synonym 'a schedule_module = "'a trace set \<times> 'a signature"
+type_synonym 'a trace_module = "'a trace set \<times> 'a signature"
 
 
-(*  ------------------- Executions ------------------------------ *)
+subsection \<open>Executions\<close>
 
 definition is_exec_fragC :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 's \<Rightarrow> tr"
-where
-  "is_exec_fragC A = (fix $ (LAM h ex. (%s. case ex of
-      nil => TT
-    | x##xs => (flift1
-            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p))
-             $x)
-   )))"
+  where "is_exec_fragC A =
+    (fix $
+      (LAM h ex.
+        (\<lambda>s.
+          case ex of
+            nil \<Rightarrow> TT
+          | x ## xs \<Rightarrow> flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (h $ xs) (snd p)) $ x)))"
 
-definition is_exec_frag :: "[('a,'s)ioa, ('a,'s)execution] \<Rightarrow> bool"
-  where "is_exec_frag A ex = ((is_exec_fragC A $ (snd ex)) (fst ex) ~= FF)"
+definition is_exec_frag :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+  where "is_exec_frag A ex \<longleftrightarrow> (is_exec_fragC A $ (snd ex)) (fst ex) \<noteq> FF"
 
 definition executions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set"
-  where "executions ioa = {e. ((fst e) \<in> starts_of(ioa)) \<and> is_exec_frag ioa e}"
+  where "executions ioa = {e. fst e \<in> starts_of ioa \<and> is_exec_frag ioa e}"
 
 
-(*  ------------------- Schedules ------------------------------ *)
+subsection \<open>Schedules\<close>
 
 definition filter_act :: "('a, 's) pairs \<rightarrow> 'a trace"
   where "filter_act = Map fst"
 
-definition has_schedule :: "[('a, 's) ioa, 'a trace] \<Rightarrow> bool"
+definition has_schedule :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool"
   where "has_schedule ioa sch \<longleftrightarrow> (\<exists>ex \<in> executions ioa. sch = filter_act $ (snd ex))"
 
 definition schedules :: "('a, 's) ioa \<Rightarrow> 'a trace set"
   where "schedules ioa = {sch. has_schedule ioa sch}"
 
 
-(*  ------------------- Traces ------------------------------ *)
+subsection \<open>Traces\<close>
 
-definition has_trace :: "[('a, 's) ioa, 'a trace] \<Rightarrow> bool"
-  where "has_trace ioa tr = (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) $ sch)"
+definition has_trace :: "('a, 's) ioa \<Rightarrow> 'a trace \<Rightarrow> bool"
+  where "has_trace ioa tr \<longleftrightarrow> (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) $ sch)"
 
 definition traces :: "('a, 's) ioa \<Rightarrow> 'a trace set"
   where "traces ioa \<equiv> {tr. has_trace ioa tr}"
@@ -60,57 +60,63 @@
   where "mk_trace ioa = (LAM tr. Filter (\<lambda>a. a \<in> ext ioa) $ (filter_act $ tr))"
 
 
-(*  ------------------- Fair Traces ------------------------------ *)
+subsection \<open>Fair Traces\<close>
 
 definition laststate :: "('a, 's) execution \<Rightarrow> 's"
-where
-  "laststate ex = (case Last $ (snd ex) of
-                    UU  => fst ex
-                  | Def at => snd at)"
+  where "laststate ex =
+    (case Last $ (snd ex) of
+      UU \<Rightarrow> fst ex
+    | Def at \<Rightarrow> snd at)"
 
-(* A predicate holds infinitely (finitely) often in a sequence *)
-
+text \<open>A predicate holds infinitely (finitely) often in a sequence.\<close>
 definition inf_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
   where "inf_often P s \<longleftrightarrow> Infinite (Filter P $ s)"
 
-(*  filtering P yields a finite or partial sequence *)
+text \<open>Filtering \<open>P\<close> yields a finite or partial sequence.\<close>
 definition fin_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
   where "fin_often P s \<longleftrightarrow> \<not> inf_often P s"
 
 
-(* fairness of executions *)
+subsection \<open>Fairness of executions\<close>
 
-(* Note that partial execs cannot be wfair as the inf_often predicate in the
-   else branch prohibits it. However they can be sfair in the case when all W
-   are only finitely often enabled: Is this the right model?
-   See LiveIOA for solution conforming with the literature and superseding this one *)
+text \<open>
+  Note that partial execs cannot be \<open>wfair\<close> as the inf_often predicate in the
+  else branch prohibits it. However they can be \<open>sfair\<close> in the case when all
+  \<open>W\<close> are only finitely often enabled: Is this the right model?
+
+  See @{file "LiveIOA.thy"} for solution conforming with the literature and
+  superseding this one.
+\<close>
+
 definition is_wfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
-where
-  "is_wfair A W ex \<longleftrightarrow>
-    (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or> inf_often (\<lambda>x. \<not> Enabled A W (snd x)) (snd ex))"
+  where "is_wfair A W ex \<longleftrightarrow>
+    (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or>
+      inf_often (\<lambda>x. \<not> Enabled A W (snd x)) (snd ex))"
+
 definition wfair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
-where
-  "wfair_ex A ex \<longleftrightarrow> (\<forall>W \<in> wfair_of A.
-                      if Finite (snd ex)
-                      then \<not> Enabled A W (laststate ex)
-                      else is_wfair A W ex)"
+  where "wfair_ex A ex \<longleftrightarrow>
+    (\<forall>W \<in> wfair_of A.
+      if Finite (snd ex)
+      then \<not> Enabled A W (laststate ex)
+      else is_wfair A W ex)"
 
 definition is_sfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
-where
-  "is_sfair A W ex \<longleftrightarrow>
-    (inf_often (\<lambda>x. fst x:W) (snd ex) \<or> fin_often (\<lambda>x. Enabled A W (snd x)) (snd ex))"
+  where "is_sfair A W ex \<longleftrightarrow>
+    (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or>
+      fin_often (\<lambda>x. Enabled A W (snd x)) (snd ex))"
+
 definition sfair_ex :: "('a, 's)ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
-where
-  "sfair_ex A ex \<longleftrightarrow> (\<forall>W \<in> sfair_of A.
-                      if   Finite (snd ex)
-                      then ~Enabled A W (laststate ex)
-                      else is_sfair A W ex)"
+  where "sfair_ex A ex \<longleftrightarrow>
+    (\<forall>W \<in> sfair_of A.
+      if Finite (snd ex)
+      then \<not> Enabled A W (laststate ex)
+      else is_sfair A W ex)"
 
 definition fair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
   where "fair_ex A ex \<longleftrightarrow> wfair_ex A ex \<and> sfair_ex A ex"
 
 
-(* fair behavior sets *)
+text \<open>Fair behavior sets.\<close>
 
 definition fairexecutions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set"
   where "fairexecutions A = {ex. ex \<in> executions A \<and> fair_ex A ex}"
@@ -119,25 +125,24 @@
   where "fairtraces A = {mk_trace A $ (snd ex) | ex. ex \<in> fairexecutions A}"
 
 
-(*  ------------------- Implementation ------------------------------ *)
+subsection \<open>Implementation\<close>
 
-(* Notions of implementation *)
+subsubsection \<open>Notions of implementation\<close>
 
-definition ioa_implements :: "[('a, 's1) ioa, ('a, 's2) ioa] \<Rightarrow> bool"  (infixr "=<|" 12)
-where
-  "(ioa1 =<| ioa2) \<longleftrightarrow>
-    (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) \<and>
-     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) \<and>
-      traces(ioa1) \<subseteq> traces(ioa2))"
+definition ioa_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"  (infixr "=<|" 12)
+  where "(ioa1 =<| ioa2) \<longleftrightarrow>
+    (inputs (asig_of ioa1) = inputs (asig_of ioa2) \<and>
+     outputs (asig_of ioa1) = outputs (asig_of ioa2)) \<and>
+    traces ioa1 \<subseteq> traces ioa2"
 
 definition fair_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
-where
-  "fair_implements C A \<longleftrightarrow> inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A"
+  where "fair_implements C A \<longleftrightarrow>
+    inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A"
 
 
-(*  ------------------- Modules ------------------------------ *)
+subsection \<open>Modules\<close>
 
-(* Execution, schedule and trace modules *)
+subsubsection \<open>Execution, schedule and trace modules\<close>
 
 definition Execs :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution_module"
   where "Execs A = (executions A, asig_of A)"
@@ -148,7 +153,6 @@
 definition Traces :: "('a, 's) ioa \<Rightarrow> 'a trace_module"
   where "Traces A = (traces A, asig_of A)"
 
-
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
 declare Let_def [simp]
 setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
@@ -156,56 +160,50 @@
 lemmas exec_rws = executions_def is_exec_frag_def
 
 
-
-subsection "recursive equations of operators"
+subsection \<open>Recursive equations of operators\<close>
 
-(* ---------------------------------------------------------------- *)
-(*                               filter_act                         *)
-(* ---------------------------------------------------------------- *)
+subsubsection \<open>\<open>filter_act\<close>\<close>
 
-
-lemma filter_act_UU: "filter_act$UU = UU"
+lemma filter_act_UU: "filter_act $ UU = UU"
   by (simp add: filter_act_def)
 
-lemma filter_act_nil: "filter_act$nil = nil"
+lemma filter_act_nil: "filter_act $ nil = nil"
   by (simp add: filter_act_def)
 
-lemma filter_act_cons: "filter_act$(x\<leadsto>xs) = (fst x) \<leadsto> filter_act$xs"
+lemma filter_act_cons: "filter_act $ (x \<leadsto> xs) = fst x \<leadsto> filter_act $ xs"
   by (simp add: filter_act_def)
 
 declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
 
 
-(* ---------------------------------------------------------------- *)
-(*                             mk_trace                             *)
-(* ---------------------------------------------------------------- *)
+subsubsection \<open>\<open>mk_trace\<close>\<close>
 
-lemma mk_trace_UU: "mk_trace A$UU=UU"
+lemma mk_trace_UU: "mk_trace A $ UU = UU"
   by (simp add: mk_trace_def)
 
-lemma mk_trace_nil: "mk_trace A$nil=nil"
+lemma mk_trace_nil: "mk_trace A $ nil = nil"
   by (simp add: mk_trace_def)
 
-lemma mk_trace_cons: "mk_trace A$(at \<leadsto> xs) =
-             (if ((fst at):ext A)
-                  then (fst at) \<leadsto> (mk_trace A$xs)
-                  else mk_trace A$xs)"
-
+lemma mk_trace_cons:
+  "mk_trace A $ (at \<leadsto> xs) =
+    (if fst at \<in> ext A
+     then fst at \<leadsto> mk_trace A $ xs
+     else mk_trace A $ xs)"
   by (simp add: mk_trace_def)
 
 declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
 
-(* ---------------------------------------------------------------- *)
-(*                             is_exec_fragC                             *)
-(* ---------------------------------------------------------------- *)
 
+subsubsection \<open>\<open>is_exec_fragC\<close>\<close>
 
-lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of
-       nil => TT
-     | x##xs => (flift1
-             (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p))
-              $x)
-    ))"
+lemma is_exec_fragC_unfold:
+  "is_exec_fragC A =
+    (LAM ex.
+      (\<lambda>s.
+        case ex of
+          nil \<Rightarrow> TT
+        | x ## xs \<Rightarrow>
+            (flift1 (\<lambda>p. Def ((s, p) \<in> trans_of A) andalso (is_exec_fragC A$xs) (snd p)) $ x)))"
   apply (rule trans)
   apply (rule fix_eq4)
   apply (rule is_exec_fragC_def)
@@ -213,32 +211,29 @@
   apply (simp add: flift1_def)
   done
 
-lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU"
+lemma is_exec_fragC_UU: "(is_exec_fragC A $ UU) s = UU"
   apply (subst is_exec_fragC_unfold)
   apply simp
   done
 
-lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT"
+lemma is_exec_fragC_nil: "(is_exec_fragC A $ nil) s = TT"
   apply (subst is_exec_fragC_unfold)
   apply simp
   done
 
-lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr\<leadsto>xs)) s =
-                         (Def ((s,pr):trans_of A)
-                 andalso (is_exec_fragC A$xs)(snd pr))"
+lemma is_exec_fragC_cons:
+  "(is_exec_fragC A $ (pr \<leadsto> xs)) s =
+    (Def ((s, pr) \<in> trans_of A) andalso (is_exec_fragC A $ xs) (snd pr))"
   apply (rule trans)
   apply (subst is_exec_fragC_unfold)
   apply (simp add: Consq_def flift1_def)
   apply simp
   done
 
-
 declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]
 
 
-(* ---------------------------------------------------------------- *)
-(*                        is_exec_frag                              *)
-(* ---------------------------------------------------------------- *)
+subsubsection \<open>\<open>is_exec_frag\<close>\<close>
 
 lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"
   by (simp add: is_exec_frag_def)
@@ -246,30 +241,26 @@
 lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"
   by (simp add: is_exec_frag_def)
 
-lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\<leadsto>ex) =
-                                (((s,a,t):trans_of A) &
-                                is_exec_frag A (t, ex))"
+lemma is_exec_frag_cons:
+  "is_exec_frag A (s, (a, t) \<leadsto> ex) \<longleftrightarrow> (s, a, t) \<in> trans_of A \<and> is_exec_frag A (t, ex)"
   by (simp add: is_exec_frag_def)
 
-
-(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
 declare is_exec_frag_UU [simp] is_exec_frag_nil [simp] is_exec_frag_cons [simp]
 
-(* ---------------------------------------------------------------------------- *)
-                           section "laststate"
-(* ---------------------------------------------------------------------------- *)
 
-lemma laststate_UU: "laststate (s,UU) = s"
+subsubsection \<open>\<open>laststate\<close>\<close>
+
+lemma laststate_UU: "laststate (s, UU) = s"
   by (simp add: laststate_def)
 
-lemma laststate_nil: "laststate (s,nil) = s"
+lemma laststate_nil: "laststate (s, nil) = s"
   by (simp add: laststate_def)
 
-lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at\<leadsto>ex) = laststate (snd at,ex)"
-  apply (simp (no_asm) add: laststate_def)
-  apply (case_tac "ex=nil")
-  apply (simp (no_asm_simp))
-  apply (simp (no_asm_simp))
+lemma laststate_cons: "Finite ex \<Longrightarrow> laststate (s, at \<leadsto> ex) = laststate (snd at, ex)"
+  apply (simp add: laststate_def)
+  apply (cases "ex = nil")
+  apply simp
+  apply simp
   apply (drule Finite_Last1 [THEN mp])
   apply assumption
   apply defined
@@ -277,60 +268,56 @@
 
 declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
 
-lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
-  apply (tactic "Seq_Finite_induct_tac @{context} 1")
-  done
+lemma exists_laststate: "Finite ex \<Longrightarrow> \<forall>s. \<exists>u. laststate (s, ex) = u"
+  by (tactic "Seq_Finite_induct_tac @{context} 1")
 
 
-subsection "has_trace, mk_trace"
+subsection \<open>\<open>has_trace\<close> \<open>mk_trace\<close>\<close>
 
-(* alternative definition of has_trace tailored for the refinement proof, as it does not
-   take the detour of schedules *)
-
-lemma has_trace_def2:
-  "has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
+(*alternative definition of has_trace tailored for the refinement proof, as it does not
+  take the detour of schedules*)
+lemma has_trace_def2: "has_trace A b \<longleftrightarrow> (\<exists>ex \<in> executions A. b = mk_trace A $ (snd ex))"
   apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def [abs_def])
   apply auto
   done
 
 
-subsection "signatures and executions, schedules"
+subsection \<open>Signatures and executions, schedules\<close>
 
-(* All executions of A have only actions of A. This is only true because of the
-   predicate state_trans (part of the predicate IOA): We have no dependent types.
-   For executions of parallel automata this assumption is not needed, as in par_def
-   this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
+text \<open>
+  All executions of \<open>A\<close> have only actions of \<open>A\<close>. This is only true because of
+  the predicate \<open>state_trans\<close> (part of the predicate \<open>IOA\<close>): We have no
+  dependent types. For executions of parallel automata this assumption is not
+  needed, as in \<open>par_def\<close> this condition is included once more. (See Lemmas
+  1.1.1c in CompoExecs for example.)
+\<close>
 
 lemma execfrag_in_sig:
-  "!! A. is_trans_of A ==>
-  ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
+  "is_trans_of A \<Longrightarrow> \<forall>s. is_exec_frag A (s, xs) \<longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ xs)"
   apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
     @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
-  (* main case *)
+  text \<open>main case\<close>
   apply (auto simp add: is_trans_of_def)
   done
 
 lemma exec_in_sig:
-  "!! A.[|  is_trans_of A; x:executions A |] ==>
-  Forall (%a. a:act A) (filter_act$(snd x))"
+  "is_trans_of A \<Longrightarrow> x \<in> executions A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ (snd x))"
   apply (simp add: executions_def)
   apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
   apply (rule execfrag_in_sig [THEN spec, THEN mp])
   apply auto
   done
 
-lemma scheds_in_sig:
-  "!! A.[|  is_trans_of A; x:schedules A |] ==>
-    Forall (%a. a:act A) x"
+lemma scheds_in_sig: "is_trans_of A \<Longrightarrow> x \<in> schedules A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) x"
   apply (unfold schedules_def has_schedule_def [abs_def])
   apply (fast intro!: exec_in_sig)
   done
 
 
-subsection "executions are prefix closed"
+subsection \<open>Executions are prefix closed\<close>
 
-(* only admissible in y, not if done in x !! *)
-lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
+(*only admissible in y, not if done in x!*)
+lemma execfrag_prefixclosed: "\<forall>x s. is_exec_frag A (s, x) \<and> y \<sqsubseteq> x \<longrightarrow> is_exec_frag A (s, y)"
   apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
   apply (intro strip)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
@@ -341,11 +328,9 @@
 lemmas exec_prefixclosed =
   conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]]
 
-
-(* second prefix notion for Finite x *)
-
+(*second prefix notion for Finite x*)
 lemma exec_prefix2closed [rule_format]:
-  "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
+  "\<forall>y s. is_exec_frag A (s, x @@ y) \<longrightarrow> is_exec_frag A (s, x)"
   apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
   apply (intro strip)
   apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)