# HG changeset patch
# User wenzelm
# Date 1452983090 -3600
# Node ID bdaa0eb0fc7420ef07ddd1f1a182550fd57ea8fc
# Parent  eb9f5ee249f9bd070fdbb4b5d7fff61466cb67d5
misc tuning and modernization;

diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -10,590 +10,506 @@
 
 default_sort type
 
-definition
-  cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
-  "cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
-definition
-  \<comment> \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
-  cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where
-  "cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)"
+definition cex_abs :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
+  where "cex_abs f ex = (f (fst ex), Map (\<lambda>(a, t). (a, f t)) $ (snd ex))"
+
+text \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
+definition cex_absSeq ::
+    "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a option, 's1) transition Seq \<Rightarrow> ('a option, 's2)transition Seq"
+  where "cex_absSeq f = (\<lambda>s. Map (\<lambda>(s, a, t). (f s, a, f t)) $ s)"
 
-definition
-  is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_abstraction 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
-            --> (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)))"
+definition is_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_abstraction 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> f s \<midarrow>a\<midarrow>A\<rightarrow> f t))"
+
+definition weakeningIOA :: "('a, 's2) ioa \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
+  where "weakeningIOA A C h \<longleftrightarrow> (\<forall>ex. ex \<in> executions C \<longrightarrow> cex_abs h ex \<in> executions A)"
 
-definition
-  weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where
-  "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)"
-definition
-  temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
-  "temp_strengthening Q P h = (!ex. (cex_abs h ex \<TTurnstile> Q) --> (ex \<TTurnstile> P))"
-definition
-  temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
-  "temp_weakening Q P h = temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
+definition temp_strengthening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
+  where "temp_strengthening Q P h \<longleftrightarrow> (\<forall>ex. (cex_abs h ex \<TTurnstile> Q) \<longrightarrow> (ex \<TTurnstile> P))"
+
+definition temp_weakening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
+  where "temp_weakening Q P h \<longleftrightarrow> temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
 
-definition
-  state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
-  "state_strengthening Q P h = (!s t a.  Q (h(s),a,h(t)) --> P (s,a,t))"
-definition
-  state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
-  "state_weakening Q P h = state_strengthening (\<^bold>\<not>Q) (\<^bold>\<not>P) h"
+definition state_strengthening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
+  where "state_strengthening Q P h \<longleftrightarrow> (\<forall>s t a. Q (h s, a, h t) \<longrightarrow> P (s, a, t))"
 
-definition
-  is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
-  "is_live_abstraction h CL AM =
-     (is_abstraction h (fst CL) (fst AM) &
-      temp_weakening (snd AM) (snd CL) h)"
+definition state_weakening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
+  where "state_weakening Q P h \<longleftrightarrow> state_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
+
+definition is_live_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
+  where "is_live_abstraction h CL AM \<longleftrightarrow>
+    is_abstraction h (fst CL) (fst AM) \<and> temp_weakening (snd AM) (snd CL) h"
 
 
+(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
 axiomatization where
-(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
-ex2seq_abs_cex:
-  "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
+  ex2seq_abs_cex: "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
 
-axiomatization where
 (* analog to the proved thm strength_Box - proof skipped as trivial *)
-weak_Box:
-"temp_weakening P Q h
- ==> temp_weakening (\<box>P) (\<box>Q) h"
-
 axiomatization where
+  weak_Box: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<box>P) (\<box>Q) h"
+
 (* analog to the proved thm strength_Next - proof skipped as trivial *)
-weak_Next:
-"temp_weakening P Q h
- ==> temp_weakening (Next P) (Next Q) h"
+axiomatization where
+  weak_Next: "temp_weakening P Q h \<Longrightarrow> temp_weakening (Next P) (Next Q) h"
 
 
-subsection "cex_abs"
+subsection \<open>\<open>cex_abs\<close>\<close>
 
-lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)"
+lemma cex_abs_UU [simp]: "cex_abs f (s, UU) = (f s, UU)"
   by (simp add: cex_abs_def)
 
-lemma cex_abs_nil: "cex_abs f (s,nil) = (f s, nil)"
+lemma cex_abs_nil [simp]: "cex_abs f (s,nil) = (f s, nil)"
   by (simp add: cex_abs_def)
 
-lemma cex_abs_cons: "cex_abs f (s,(a,t)\<leadsto>ex) = (f s, (a,f t) \<leadsto> (snd (cex_abs f (t,ex))))"
+lemma cex_abs_cons [simp]:
+  "cex_abs f (s, (a, t) \<leadsto> ex) = (f s, (a, f t) \<leadsto> (snd (cex_abs f (t, ex))))"
   by (simp add: cex_abs_def)
 
-declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp]
-
 
-subsection "lemmas"
+subsection \<open>Lemmas\<close>
 
-lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex \<TTurnstile> P) --> (cex_abs h ex \<TTurnstile> Q))"
+lemma temp_weakening_def2: "temp_weakening Q P h \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P) \<longrightarrow> (cex_abs h ex \<TTurnstile> Q))"
   apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def)
   apply auto
   done
 
-lemma state_weakening_def2: "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))"
+lemma state_weakening_def2: "state_weakening Q P h \<longleftrightarrow> (\<forall>s t a. P (s, a, t) \<longrightarrow> Q (h s, a, h t))"
   apply (simp add: state_weakening_def state_strengthening_def NOT_def)
   apply auto
   done
 
 
-subsection "Abstraction Rules for Properties"
+subsection \<open>Abstraction Rules for Properties\<close>
 
 lemma exec_frag_abstraction [rule_format]:
- "[| is_abstraction h C A |] ==>
-  !s. reachable C s & is_exec_frag C (s,xs)
-  --> is_exec_frag A (cex_abs h (s,xs))"
-apply (unfold cex_abs_def)
-apply simp
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
-txt \<open>main case\<close>
-apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
-done
+  "is_abstraction h C A \<Longrightarrow>
+    \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow> is_exec_frag A (cex_abs h (s, xs))"
+  apply (simp add: cex_abs_def)
+  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  txt \<open>main case\<close>
+  apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
+  done
+
+lemma abs_is_weakening: "is_abstraction h C A \<Longrightarrow> weakeningIOA A C h"
+  apply (simp add: weakeningIOA_def)
+  apply auto
+  apply (simp add: executions_def)
+  txt \<open>start state\<close>
+  apply (rule conjI)
+  apply (simp add: is_abstraction_def cex_abs_def)
+  txt \<open>is-execution-fragment\<close>
+  apply (erule exec_frag_abstraction)
+  apply (simp add: reachable.reachable_0)
+  done
 
 
-lemma abs_is_weakening: "is_abstraction h C A ==> weakeningIOA A C h"
-apply (simp add: weakeningIOA_def)
-apply auto
-apply (simp add: executions_def)
-txt \<open>start state\<close>
-apply (rule conjI)
-apply (simp add: is_abstraction_def cex_abs_def)
-txt \<open>is-execution-fragment\<close>
-apply (erule exec_frag_abstraction)
-apply (simp add: reachable.reachable_0)
-done
+lemma AbsRuleT1:
+  "is_abstraction h C A \<Longrightarrow> validIOA A Q \<Longrightarrow> temp_strengthening Q P h \<Longrightarrow> validIOA C P"
+  apply (drule abs_is_weakening)
+  apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
+  apply (auto simp add: split_paired_all)
+  done
 
 
-lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |]
-          ==> validIOA C P"
-apply (drule abs_is_weakening)
-apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
-apply (auto simp add: split_paired_all)
-done
+(* FIXME: to TLS.thy *)
 
-
-(* FIX: Nach TLS.ML *)
-
-lemma IMPLIES_temp_sat: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) = ((ex \<TTurnstile> P) --> (ex \<TTurnstile> Q))"
+lemma IMPLIES_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<longrightarrow> (ex \<TTurnstile> Q))"
   by (simp add: IMPLIES_def temp_sat_def satisfies_def)
 
-lemma AND_temp_sat: "(ex \<TTurnstile> P \<^bold>\<and> Q) = ((ex \<TTurnstile> P) & (ex \<TTurnstile> Q))"
+lemma AND_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<and> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<and> (ex \<TTurnstile> Q))"
   by (simp add: AND_def temp_sat_def satisfies_def)
 
-lemma OR_temp_sat: "(ex \<TTurnstile> P \<^bold>\<or> Q) = ((ex \<TTurnstile> P) | (ex \<TTurnstile> Q))"
+lemma OR_temp_sat [simp]: "(ex \<TTurnstile> P \<^bold>\<or> Q) \<longleftrightarrow> ((ex \<TTurnstile> P) \<or> (ex \<TTurnstile> Q))"
   by (simp add: OR_def temp_sat_def satisfies_def)
 
-lemma NOT_temp_sat: "(ex \<TTurnstile> \<^bold>\<not> P) = (~ (ex \<TTurnstile> P))"
+lemma NOT_temp_sat [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))"
   by (simp add: NOT_def temp_sat_def satisfies_def)
 
-declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp]
-
 
 lemma AbsRuleT2:
-   "[|is_live_abstraction h (C,L) (A,M);
-          validLIOA (A,M) Q;  temp_strengthening Q P h |]
-          ==> validLIOA (C,L) P"
-apply (unfold is_live_abstraction_def)
-apply auto
-apply (drule abs_is_weakening)
-apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (auto simp add: split_paired_all)
-done
+  "is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A, M) Q \<Longrightarrow> temp_strengthening Q P h
+    \<Longrightarrow> validLIOA (C, L) P"
+  apply (unfold is_live_abstraction_def)
+  apply auto
+  apply (drule abs_is_weakening)
+  apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
+  apply (auto simp add: split_paired_all)
+  done
 
 
 lemma AbsRuleTImprove:
-   "[|is_live_abstraction h (C,L) (A,M);
-          validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q);  temp_strengthening Q P h;
-          temp_weakening H1 H2 h; validLIOA (C,L) H2 |]
-          ==> validLIOA (C,L) P"
-apply (unfold is_live_abstraction_def)
-apply auto
-apply (drule abs_is_weakening)
-apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
-apply (auto simp add: split_paired_all)
-done
+  "is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q) \<Longrightarrow>
+    temp_strengthening Q P h \<Longrightarrow> temp_weakening H1 H2 h \<Longrightarrow> validLIOA (C, L) H2 \<Longrightarrow>
+    validLIOA (C, L) P"
+  apply (unfold is_live_abstraction_def)
+  apply auto
+  apply (drule abs_is_weakening)
+  apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
+  apply (auto simp add: split_paired_all)
+  done
 
 
-subsection "Correctness of safe abstraction"
+subsection \<open>Correctness of safe abstraction\<close>
+
+lemma abstraction_is_ref_map: "is_abstraction h C A \<Longrightarrow> is_ref_map h C A"
+  apply (auto simp: is_abstraction_def is_ref_map_def)
+  apply (rule_tac x = "(a,h t) \<leadsto>nil" in exI)
+  apply (simp add: move_def)
+  done
 
-lemma abstraction_is_ref_map:
-"is_abstraction h C A ==> is_ref_map h C A"
-apply (unfold is_abstraction_def is_ref_map_def)
-apply auto
-apply (rule_tac x = "(a,h t) \<leadsto>nil" in exI)
-apply (simp add: move_def)
-done
+lemma abs_safety: "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_abstraction h C A \<Longrightarrow> C =<| A"
+  apply (simp add: ioa_implements_def)
+  apply (rule trace_inclusion)
+  apply (simp (no_asm) add: externals_def)
+  apply (auto)[1]
+  apply (erule abstraction_is_ref_map)
+  done
 
 
-lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A);
-                   is_abstraction h C A |]
-                ==> C =<| A"
-apply (simp add: ioa_implements_def)
-apply (rule trace_inclusion)
-apply (simp (no_asm) add: externals_def)
-apply (auto)[1]
-apply (erule abstraction_is_ref_map)
-done
+subsection \<open>Correctness of life abstraction\<close>
+
+text \<open>
+  Reduces to \<open>Filter (Map fst x) = Filter (Map fst (Map (\<lambda>(a, t). (a, x)) x)\<close>,
+  that is to special Map Lemma.
+\<close>
+lemma traces_coincide_abs:
+  "ext C = ext A \<Longrightarrow> mk_trace C $ xs = mk_trace A $ (snd (cex_abs f (s, xs)))"
+  apply (unfold cex_abs_def mk_trace_def filter_act_def)
+  apply simp
+  apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
+  done
 
 
-subsection "Correctness of life abstraction"
-
-(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
-   that is to special Map Lemma *)
-lemma traces_coincide_abs:
-  "ext C = ext A
-         ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
-apply (unfold cex_abs_def mk_trace_def filter_act_def)
-apply simp
-apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
-done
-
-
-(* Does not work with abstraction_is_ref_map as proof of abs_safety, because
-   is_live_abstraction includes temp_strengthening which is necessarily based
-   on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
-   way for cex_abs *)
-lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A);
-                   is_live_abstraction h (C,M) (A,L) |]
-                ==> live_implements (C,M) (A,L)"
-apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
-apply auto
-apply (rule_tac x = "cex_abs h ex" in exI)
-apply auto
-  (* Traces coincide *)
+text \<open>
+  Does not work with \<open>abstraction_is_ref_map\<close> as proof of \<open>abs_safety\<close>, because
+  \<open>is_live_abstraction\<close> includes \<open>temp_strengthening\<close> which is necessarily based
+  on \<open>cex_abs\<close> and not on \<open>corresp_ex\<close>. Thus, the proof is redone in a more specific
+  way for \<open>cex_abs\<close>.
+\<close>
+lemma abs_liveness:
+  "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_abstraction h (C, M) (A, L) \<Longrightarrow>
+    live_implements (C, M) (A, L)"
+  apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
+  apply auto
+  apply (rule_tac x = "cex_abs h ex" in exI)
+  apply auto
+  text \<open>Traces coincide\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (rule traces_coincide_abs)
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
 
-  (* cex_abs is execution *)
+  text \<open>\<open>cex_abs\<close> is execution\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
-  (* start state *)
+  text \<open>start state\<close>
   apply (rule conjI)
   apply (simp add: is_abstraction_def cex_abs_def)
-  (* is-execution-fragment *)
+  text \<open>\<open>is_execution_fragment\<close>\<close>
   apply (erule exec_frag_abstraction)
   apply (simp add: reachable.reachable_0)
 
- (* Liveness *)
-apply (simp add: temp_weakening_def2)
- apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-done
+  text \<open>Liveness\<close>
+  apply (simp add: temp_weakening_def2)
+   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  done
 
-(* FIX: NAch Traces.ML bringen *)
+(* FIXME: to Traces.thy *)
 
-lemma implements_trans:
-"[| A =<| B; B =<| C|] ==> A =<| C"
-by (auto simp add: ioa_implements_def)
+lemma implements_trans: "A =<| B \<Longrightarrow> B =<| C \<Longrightarrow> A =<| C"
+  by (auto simp add: ioa_implements_def)
 
 
-subsection "Abstraction Rules for Automata"
+subsection \<open>Abstraction Rules for Automata\<close>
 
-lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A);
-                   inp(Q)=inp(P); out(Q)=out(P);
-                   is_abstraction h1 C A;
-                   A =<| Q ;
-                   is_abstraction h2 Q P |]
-                ==> C =<| P"
-apply (drule abs_safety)
-apply assumption+
-apply (drule abs_safety)
-apply assumption+
-apply (erule implements_trans)
-apply (erule implements_trans)
-apply assumption
-done
+lemma AbsRuleA1:
+  "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow>
+    is_abstraction h1 C A \<Longrightarrow> A =<| Q \<Longrightarrow> is_abstraction h2 Q P \<Longrightarrow> C =<| P"
+  apply (drule abs_safety)
+  apply assumption+
+  apply (drule abs_safety)
+  apply assumption+
+  apply (erule implements_trans)
+  apply (erule implements_trans)
+  apply assumption
+  done
 
-
-lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A);
-                   inp(Q)=inp(P); out(Q)=out(P);
-                   is_live_abstraction h1 (C,LC) (A,LA);
-                   live_implements (A,LA) (Q,LQ) ;
-                   is_live_abstraction h2 (Q,LQ) (P,LP) |]
-                ==> live_implements (C,LC) (P,LP)"
-apply (drule abs_liveness)
-apply assumption+
-apply (drule abs_liveness)
-apply assumption+
-apply (erule live_implements_trans)
-apply (erule live_implements_trans)
-apply assumption
-done
+lemma AbsRuleA2:
+  "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow>
+    is_live_abstraction h1 (C, LC) (A, LA) \<Longrightarrow> live_implements (A, LA) (Q, LQ) \<Longrightarrow>
+    is_live_abstraction h2 (Q, LQ) (P, LP) \<Longrightarrow> live_implements (C, LC) (P, LP)"
+  apply (drule abs_liveness)
+  apply assumption+
+  apply (drule abs_liveness)
+  apply assumption+
+  apply (erule live_implements_trans)
+  apply (erule live_implements_trans)
+  apply assumption
+  done
 
 
 declare split_paired_All [simp del]
 
 
-subsection "Localizing Temporal Strengthenings and Weakenings"
+subsection \<open>Localizing Temporal Strengthenings and Weakenings\<close>
 
 lemma strength_AND:
-"[| temp_strengthening P1 Q1 h;
-          temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
-apply (unfold temp_strengthening_def)
-apply auto
-done
+  "temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
+    temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
+  by (auto simp: temp_strengthening_def)
 
 lemma strength_OR:
-"[| temp_strengthening P1 Q1 h;
-          temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
-apply (unfold temp_strengthening_def)
-apply auto
-done
+  "temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
+    temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
+  by (auto simp: temp_strengthening_def)
 
-lemma strength_NOT:
-"[| temp_weakening P Q h |]
-       ==> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
-apply (unfold temp_strengthening_def)
-apply (simp add: temp_weakening_def2)
-apply auto
-done
+lemma strength_NOT: "temp_weakening P Q h \<Longrightarrow> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
+  by (auto simp: temp_weakening_def2 temp_strengthening_def)
 
 lemma strength_IMPLIES:
-"[| temp_weakening P1 Q1 h;
-          temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
-apply (unfold temp_strengthening_def)
-apply (simp add: temp_weakening_def2)
-done
+  "temp_weakening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
+    temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
+  by (simp add: temp_weakening_def2 temp_strengthening_def)
 
 
 lemma weak_AND:
-"[| temp_weakening P1 Q1 h;
-          temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
-apply (simp add: temp_weakening_def2)
-done
+  "temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
+    temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
+  by (simp add: temp_weakening_def2)
 
 lemma weak_OR:
-"[| temp_weakening P1 Q1 h;
-          temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
-apply (simp add: temp_weakening_def2)
-done
+  "temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
+    temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
+  by (simp add: temp_weakening_def2)
 
 lemma weak_NOT:
-"[| temp_strengthening P Q h |]
-       ==> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
-apply (unfold temp_strengthening_def)
-apply (simp add: temp_weakening_def2)
-apply auto
-done
+  "temp_strengthening P Q h \<Longrightarrow> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
+  by (auto simp add: temp_weakening_def2 temp_strengthening_def)
 
 lemma weak_IMPLIES:
-"[| temp_strengthening P1 Q1 h;
-          temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
-apply (unfold temp_strengthening_def)
-apply (simp add: temp_weakening_def2)
-done
+  "temp_strengthening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
+    temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
+  by (simp add: temp_weakening_def2 temp_strengthening_def)
 
 
 subsubsection \<open>Box\<close>
 
-(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
-lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
-apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
-done
+(* FIXME: should be same as nil_is_Conc2 when all nils are turned to right side! *)
+lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x = nil \<and> y = UU))"
+  by (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
 
 lemma ex2seqConc [rule_format]:
-"Finite s1 -->
-  (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
-apply (rule impI)
-apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
-apply blast
-(* main case *)
-apply clarify
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-(* UU case *)
-apply (simp add: nil_is_Conc)
-(* nil case *)
-apply (simp add: nil_is_Conc)
-(* cons case *)
-apply (tactic \<open>pair_tac @{context} "aa" 1\<close>)
-apply auto
-done
+  "Finite s1 \<longrightarrow> (\<forall>ex. (s \<noteq> nil \<and> s \<noteq> UU \<and> ex2seq ex = s1 @@ s) \<longrightarrow> (\<exists>ex'. s = ex2seq ex'))"
+  apply (rule impI)
+  apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
+  apply blast
+  text \<open>main case\<close>
+  apply clarify
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  text \<open>\<open>UU\<close> case\<close>
+  apply (simp add: nil_is_Conc)
+  text \<open>\<open>nil\<close> case\<close>
+  apply (simp add: nil_is_Conc)
+  text \<open>cons case\<close>
+  apply (tactic \<open>pair_tac @{context} "aa" 1\<close>)
+  apply auto
+  done
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
-
-lemma ex2seq_tsuffix:
-"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')"
-apply (unfold tsuffix_def suffix_def)
-apply auto
-apply (drule ex2seqConc)
-apply auto
-done
+lemma ex2seq_tsuffix: "tsuffix s (ex2seq ex) \<Longrightarrow> \<exists>ex'. s = (ex2seq ex')"
+  apply (unfold tsuffix_def suffix_def)
+  apply auto
+  apply (drule ex2seqConc)
+  apply auto
+  done
 
 
-(* FIX: NAch Sequence.ML bringen *)
+(* FIXME: to Sequence.thy *)
 
-lemma Mapnil: "(Map f$s = nil) = (s=nil)"
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-done
+lemma Mapnil: "Map f $ s = nil \<longleftrightarrow> s = nil"
+  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
 
-lemma MapUU: "(Map f$s = UU) = (s=UU)"
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-done
+lemma MapUU: "Map f $ s = UU \<longleftrightarrow> s = UU"
+  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
 
 
-(* important property of cex_absSeq: As it is a 1to1 correspondence,
+(*important property of cex_absSeq: As it is a 1to1 correspondence,
   properties carry over *)
-
-lemma cex_absSeq_tsuffix:
-"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
-apply (unfold tsuffix_def suffix_def cex_absSeq_def)
-apply auto
-apply (simp add: Mapnil)
-apply (simp add: MapUU)
-apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI)
-apply (simp add: Map2Finite MapConc)
-done
+lemma cex_absSeq_tsuffix: "tsuffix s t \<Longrightarrow> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
+  apply (unfold tsuffix_def suffix_def cex_absSeq_def)
+  apply auto
+  apply (simp add: Mapnil)
+  apply (simp add: MapUU)
+  apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))$s1" in exI)
+  apply (simp add: Map2Finite MapConc)
+  done
 
 
-lemma strength_Box:
-"[| temp_strengthening P Q h |]
-       ==> temp_strengthening (\<box>P) (\<box>Q) h"
-apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
-apply clarify
-apply (frule ex2seq_tsuffix)
-apply clarify
-apply (drule_tac h = "h" in cex_absSeq_tsuffix)
-apply (simp add: ex2seq_abs_cex)
-done
+lemma strength_Box: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<box>P) (\<box>Q) h"
+  apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
+  apply clarify
+  apply (frule ex2seq_tsuffix)
+  apply clarify
+  apply (drule_tac h = "h" in cex_absSeq_tsuffix)
+  apply (simp add: ex2seq_abs_cex)
+  done
 
 
 subsubsection \<open>Init\<close>
 
 lemma strength_Init:
-"[| state_strengthening P Q h |]
-       ==> temp_strengthening (Init P) (Init Q) h"
-apply (unfold temp_strengthening_def state_strengthening_def
-  temp_sat_def satisfies_def Init_def unlift_def)
-apply auto
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+  "state_strengthening P Q h \<Longrightarrow> temp_strengthening (Init P) (Init Q) h"
+  apply (unfold temp_strengthening_def state_strengthening_def
+    temp_sat_def satisfies_def Init_def unlift_def)
+  apply auto
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  done
 
 
 subsubsection \<open>Next\<close>
 
-lemma TL_ex2seq_UU:
-"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+lemma TL_ex2seq_UU: "TL $ (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL $ (ex2seq ex) = UU"
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  done
 
-lemma TL_ex2seq_nil:
-"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+lemma TL_ex2seq_nil: "TL $ (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL $ (ex2seq ex) = nil"
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  done
 
-(* FIX: put to Sequence Lemmas *)
-lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
-apply (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
-done
+(* FIXME: put to Sequence Lemmas *)
+lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)"
+  by (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
 
-(* important property of cex_absSeq: As it is a 1to1 correspondence,
-  properties carry over *)
-
-lemma cex_absSeq_TL:
-"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))"
-apply (unfold cex_absSeq_def)
-apply (simp add: MapTL)
-done
+(*important property of cex_absSeq: As it is a 1to1 correspondence,
+  properties carry over*)
+lemma cex_absSeq_TL: "cex_absSeq h (TL $ s) = TL $ (cex_absSeq h s)"
+  by (simp add: MapTL cex_absSeq_def)
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
+lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL$(ex2seq ex) = ex2seq ex'"
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply auto
+  done
 
-lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply auto
-done
+lemma ex2seqnilTL: "TL $ (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU"
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  done
 
-
-lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (Next P) (Next Q) h"
+  apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
+  apply simp
+  apply auto
+  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
+  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
+  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
+  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
+  text \<open>cons case\<close>
+  apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL)
+  apply (erule conjE)
+  apply (drule TLex2seq)
+  apply assumption
+  apply auto
+  done
 
 
-lemma strength_Next:
-"[| temp_strengthening P Q h |]
-       ==> temp_strengthening (Next P) (Next Q) h"
-apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
-apply simp
-apply auto
-apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
-apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
-apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
-apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
-(* cons case *)
-apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL)
-apply (erule conjE)
-apply (drule TLex2seq)
-apply assumption
-apply auto
-done
+text \<open>Localizing Temporal Weakenings - 2\<close>
 
-
-text \<open>Localizing Temporal Weakenings     - 2\<close>
-
-lemma weak_Init:
-"[| state_weakening P Q h |]
-       ==> temp_weakening (Init P) (Init Q) h"
-apply (simp add: temp_weakening_def2 state_weakening_def2
-  temp_sat_def satisfies_def Init_def unlift_def)
-apply auto
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+lemma weak_Init: "state_weakening P Q h \<Longrightarrow> temp_weakening (Init P) (Init Q) h"
+  apply (simp add: temp_weakening_def2 state_weakening_def2
+    temp_sat_def satisfies_def Init_def unlift_def)
+  apply auto
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  done
 
 
 text \<open>Localizing Temproal Strengthenings - 3\<close>
 
-lemma strength_Diamond:
-"[| temp_strengthening P Q h |]
-       ==> temp_strengthening (\<diamond>P) (\<diamond>Q) h"
-apply (unfold Diamond_def)
-apply (rule strength_NOT)
-apply (rule weak_Box)
-apply (erule weak_NOT)
-done
+lemma strength_Diamond: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<diamond>P) (\<diamond>Q) h"
+  apply (unfold Diamond_def)
+  apply (rule strength_NOT)
+  apply (rule weak_Box)
+  apply (erule weak_NOT)
+  done
 
 lemma strength_Leadsto:
-"[| temp_weakening P1 P2 h;
-          temp_strengthening Q1 Q2 h |]
-       ==> temp_strengthening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
-apply (unfold Leadsto_def)
-apply (rule strength_Box)
-apply (erule strength_IMPLIES)
-apply (erule strength_Diamond)
-done
+  "temp_weakening P1 P2 h \<Longrightarrow> temp_strengthening Q1 Q2 h \<Longrightarrow>
+    temp_strengthening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
+  apply (unfold Leadsto_def)
+  apply (rule strength_Box)
+  apply (erule strength_IMPLIES)
+  apply (erule strength_Diamond)
+  done
 
 
 text \<open>Localizing Temporal Weakenings - 3\<close>
 
-lemma weak_Diamond:
-"[| temp_weakening P Q h |]
-       ==> temp_weakening (\<diamond>P) (\<diamond>Q) h"
-apply (unfold Diamond_def)
-apply (rule weak_NOT)
-apply (rule strength_Box)
-apply (erule strength_NOT)
-done
+lemma weak_Diamond: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<diamond>P) (\<diamond>Q) h"
+  apply (unfold Diamond_def)
+  apply (rule weak_NOT)
+  apply (rule strength_Box)
+  apply (erule strength_NOT)
+  done
 
 lemma weak_Leadsto:
-"[| temp_strengthening P1 P2 h;
-          temp_weakening Q1 Q2 h |]
-       ==> temp_weakening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
-apply (unfold Leadsto_def)
-apply (rule weak_Box)
-apply (erule weak_IMPLIES)
-apply (erule weak_Diamond)
-done
+  "temp_strengthening P1 P2 h \<Longrightarrow> temp_weakening Q1 Q2 h \<Longrightarrow>
+    temp_weakening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
+  apply (unfold Leadsto_def)
+  apply (rule weak_Box)
+  apply (erule weak_IMPLIES)
+  apply (erule weak_Diamond)
+  done
 
 lemma weak_WF:
-  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
-    ==> temp_weakening (WF A acts) (WF C acts) h"
-apply (unfold WF_def)
-apply (rule weak_IMPLIES)
-apply (rule strength_Diamond)
-apply (rule strength_Box)
-apply (rule strength_Init)
-apply (rule_tac [2] weak_Box)
-apply (rule_tac [2] weak_Diamond)
-apply (rule_tac [2] weak_Init)
-apply (auto simp add: state_weakening_def state_strengthening_def
-  xt2_def plift_def option_lift_def NOT_def)
-done
+  "(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s)
+    \<Longrightarrow> temp_weakening (WF A acts) (WF C acts) h"
+  apply (unfold WF_def)
+  apply (rule weak_IMPLIES)
+  apply (rule strength_Diamond)
+  apply (rule strength_Box)
+  apply (rule strength_Init)
+  apply (rule_tac [2] weak_Box)
+  apply (rule_tac [2] weak_Diamond)
+  apply (rule_tac [2] weak_Init)
+  apply (auto simp add: state_weakening_def state_strengthening_def
+    xt2_def plift_def option_lift_def NOT_def)
+  done
 
 lemma weak_SF:
-  " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
-    ==> temp_weakening (SF A acts) (SF C acts) h"
-apply (unfold SF_def)
-apply (rule weak_IMPLIES)
-apply (rule strength_Box)
-apply (rule strength_Diamond)
-apply (rule strength_Init)
-apply (rule_tac [2] weak_Box)
-apply (rule_tac [2] weak_Diamond)
-apply (rule_tac [2] weak_Init)
-apply (auto simp add: state_weakening_def state_strengthening_def
-  xt2_def plift_def option_lift_def NOT_def)
-done
+  "(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s)
+    \<Longrightarrow> temp_weakening (SF A acts) (SF C acts) h"
+  apply (unfold SF_def)
+  apply (rule weak_IMPLIES)
+  apply (rule strength_Box)
+  apply (rule strength_Diamond)
+  apply (rule strength_Init)
+  apply (rule_tac [2] weak_Box)
+  apply (rule_tac [2] weak_Diamond)
+  apply (rule_tac [2] weak_Init)
+  apply (auto simp add: state_weakening_def state_strengthening_def
+    xt2_def plift_def option_lift_def NOT_def)
+  done
 
 
 lemmas weak_strength_lemmas =
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/Compositionality.thy
--- a/src/HOL/HOLCF/IOA/Compositionality.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Compositionality.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -7,69 +7,71 @@
 imports CompoTraces
 begin
 
-lemma compatibility_consequence3: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"
-apply auto
-done
+lemma compatibility_consequence3: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eA \<or> eB) \<longrightarrow> A = eA"
+  by auto
+
+lemma Filter_actAisFilter_extA:
+  "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext A \<or> a \<in> ext B) tr \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ tr = Filter (\<lambda>a. a \<in> ext A) $ tr"
+  apply (rule ForallPFilterQR)
+  text \<open>i.e.: \<open>(\<forall>x. P x \<longrightarrow> (Q x = R x)) \<Longrightarrow> Forall P tr \<Longrightarrow> Filter Q $ tr = Filter R $ tr\<close>\<close>
+  prefer 2 apply assumption
+  apply (rule compatibility_consequence3)
+  apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
+  done
 
 
-lemma Filter_actAisFilter_extA: 
-"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==>  
-            Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"
-apply (rule ForallPFilterQR)
-(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
-prefer 2 apply (assumption)
-apply (rule compatibility_consequence3)
-apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
-done
+text \<open>
+  The next two theorems are only necessary, as there is no theorem
+  \<open>ext (A \<parallel> B) = ext (B \<parallel> A)\<close>
+\<close>
 
+lemma compatibility_consequence4: "eA \<longrightarrow> A \<Longrightarrow> eB \<and> \<not> eA \<longrightarrow> \<not> A \<Longrightarrow> (eB \<or> eA) \<longrightarrow> A = eA"
+  by auto
 
-(* the next two theorems are only necessary, as there is no theorem ext (A\<parallel>B) = ext (B\<parallel>A) *)
-
-lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"
-apply auto
-done
-
-lemma Filter_actAisFilter_extA2: "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==>  
-            Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"
-apply (rule ForallPFilterQR)
-prefer 2 apply (assumption)
-apply (rule compatibility_consequence4)
-apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
-done
+lemma Filter_actAisFilter_extA2:
+  "compatible A B \<Longrightarrow> Forall (\<lambda>a. a \<in> ext B \<or> a \<in> ext A) tr \<Longrightarrow>
+    Filter (\<lambda>a. a \<in> act A) $ tr = Filter (\<lambda>a. a \<in> ext A) $ tr"
+  apply (rule ForallPFilterQR)
+  prefer 2 apply (assumption)
+  apply (rule compatibility_consequence4)
+  apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
+  done
 
 
-subsection " Main Compositionality Theorem "
+subsection \<open>Main Compositionality Theorem\<close>
 
-lemma compositionality: "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2; 
-             is_asig_of A1; is_asig_of A2;  
-             is_asig_of B1; is_asig_of B2;  
-             compatible A1 B1; compatible A2 B2;  
-             A1 =<| A2;  
-             B1 =<| B2 |]  
-         ==> (A1 \<parallel> B1) =<| (A2 \<parallel> B2)"
-apply (simp add: is_asig_of_def)
-apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
-apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
-apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
-apply auto
-apply (simp add: compositionality_tr)
-apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2")
-prefer 2
-apply (simp add: externals_def)
-apply (erule conjE)+
-(* rewrite with proven subgoal *)
-apply (simp add: externals_of_par)
-apply auto
-
-(* 2 goals, the 3rd has been solved automatically *)
-(* 1: Filter A2 x : traces A2 *)
-apply (drule_tac A = "traces A1" in subsetD)
-apply assumption
-apply (simp add: Filter_actAisFilter_extA)
-(* 2: Filter B2 x : traces B2 *)
-apply (drule_tac A = "traces B1" in subsetD)
-apply assumption
-apply (simp add: Filter_actAisFilter_extA2)
-done
+lemma compositionality:
+  assumes "is_trans_of A1" and "is_trans_of A2"
+    and "is_trans_of B1" and "is_trans_of B2"
+    and "is_asig_of A1" and "is_asig_of A2"
+    and "is_asig_of B1" and "is_asig_of B2"
+    and "compatible A1 B1" and "compatible A2 B2"
+    and "A1 =<| A2" and "B1 =<| B2"
+  shows "(A1 \<parallel> B1) =<| (A2 \<parallel> B2)"
+  apply (insert assms)
+  apply (simp add: is_asig_of_def)
+  apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
+  apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
+  apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
+  apply auto
+  apply (simp add: compositionality_tr)
+  apply (subgoal_tac "ext A1 = ext A2 \<and> ext B1 = ext B2")
+  prefer 2
+  apply (simp add: externals_def)
+  apply (erule conjE)+
+  text \<open>rewrite with proven subgoal\<close>
+  apply (simp add: externals_of_par)
+  apply auto
+  text \<open>2 goals, the 3rd has been solved automatically\<close>
+  text \<open>1: \<open>Filter A2 x \<in> traces A2\<close>\<close>
+  apply (drule_tac A = "traces A1" in subsetD)
+  apply assumption
+  apply (simp add: Filter_actAisFilter_extA)
+  text \<open>2: \<open>Filter B2 x \<in> traces B2\<close>\<close>
+  apply (drule_tac A = "traces B1" in subsetD)
+  apply assumption
+  apply (simp add: Filter_actAisFilter_extA2)
+  done
 
 end
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/LiveIOA.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/LiveIOA.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -10,73 +10,64 @@
 
 default_sort type
 
-type_synonym
-  ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
+type_synonym ('a, 's) live_ioa = "('a, 's)ioa \<times> ('a, 's) ioa_temp"
 
-definition
-  validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
-  "validLIOA AL P = validIOA (fst AL) ((snd AL) \<^bold>\<longrightarrow> P)"
+definition validLIOA :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool"
+  where "validLIOA AL P \<longleftrightarrow> validIOA (fst AL) (snd AL \<^bold>\<longrightarrow> P)"
 
-definition
-  WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "WF A acts = (\<diamond>\<box>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
-definition
-  SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "SF A acts = (\<box>\<diamond>\<langle>%(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (%a. a : acts))\<rangle>)"
+definition WF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp"
+  where "WF A acts = (\<diamond>\<box>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)"
+
+definition SF :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) ioa_temp"
+  where "SF A acts = (\<box>\<diamond>\<langle>\<lambda>(s,a,t). Enabled A acts s\<rangle> \<^bold>\<longrightarrow> \<box>\<diamond>\<langle>xt2 (plift (\<lambda>a. a \<in> acts))\<rangle>)"
+
+definition liveexecutions :: "('a, 's) live_ioa \<Rightarrow> ('a, 's) execution set"
+  where "liveexecutions AP = {exec. exec \<in> executions (fst AP) \<and> (exec \<TTurnstile> snd AP)}"
 
-definition
-  liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
-  "liveexecutions AP = {exec. exec : executions (fst AP) & (exec \<TTurnstile> (snd AP))}"
-definition
-  livetraces :: "('a,'s)live_ioa => 'a trace set" where
-  "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
-definition
-  live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
-  "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
-                            (out (fst CL) = out (fst AM)) &
-                            livetraces CL <= livetraces AM)"
-definition
-  is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
-  "is_live_ref_map f CL AM =
-           (is_ref_map f (fst CL ) (fst AM) &
-            (! exec : executions (fst CL). (exec \<TTurnstile> (snd CL)) -->
-                                           ((corresp_ex (fst AM) f exec) \<TTurnstile> (snd AM))))"
+definition livetraces :: "('a, 's) live_ioa \<Rightarrow> 'a trace set"
+  where "livetraces AP = {mk_trace (fst AP) $ (snd ex) |ex. ex \<in> liveexecutions AP}"
+
+definition live_implements :: "('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
+  where "live_implements CL AM \<longleftrightarrow>
+    inp (fst CL) = inp (fst AM) \<and> out (fst CL) = out (fst AM) \<and>
+      livetraces CL \<subseteq> livetraces AM"
+
+definition is_live_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
+  where "is_live_ref_map f CL AM \<longleftrightarrow>
+    is_ref_map f (fst CL ) (fst AM) \<and>
+    (\<forall>exec \<in> executions (fst CL). (exec \<TTurnstile> (snd CL)) \<longrightarrow>
+      (corresp_ex (fst AM) f exec \<TTurnstile> snd AM))"
+
+lemma live_implements_trans:
+  "live_implements (A, LA) (B, LB) \<Longrightarrow> live_implements (B, LB) (C, LC) \<Longrightarrow>
+    live_implements (A, LA) (C, LC)"
+  by (auto simp: live_implements_def)
 
 
-lemma live_implements_trans:
-"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
-      ==> live_implements (A,LA) (C,LC)"
-apply (unfold live_implements_def)
-apply auto
-done
-
+subsection \<open>Correctness of live refmap\<close>
 
-subsection "Correctness of live refmap"
-
-lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
-                   is_live_ref_map f (C,M) (A,L) |]
-                ==> live_implements (C,M) (A,L)"
-apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
-apply auto
-apply (rule_tac x = "corresp_ex A f ex" in exI)
-apply auto
-  (* Traces coincide, Lemma 1 *)
+lemma live_implements:
+  "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_ref_map f (C, M) (A, L)
+    \<Longrightarrow> live_implements (C, M) (A, L)"
+  apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
+  apply auto
+  apply (rule_tac x = "corresp_ex A f ex" in exI)
+  apply auto
+  text \<open>Traces coincide, Lemma 1\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
-
-  (* corresp_ex is execution, Lemma 2 *)
+  text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
-  (* start state *)
+  text \<open>start state\<close>
   apply (rule conjI)
   apply (simp add: is_ref_map_def corresp_ex_def)
-  (* is-execution-fragment *)
+  text \<open>\<open>is_execution_fragment\<close>\<close>
   apply (erule lemma_2 [THEN spec, THEN mp])
   apply (simp add: reachable.reachable_0)
-
-done
+  done
 
 end
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/Pred.thy
--- a/src/HOL/HOLCF/IOA/Pred.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Pred.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -15,7 +15,7 @@
 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"  (*  ("|-") *)
+definition valid :: "'a predicate \<Rightarrow> bool"  (*  FIXME ("|-") *)
   where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
 
 definition NOT :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -8,240 +8,228 @@
 imports Simulations
 begin
 
-definition
-  (* Note: s2 instead of s1 in last argument type !! *)
-  corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
-                   -> ('s2 => ('a,'s2)pairs)" where
-  "corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of
-      nil =>  nil
-    | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
-                                 T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
-                             in
-                                (@cex. move A cex s a T')
-                                 @@ ((h$xs) T'))
-                        $x) )))"
+(*Note: s2 instead of s1 in last argument type!*)
+definition corresp_ex_simC ::
+    "('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) pairs \<rightarrow> ('s2 \<Rightarrow> ('a, 's2) pairs)"
+  where "corresp_ex_simC A R =
+    (fix $ (LAM h ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> nil
+    | x ## xs \<Rightarrow>
+        (flift1
+          (\<lambda>pr.
+            let
+              a = fst pr;
+              t = snd pr;
+              T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
+            in (SOME cex. move A cex s a T') @@ ((h $ xs) T')) $ x))))"
 
-definition
-  corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) =>
-                      ('a,'s1)execution => ('a,'s2)execution" where
-  "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
-                            in
-                               (S',(corresp_ex_simC A R$(snd ex)) S')"
+definition corresp_ex_sim ::
+    "('a, 's2) ioa \<Rightarrow> ('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
+  where "corresp_ex_sim A R ex \<equiv>
+    let S' = SOME s'. (fst ex, s') \<in> R \<and> s' \<in> starts_of A
+    in (S', (corresp_ex_simC A R $ (snd ex)) S')"
 
 
-subsection "corresp_ex_sim"
-
-lemma corresp_ex_simC_unfold: "corresp_ex_simC A R  = (LAM ex. (%s. case ex of
-       nil =>  nil
-     | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
-                                  T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
-                              in
-                                 (@cex. move A cex s a T')
-                               @@ ((corresp_ex_simC A R $xs) T'))
-                         $x) ))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (simp only: corresp_ex_simC_def)
-apply (rule beta_cfun)
-apply (simp add: flift1_def)
-done
+subsection \<open>\<open>corresp_ex_sim\<close>\<close>
 
-lemma corresp_ex_simC_UU: "(corresp_ex_simC A R$UU) s=UU"
-apply (subst corresp_ex_simC_unfold)
-apply simp
-done
-
-lemma corresp_ex_simC_nil: "(corresp_ex_simC A R$nil) s = nil"
-apply (subst corresp_ex_simC_unfold)
-apply simp
-done
+lemma corresp_ex_simC_unfold:
+  "corresp_ex_simC A R =
+    (LAM ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> nil
+    | x ## xs \<Rightarrow>
+        (flift1
+          (\<lambda>pr.
+            let
+              a = fst pr;
+              t = snd pr;
+              T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
+            in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R $ xs) T')) $ x)))"
+  apply (rule trans)
+  apply (rule fix_eq2)
+  apply (simp only: corresp_ex_simC_def)
+  apply (rule beta_cfun)
+  apply (simp add: flift1_def)
+  done
 
-lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)\<leadsto>xs)) s =
-           (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
-            in
-             (@cex. move A cex s a T')
-              @@ ((corresp_ex_simC A R$xs) T'))"
-apply (rule trans)
-apply (subst corresp_ex_simC_unfold)
-apply (simp add: Consq_def flift1_def)
-apply simp
-done
+lemma corresp_ex_simC_UU [simp]: "(corresp_ex_simC A R $ UU) s = UU"
+  apply (subst corresp_ex_simC_unfold)
+  apply simp
+  done
+
+lemma corresp_ex_simC_nil [simp]: "(corresp_ex_simC A R $ nil) s = nil"
+  apply (subst corresp_ex_simC_unfold)
+  apply simp
+  done
+
+lemma corresp_ex_simC_cons [simp]:
+  "(corresp_ex_simC A R $ ((a, t) \<leadsto> xs)) s =
+    (let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s a t'
+     in (SOME cex. move A cex s a T') @@ ((corresp_ex_simC A R $ xs) T'))"
+  apply (rule trans)
+  apply (subst corresp_ex_simC_unfold)
+  apply (simp add: Consq_def flift1_def)
+  apply simp
+  done
 
 
-declare corresp_ex_simC_UU [simp] corresp_ex_simC_nil [simp] corresp_ex_simC_cons [simp]
-
-
-subsection "properties of move"
-
-declare Let_def [simp del]
+subsection \<open>Properties of move\<close>
 
 lemma move_is_move_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-      let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-      (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"
-apply (unfold is_simulation_def)
-
-(* Does not perform conditional rewriting on assumptions automatically as
-   usual. Instantiate all variables per hand. Ask Tobias?? *)
-apply (subgoal_tac "? t' ex. (t,t') :R & move A ex s' a t'")
-prefer 2
-apply simp
-apply (erule conjE)
-apply (erule_tac x = "s" in allE)
-apply (erule_tac x = "s'" in allE)
-apply (erule_tac x = "t" in allE)
-apply (erule_tac x = "a" in allE)
-apply simp
-(* Go on as usual *)
-apply (erule exE)
-apply (drule_tac x = "t'" and P = "%t'. ? ex. (t,t') :R & move A ex s' a t'" in someI)
-apply (erule exE)
-apply (erule conjE)
-apply (simp add: Let_def)
-apply (rule_tac x = "ex" in someI)
-apply assumption
-done
-
-declare Let_def [simp]
+   "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+     let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+     in (t, T') \<in> R \<and> move A (SOME ex2. move A ex2 s' a T') s' a T'"
+  supply Let_def [simp del]
+  apply (unfold is_simulation_def)
+  (* Does not perform conditional rewriting on assumptions automatically as
+     usual. Instantiate all variables per hand. Ask Tobias?? *)
+  apply (subgoal_tac "\<exists>t' ex. (t, t') \<in> R \<and> move A ex s' a t'")
+  prefer 2
+  apply simp
+  apply (erule conjE)
+  apply (erule_tac x = "s" in allE)
+  apply (erule_tac x = "s'" in allE)
+  apply (erule_tac x = "t" in allE)
+  apply (erule_tac x = "a" in allE)
+  apply simp
+  (* Go on as usual *)
+  apply (erule exE)
+  apply (drule_tac x = "t'" and P = "\<lambda>t'. \<exists>ex. (t, t') \<in> R \<and> move A ex s' a t'" in someI)
+  apply (erule exE)
+  apply (erule conjE)
+  apply (simp add: Let_def)
+  apply (rule_tac x = "ex" in someI)
+  apply assumption
+  done
 
 lemma move_subprop1_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-     is_exec_frag A (s',@x. move A x s' a T')"
-apply (cut_tac move_is_move_sim)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+    in is_exec_frag A (s', SOME x. move A x s' a T')"
+  apply (cut_tac move_is_move_sim)
+  defer
+  apply assumption+
+  apply (simp add: move_def)
+  done
 
 lemma move_subprop2_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-    Finite (@x. move A x s' a T')"
-apply (cut_tac move_is_move_sim)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+    in Finite (SOME x. move A x s' a T')"
+  apply (cut_tac move_is_move_sim)
+  defer
+  apply assumption+
+  apply (simp add: move_def)
+  done
 
 lemma move_subprop3_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-     laststate (s',@x. move A x s' a T') = T'"
-apply (cut_tac move_is_move_sim)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+    in laststate (s', SOME x. move A x s' a T') = T'"
+  apply (cut_tac move_is_move_sim)
+  defer
+  apply assumption+
+  apply (simp add: move_def)
+  done
 
 lemma move_subprop4_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-      mk_trace A$((@x. move A x s' a T')) =
-        (if a:ext A then a\<leadsto>nil else nil)"
-apply (cut_tac move_is_move_sim)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+    in mk_trace A $ (SOME x. move A x s' a T') = (if a \<in> ext A then a \<leadsto> nil else nil)"
+  apply (cut_tac move_is_move_sim)
+  defer
+  apply assumption+
+  apply (simp add: move_def)
+  done
 
 lemma move_subprop5_sim:
-   "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
-    let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
-      (t,T'):R"
-apply (cut_tac move_is_move_sim)
-defer
-apply assumption+
-apply (simp add: move_def)
-done
+  "is_simulation R C A \<Longrightarrow> reachable C s \<Longrightarrow> s \<midarrow>a\<midarrow>C\<rightarrow> t \<Longrightarrow> (s, s') \<in> R \<Longrightarrow>
+    let T' = SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'
+    in (t, T') \<in> R"
+  apply (cut_tac move_is_move_sim)
+  defer
+  apply assumption+
+  apply (simp add: move_def)
+  done
 
 
 subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
 
 subsubsection "Lemmata for <=="
 
-(* ------------------------------------------------------
-                 Lemma 1 :Traces coincide
-   ------------------------------------------------------- *)
+text \<open>Lemma 1: Traces coincide\<close>
 
-declare split_if [split del]
 lemma traces_coincide_sim [rule_format (no_asm)]:
-  "[|is_simulation R C A; ext C = ext A|] ==>
-         !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
-             mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
+  "is_simulation R C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
+    \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R \<longrightarrow>
+      mk_trace C $ ex = mk_trace A $ ((corresp_ex_simC A R $ ex) s')"
+  supply split_if [split del]
+  apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
+  (* cons case *)
+  apply auto
+  apply (rename_tac ex a t s s')
+  apply (simp add: mk_traceConc)
+  apply (frule reachable.reachable_n)
+  apply assumption
+  apply (erule_tac x = "t" in allE)
+  apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
+  apply (simp add: move_subprop5_sim [unfolded Let_def]
+    move_subprop4_sim [unfolded Let_def] split add: split_if)
+  done
+
+text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
 
-apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
-(* cons case *)
-apply auto
-apply (rename_tac ex a t s s')
-apply (simp add: mk_traceConc)
-apply (frule reachable.reachable_n)
-apply assumption
-apply (erule_tac x = "t" in allE)
-apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
-apply (simp add: move_subprop5_sim [unfolded Let_def]
-  move_subprop4_sim [unfolded Let_def] split add: split_if)
-done
-declare split_if [split]
+lemma correspsim_is_execution [rule_format]:
+  "is_simulation R C A \<Longrightarrow>
+    \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R
+      \<longrightarrow> is_exec_frag A (s', (corresp_ex_simC A R $ ex) s')"
+  apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
+  text \<open>main case\<close>
+  apply auto
+  apply (rename_tac ex a t s s')
+  apply (rule_tac t = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in lemma_2_1)
+
+  text \<open>Finite\<close>
+  apply (erule move_subprop2_sim [unfolded Let_def])
+  apply assumption+
+  apply (rule conjI)
 
+  text \<open>\<open>is_exec_frag\<close>\<close>
+  apply (erule move_subprop1_sim [unfolded Let_def])
+  apply assumption+
+  apply (rule conjI)
 
-(* ----------------------------------------------------------- *)
-(*               Lemma 2 : corresp_ex_sim is execution         *)
-(* ----------------------------------------------------------- *)
+  text \<open>Induction hypothesis\<close>
+  text \<open>\<open>reachable_n\<close> looping, therefore apply it manually\<close>
+  apply (erule_tac x = "t" in allE)
+  apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
+  apply simp
+  apply (frule reachable.reachable_n)
+  apply assumption
+  apply (simp add: move_subprop5_sim [unfolded Let_def])
+  text \<open>laststate\<close>
+  apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
+  apply assumption+
+  done
 
 
-lemma correspsim_is_execution [rule_format (no_asm)]:
- "[| is_simulation R C A |] ==>
-  !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
-  --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
-
-apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
-(* main case *)
-apply auto
-apply (rename_tac ex a t s s')
-apply (rule_tac t = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in lemma_2_1)
-
-(* Finite *)
-apply (erule move_subprop2_sim [unfolded Let_def])
-apply assumption+
-apply (rule conjI)
-
-(* is_exec_frag *)
-apply (erule move_subprop1_sim [unfolded Let_def])
-apply assumption+
-apply (rule conjI)
+subsection \<open>Main Theorem: TRACE - INCLUSION\<close>
 
-(* Induction hypothesis  *)
-(* reachable_n looping, therefore apply it manually *)
-apply (erule_tac x = "t" in allE)
-apply (erule_tac x = "@t'. ? ex1. (t,t') :R & move A ex1 s' a t'" in allE)
-apply simp
-apply (frule reachable.reachable_n)
-apply assumption
-apply (simp add: move_subprop5_sim [unfolded Let_def])
-(* laststate *)
-apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
-apply assumption+
-done
-
-
-subsection "Main Theorem: TRACE - INCLUSION"
-
-(* -------------------------------------------------------------------------------- *)
-
-  (* generate condition (s,S'):R & S':starts_of A, the first being intereting
-     for the induction cases concerning the two lemmas correpsim_is_execution and
-     traces_coincide_sim, the second for the start state case.
-     S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C  *)
+text \<open>
+  Generate condition \<open>(s, S') \<in> R \<and> S' \<in> starts_of A\<close>, the first being
+  interesting for the induction cases concerning the two lemmas
+  \<open>correpsim_is_execution\<close> and \<open>traces_coincide_sim\<close>, the second for the start
+  state case.
+  \<open>S' := SOME s'. (s, s') \<in> R \<and> s' \<in> starts_of A\<close>, where \<open>s \<in> starts_of C\<close>
+\<close>
 
 lemma simulation_starts:
-"[| is_simulation R C A; s:starts_of C |]
-  ==> let S' = @s'. (s,s'):R & s':starts_of A in
-      (s,S'):R & S':starts_of A"
+  "is_simulation R C A \<Longrightarrow> s:starts_of C \<Longrightarrow>
+    let S' = SOME s'. (s, s') \<in> R \<and> s' \<in> starts_of A
+    in (s, S') \<in> R \<and> S' \<in> starts_of A"
   apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
   apply (erule conjE)+
   apply (erule ballE)
-  prefer 2 apply (blast)
+  prefer 2 apply blast
   apply (erule exE)
   apply (rule someI2)
   apply assumption
@@ -253,35 +241,32 @@
 
 
 lemma trace_inclusion_for_simulations:
-  "[| ext C = ext A; is_simulation R C A |]
-           ==> traces C <= traces A"
-
+  "ext C = ext A \<Longrightarrow> is_simulation R C A \<Longrightarrow> traces C \<subseteq> traces A"
   apply (unfold traces_def)
-
-  apply (simp (no_asm) add: has_trace_def2)
+  apply (simp add: has_trace_def2)
   apply auto
 
-  (* give execution of abstract automata *)
+  text \<open>give execution of abstract automata\<close>
   apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
 
-  (* Traces coincide, Lemma 1 *)
+  text \<open>Traces coincide, Lemma 1\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (rename_tac s ex)
-  apply (simp (no_asm) add: corresp_ex_sim_def)
+  apply (simp add: corresp_ex_sim_def)
   apply (rule_tac s = "s" in traces_coincide_sim)
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0 sim_starts1)
 
-  (* corresp_ex_sim is execution, Lemma 2 *)
+  text \<open>\<open>corresp_ex_sim\<close> is execution, Lemma 2\<close>
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   apply (rename_tac s ex)
 
-  (* start state *)
+  text \<open>start state\<close>
   apply (rule conjI)
   apply (simp add: sim_starts2 corresp_ex_sim_def)
 
-  (* is-execution-fragment *)
+  text \<open>\<open>is_execution-fragment\<close>\<close>
   apply (simp add: corresp_ex_sim_def)
   apply (rule_tac s = s in correspsim_is_execution)
   apply assumption
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/Simulations.thy
--- a/src/HOL/HOLCF/IOA/Simulations.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Simulations.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -10,76 +10,51 @@
 
 default_sort type
 
-definition
-  is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_simulation R C A =
-   ((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
-   (!s s' t a. reachable C s &
-               s \<midarrow>a\<midarrow>C\<rightarrow> t   &
-               (s,s') : R
-               --> (? t' ex. (t,t'):R & move A ex s' a t')))"
+definition is_simulation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_simulation R C A \<longleftrightarrow>
+    (\<forall>s \<in> starts_of C. R``{s} \<inter> starts_of A \<noteq> {}) \<and>
+    (\<forall>s s' t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (s, s') \<in> R
+      \<longrightarrow> (\<exists>t' ex. (t, t') \<in> R \<and> move A ex s' a t'))"
 
-definition
-  is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_backward_simulation R C A =
-   ((!s:starts_of C. R``{s} <= starts_of A) &
-   (!s t t' a. reachable C s &
-               s \<midarrow>a\<midarrow>C\<rightarrow> t   &
-               (t,t') : R
-               --> (? ex s'. (s,s'):R & move A ex s' a t')))"
+definition is_backward_simulation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_backward_simulation R C A \<longleftrightarrow>
+    (\<forall>s \<in> starts_of C. R``{s} \<subseteq> starts_of A) \<and>
+    (\<forall>s t t' a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (t, t') \<in> R
+      \<longrightarrow> (\<exists>ex s'. (s,s') \<in> R \<and> move A ex s' a t'))"
 
-definition
-  is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_forw_back_simulation R C A =
-   ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
-   (!s S' t a. reachable C s &
-               s \<midarrow>a\<midarrow>C\<rightarrow> t   &
-               (s,S') : R
-               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
+definition is_forw_back_simulation ::
+    "('s1 \<times> 's2 set) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_forw_back_simulation R C A \<longleftrightarrow>
+    (\<forall>s \<in> starts_of C. \<exists>S'. (s, S') \<in> R \<and> S' \<subseteq> starts_of A) \<and>
+    (\<forall>s S' t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (s, S') \<in> R
+      \<longrightarrow> (\<exists>T'. (t, T') \<in> R \<and> (\<forall>t' \<in> T'. \<exists>s' \<in> S'. \<exists>ex. move A ex s' a t')))"
 
-definition
-  is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_back_forw_simulation R C A =
-   ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
-   (!s t T' a. reachable C s &
-               s \<midarrow>a\<midarrow>C\<rightarrow> t   &
-               (t,T') : R
-               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
+definition is_back_forw_simulation ::
+    "('s1 \<times> 's2 set) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_back_forw_simulation R C A \<longleftrightarrow>
+    ((\<forall>s \<in> starts_of C. \<forall>S'. (s, S') \<in> R \<longrightarrow> S' \<inter> starts_of A \<noteq> {}) \<and>
+    (\<forall>s t T' a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<and> (t, T') \<in> R
+      \<longrightarrow> (\<exists>S'. (s, S') \<in> R \<and> (\<forall>s' \<in> S'. \<exists>t' \<in> T'. \<exists>ex. move A ex s' a t'))))"
 
-definition
-  is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_history_relation R C A = (is_simulation R C A &
-                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
+definition is_history_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_history_relation R C A \<longleftrightarrow>
+    is_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R^-1)) A C"
 
-definition
-  is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
-  "is_prophecy_relation R C A = (is_backward_simulation R C A &
-                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
+definition is_prophecy_relation :: "('s1 \<times> 's2) set \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+  where "is_prophecy_relation R C A \<longleftrightarrow>
+    is_backward_simulation R C A \<and> is_ref_map (\<lambda>x. (SOME y. (x, y) \<in> R^-1)) A C"
 
 
-lemma set_non_empty: "(A~={}) = (? x. x:A)"
-apply auto
-done
+lemma set_non_empty: "A \<noteq> {} \<longleftrightarrow> (\<exists>x. x \<in> A)"
+  by auto
 
-lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)"
-apply (simp add: set_non_empty)
-done
-
+lemma Int_non_empty: "A \<inter> B \<noteq> {} \<longleftrightarrow> (\<exists>x. x \<in> A \<and> x \<in> B)"
+  by (simp add: set_non_empty)
 
-lemma Sim_start_convert:
-"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"
-apply (unfold Image_def)
-apply (simp add: Int_non_empty)
-done
-
-declare Sim_start_convert [simp]
+lemma Sim_start_convert [simp]: "R``{x} \<inter> S \<noteq> {} \<longleftrightarrow> (\<exists>y. (x, y) \<in> R \<and> y \<in> S)"
+  by (simp add: Image_def Int_non_empty)
 
-
-lemma ref_map_is_simulation:
-"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"
-
-apply (unfold is_ref_map_def is_simulation_def)
-apply simp
-done
+lemma ref_map_is_simulation: "is_ref_map f C A \<Longrightarrow> is_simulation {p. snd p = f (fst p)} C A"
+  by (simp add: is_ref_map_def is_simulation_def)
 
 end
diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -34,13 +34,10 @@
   where "xt2 P tr = P (fst (snd tr))"
 
 definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)"
-where
-  "ex2seqC = (fix$(LAM h ex. (%s. case ex of
-      nil =>  (s,None,s)\<leadsto>nil
-    | x##xs => (flift1 (%pr.
-                (s,Some (fst pr), snd pr)\<leadsto> (h$xs) (snd pr))
-                $x)
-      )))"
+  where "ex2seqC =
+    (fix $ (LAM h ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> (s, None, s) \<leadsto> nil
+    | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h $ xs) (snd pr)) $ x))))"
 
 definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
   where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)"
@@ -56,16 +53,9 @@
 
 
 axiomatization
-where
-
-mkfin_UU:
-  "mkfin UU = nil" and
-
-mkfin_nil:
-  "mkfin nil =nil" and
-
-mkfin_cons:
-  "(mkfin (a\<leadsto>s)) = (a\<leadsto>(mkfin s))"
+where mkfin_UU [simp]: "mkfin UU = nil"
+  and mkfin_nil [simp]: "mkfin nil = nil"
+  and mkfin_cons [simp]: "mkfin (a \<leadsto> s) = a \<leadsto> mkfin s"
 
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
@@ -75,12 +65,12 @@
 
 subsection \<open>ex2seqC\<close>
 
-lemma ex2seqC_unfold: "ex2seqC  = (LAM ex. (%s. case ex of
-       nil =>  (s,None,s)\<leadsto>nil
-     | x##xs => (flift1 (%pr.
-                 (s,Some (fst pr), snd pr)\<leadsto> (ex2seqC$xs) (snd pr))
-                 $x)
-       ))"
+lemma ex2seqC_unfold:
+  "ex2seqC =
+    (LAM ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> (s, None, s) \<leadsto> nil
+    | x ## xs \<Rightarrow>
+        (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC $ xs) (snd pr)) $ x)))"
   apply (rule trans)
   apply (rule fix_eq4)
   apply (rule ex2seqC_def)
@@ -88,43 +78,38 @@
   apply (simp add: flift1_def)
   done
 
-lemma ex2seqC_UU: "(ex2seqC $UU) s=UU"
+lemma ex2seqC_UU [simp]: "(ex2seqC $ UU) s = UU"
   apply (subst ex2seqC_unfold)
   apply simp
   done
 
-lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)\<leadsto>nil"
+lemma ex2seqC_nil [simp]: "(ex2seqC $ nil) s = (s, None, s) \<leadsto> nil"
   apply (subst ex2seqC_unfold)
   apply simp
   done
 
-lemma ex2seqC_cons: "(ex2seqC $((a,t)\<leadsto>xs)) s = (s,Some a,t)\<leadsto> ((ex2seqC$xs) t)"
+lemma ex2seqC_cons [simp]: "(ex2seqC $ ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC $ xs) t"
   apply (rule trans)
   apply (subst ex2seqC_unfold)
   apply (simp add: Consq_def flift1_def)
   apply (simp add: Consq_def flift1_def)
   done
 
-declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp]
 
-
-
-declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp]
-
-lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)\<leadsto>nil"
+lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \<leadsto> nil"
   by (simp add: ex2seq_def)
 
-lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)\<leadsto>nil"
+lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \<leadsto> nil"
   by (simp add: ex2seq_def)
 
-lemma ex2seq_cons: "ex2seq (s, (a,t)\<leadsto>ex) = (s,Some a,t) \<leadsto> ex2seq (t, ex)"
+lemma ex2seq_cons: "ex2seq (s, (a, t) \<leadsto> ex) = (s, Some a, t) \<leadsto> ex2seq (t, ex)"
   by (simp add: ex2seq_def)
 
 declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
 declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
 
 
-lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
+lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil"
   apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
@@ -137,21 +122,20 @@
    after the translation via ex2seq !! *)
 
 lemma TL_TLS:
-  "[| ! s a t. (P s) & s \<midarrow>a\<midarrow>A\<rightarrow> t --> (Q t) |]
-    ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
-              \<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
+  "\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t)
+    \<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
+              \<^bold>\<longrightarrow> (Next (Init (\<lambda>(s, a, t). Q s))))"
   apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
-
   apply clarify
   apply (simp split add: split_if)
-  (* TL = UU *)
+  text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  (* TL = nil *)
+  text \<open>\<open>TL = nil\<close>\<close>
   apply (rule conjI)
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
@@ -163,9 +147,8 @@
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  (* TL =cons *)
+  text \<open>\<open>TL = cons\<close>\<close>
   apply (simp add: unlift_def)
-
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)