# HG changeset patch
# User wenzelm
# Date 1456603783 -3600
# Node ID e5e38e1f2dd4c844abe86051b5954fd6d942e064
# Parent  31fa592761da3fae04e8fc6955797bf1a0c139ca
more symbols;

diff -r 31fa592761da -r e5e38e1f2dd4 src/HOL/HOLCF/IOA/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Feb 27 21:04:13 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Feb 27 21:09:43 2016 +0100
@@ -53,7 +53,7 @@
 
 (* analog to the proved thm strength_Next - proof skipped as trivial *)
 axiomatization where
-  weak_Next: "temp_weakening P Q h \<Longrightarrow> temp_weakening (Next P) (Next Q) h"
+  weak_Next: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<circle>P) (\<circle>Q) h"
 
 
 subsection \<open>\<open>cex_abs\<close>\<close>
@@ -382,7 +382,7 @@
   apply (pair a)
   done
 
-lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (Next P) (Next Q) h"
+lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<circle>P) (\<circle>Q) h"
   apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
   apply simp
   apply auto
diff -r 31fa592761da -r e5e38e1f2dd4 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Sat Feb 27 21:04:13 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy	Sat Feb 27 21:09:43 2016 +0100
@@ -22,8 +22,8 @@
   where "Init P s = P (unlift (HD $ s))"
     \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
 
-definition Next :: "'a temporal \<Rightarrow> 'a temporal"
-  where "(Next P) s \<longleftrightarrow> (if TL $ s = UU \<or> TL $ s = nil then P s else P (TL $ s))"
+definition Next :: "'a temporal \<Rightarrow> 'a temporal"  ("\<circle>(_)" [80] 80)
+  where "(\<circle>P) s \<longleftrightarrow> (if TL $ s = UU \<or> TL $ s = nil then P s else P (TL $ s))"
 
 definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
   where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)"
@@ -120,14 +120,14 @@
 
 lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
 
-lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
+lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (\<circle>(\<box>F))))"
   supply if_split [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>
+  text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
   apply (simp split add: if_split)
   apply auto
   apply (drule tsuffix_TL2)
@@ -135,13 +135,13 @@
   apply auto
   done
 
-lemma LTL2a: "s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
+lemma LTL2a: "s \<Turnstile> \<^bold>\<not> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>(\<^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))"
+lemma LTL2b: "s \<Turnstile> (\<circle>(\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (\<circle>F))"
   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)"
+lemma LTL3: "ex \<Turnstile> (\<circle>(F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (\<circle>F) \<^bold>\<longrightarrow> (\<circle>G)"
   by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
 
 lemma ModusPonens: "\<^bold>\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> Q"
diff -r 31fa592761da -r e5e38e1f2dd4 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Sat Feb 27 21:04:13 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Sat Feb 27 21:09:43 2016 +0100
@@ -137,7 +137,7 @@
 lemma TL_TLS:
   "\<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))))"
+              \<^bold>\<longrightarrow> (\<circle>(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: if_split)