# HG changeset patch
# User wenzelm
# Date 1452983488 -3600
# Node ID 0826f6b6ba092007c088c9be1ec00ccbc4ad182f
# Parent  bdaa0eb0fc7420ef07ddd1f1a182550fd57ea8fc
tuned;

diff -r bdaa0eb0fc74 -r 0826f6b6ba09 src/HOL/HOLCF/IOA/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Jan 16 23:24:50 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Jan 16 23:31:28 2016 +0100
@@ -114,21 +114,6 @@
   done
 
 
-(* FIXME: to TLS.thy *)
-
-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 [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 [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 [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))"
-  by (simp add: NOT_def temp_sat_def satisfies_def)
-
-
 lemma AbsRuleT2:
   "is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A, M) Q \<Longrightarrow> temp_strengthening Q P h
     \<Longrightarrow> validLIOA (C, L) P"
@@ -217,11 +202,6 @@
    apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   done
 
-(* FIXME: to Traces.thy *)
-
-lemma implements_trans: "A =<| B \<Longrightarrow> B =<| C \<Longrightarrow> A =<| C"
-  by (auto simp add: ioa_implements_def)
-
 
 subsection \<open>Abstraction Rules for Automata\<close>
 
@@ -328,15 +308,6 @@
   done
 
 
-(* FIXME: to Sequence.thy *)
-
-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 \<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,
   properties carry over *)
 lemma cex_absSeq_tsuffix: "tsuffix s t \<Longrightarrow> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
@@ -390,10 +361,6 @@
   apply (tactic \<open>pair_tac @{context} "a" 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)"
diff -r bdaa0eb0fc74 -r 0826f6b6ba09 src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Sat Jan 16 23:24:50 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Sat Jan 16 23:31:28 2016 +0100
@@ -995,4 +995,13 @@
   THEN simp_tac (ctxt addsimps rws) i;
 \<close>
 
+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 \<longleftrightarrow> s = UU"
+  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+
+lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)"
+  by (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
+
 end
diff -r bdaa0eb0fc74 -r 0826f6b6ba09 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 23:24:50 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 23:31:28 2016 +0100
@@ -52,6 +52,19 @@
   where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))"
 
 
+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 [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 [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 [simp]: "(ex \<TTurnstile> \<^bold>\<not> P) \<longleftrightarrow> (\<not> (ex \<TTurnstile> P))"
+  by (simp add: NOT_def temp_sat_def satisfies_def)
+
+
 axiomatization
 where mkfin_UU [simp]: "mkfin UU = nil"
   and mkfin_nil [simp]: "mkfin nil = nil"
diff -r bdaa0eb0fc74 -r 0826f6b6ba09 src/HOL/HOLCF/IOA/Traces.thy
--- a/src/HOL/HOLCF/IOA/Traces.thy	Sat Jan 16 23:24:50 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Traces.thy	Sat Jan 16 23:31:28 2016 +0100
@@ -139,6 +139,9 @@
   where "fair_implements C A \<longleftrightarrow>
     inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A"
 
+lemma implements_trans: "A =<| B \<Longrightarrow> B =<| C \<Longrightarrow> A =<| C"
+  by (auto simp add: ioa_implements_def)
+
 
 subsection \<open>Modules\<close>