--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:52:00 2015 +0100
@@ -30,17 +30,17 @@
"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 |== Q) --> (ex |== P))"
+ "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 (.~ Q) (.~ P) h"
+ "temp_weakening Q P h = 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 (.~Q) (.~P) h"
+ "state_weakening Q P h = state_strengthening (\<^bold>\<not>Q) (\<^bold>\<not>P) h"
definition
is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
@@ -83,7 +83,7 @@
subsection "lemmas"
-lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"
+lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex \<TTurnstile> P) --> (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
@@ -131,16 +131,16 @@
(* FIX: Nach TLS.ML *)
-lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))"
+lemma IMPLIES_temp_sat: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) = ((ex \<TTurnstile> P) --> (ex \<TTurnstile> Q))"
by (simp add: IMPLIES_def temp_sat_def satisfies_def)
-lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))"
+lemma AND_temp_sat: "(ex \<TTurnstile> P \<^bold>\<and> Q) = ((ex \<TTurnstile> P) & (ex \<TTurnstile> Q))"
by (simp add: AND_def temp_sat_def satisfies_def)
-lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))"
+lemma OR_temp_sat: "(ex \<TTurnstile> P \<^bold>\<or> Q) = ((ex \<TTurnstile> P) | (ex \<TTurnstile> Q))"
by (simp add: OR_def temp_sat_def satisfies_def)
-lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))"
+lemma NOT_temp_sat: "(ex \<TTurnstile> \<^bold>\<not> P) = (~ (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]
@@ -160,7 +160,7 @@
lemma AbsRuleTImprove:
"[|is_live_abstraction h (C,L) (A,M);
- validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h;
+ 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)
@@ -287,7 +287,7 @@
lemma strength_AND:
"[| temp_strengthening P1 Q1 h;
temp_strengthening P2 Q2 h |]
- ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"
+ ==> temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
apply (unfold temp_strengthening_def)
apply auto
done
@@ -295,14 +295,14 @@
lemma strength_OR:
"[| temp_strengthening P1 Q1 h;
temp_strengthening P2 Q2 h |]
- ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"
+ ==> temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
apply (unfold temp_strengthening_def)
apply auto
done
lemma strength_NOT:
"[| temp_weakening P Q h |]
- ==> temp_strengthening (.~ 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
@@ -311,7 +311,7 @@
lemma strength_IMPLIES:
"[| temp_weakening P1 Q1 h;
temp_strengthening P2 Q2 h |]
- ==> temp_strengthening (P1 .--> P2) (Q1 .--> 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
@@ -320,20 +320,20 @@
lemma weak_AND:
"[| temp_weakening P1 Q1 h;
temp_weakening P2 Q2 h |]
- ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"
+ ==> temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
apply (simp add: temp_weakening_def2)
done
lemma weak_OR:
"[| temp_weakening P1 Q1 h;
temp_weakening P2 Q2 h |]
- ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"
+ ==> temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
apply (simp add: temp_weakening_def2)
done
lemma weak_NOT:
"[| temp_strengthening P Q h |]
- ==> temp_weakening (.~ 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
@@ -342,7 +342,7 @@
lemma weak_IMPLIES:
"[| temp_strengthening P1 Q1 h;
temp_weakening P2 Q2 h |]
- ==> temp_weakening (P1 .--> P2) (Q1 .--> 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
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:52:00 2015 +0100
@@ -15,18 +15,18 @@
definition
validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where
- "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
+ "validLIOA AL P = 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><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+ "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
definition
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
- "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+ "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
definition
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
- "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
+ "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}"
@@ -39,8 +39,8 @@
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 |== (snd CL)) -->
- ((corresp_ex (fst AM) f exec) |== (snd AM))))"
+ (! exec : executions (fst CL). (exec \<TTurnstile> (snd CL)) -->
+ ((corresp_ex (fst AM) f exec) \<TTurnstile> (snd AM))))"
lemma live_implements_trans:
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Wed Dec 30 21:52:00 2015 +0100
@@ -15,50 +15,33 @@
consts
-satisfies ::"'a => 'a predicate => bool" ("_ |= _" [100,9] 8)
+satisfies ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
valid ::"'a predicate => bool" (* ("|-") *)
-NOT ::"'a predicate => 'a predicate" (".~ _" [40] 40)
-AND ::"'a predicate => 'a predicate => 'a predicate" (infixr ".&" 35)
-OR ::"'a predicate => 'a predicate => 'a predicate" (infixr ".|" 30)
-IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25)
-
-
-notation (output)
- NOT ("~ _" [40] 40) and
- AND (infixr "&" 35) and
- OR (infixr "|" 30) and
- IMPLIES (infixr "-->" 25)
-
-notation (xsymbols output)
- NOT ("\<not> _" [40] 40) and
- AND (infixr "\<and>" 35) and
- OR (infixr "\<or>" 30) and
- IMPLIES (infixr "\<longrightarrow>" 25)
-
-notation (xsymbols)
- satisfies ("_ \<Turnstile> _" [100,9] 8)
+NOT ::"'a predicate => 'a predicate" ("\<^bold>\<not> _" [40] 40)
+AND ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<and>" 35)
+OR ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<or>" 30)
+IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25)
defs
satisfies_def:
- "s |= P == P s"
+ "s \<Turnstile> P == P s"
-(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
valid_def:
- "valid P == (! s. (s |= P))"
+ "valid P == (! s. (s \<Turnstile> P))"
NOT_def:
"NOT P s == ~ (P s)"
AND_def:
- "(P .& Q) s == (P s) & (Q s)"
+ "(P \<^bold>\<and> Q) s == (P s) & (Q s)"
OR_def:
- "(P .| Q) s == (P s) | (Q s)"
+ "(P \<^bold>\<or> Q) s == (P s) | (Q s)"
IMPLIES_def:
- "(P .--> Q) s == (P s) --> (Q s)"
+ "(P \<^bold>\<longrightarrow> Q) s == (P s) --> (Q s)"
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:52:00 2015 +0100
@@ -792,7 +792,7 @@
lemma divide_Seq_lemma:
"HD$(Filter P$y) = Def x
- --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
+ --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a. ~P a)$y)))
& Finite (Takewhile (%x. ~ P x)$y) & P x"
(* FIX: pay attention: is only admissible with chain-finite package to be added to
@@ -809,7 +809,7 @@
done
lemma divide_Seq: "(x>>xs) << Filter P$y
- ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
+ ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a. ~ P a)$y)))
& Finite (Takewhile (%a. ~ P a)$y) & P x"
apply (rule divide_Seq_lemma [THEN mp])
apply (drule_tac f="HD" and x="x>>xs" in monofun_cfun_arg)
@@ -1030,7 +1030,7 @@
(* 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
+lemma Filter_lemma1: "Forall (%x. ~(P x & Q x)) s
--> Filter P$(Filter Q$s) =
Filter (%x. P x & Q x)$s"
@@ -1054,7 +1054,7 @@
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
+ Q1="%x. ~(P x & Q x)" and x1="s" in
take_lemma_induct [THEN mp])
(* better support for A = %x. True *)
apply (simp add: Filter_lemma1)
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:52:00 2015 +0100
@@ -20,8 +20,8 @@
| x##xs =>
(case x of
UU => UU
- | Def y => (Takewhile (%x.~P x)$s)
- @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
+ | Def y => (Takewhile (%x. \<not>P x)$s)
+ @@ (y>>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
)
))"
@@ -64,8 +64,8 @@
| x##xs =>
(case x of
UU => UU
- | Def y => (Takewhile (%a.~ P a)$s)
- @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))
+ | Def y => (Takewhile (%a. \<not> P a)$s)
+ @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs))
)
)"
apply (rule trans)
@@ -86,8 +86,8 @@
done
lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
- (Takewhile (%a.~ P a)$s)
- @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"
+ (Takewhile (%a. \<not> P a)$s)
+ @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))"
apply (rule trans)
apply (subst oraclebuild_unfold)
apply (simp add: Consq_def)
@@ -98,7 +98,7 @@
subsection "Cut rewrite rules"
lemma Cut_nil:
-"[| Forall (%a.~ P a) s; Finite s|]
+"[| Forall (%a. \<not> P a) s; Finite s|]
==> Cut P s =nil"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P$s = nil")
@@ -108,7 +108,7 @@
done
lemma Cut_UU:
-"[| Forall (%a.~ P a) s; ~Finite s|]
+"[| Forall (%a. \<not> P a) s; ~Finite s|]
==> Cut P s =UU"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P$s= UU")
@@ -118,7 +118,7 @@
done
lemma Cut_Cons:
-"[| P t; Forall (%x.~ P x) ss; Finite ss|]
+"[| P t; Forall (%x. \<not> P x) ss; Finite ss|]
==> Cut P (ss @@ (t>> rs))
= ss @@ (t >> Cut P rs)"
apply (unfold Cut_def)
@@ -129,7 +129,7 @@
subsection "Cut lemmas for main theorem"
lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in take_lemma_induct [THEN mp])
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
prefer 3 apply (fast)
apply (case_tac "Finite s")
apply (simp add: Cut_nil ForallQFilterPnil)
@@ -140,7 +140,7 @@
lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in
take_lemma_less_induct [THEN mp])
prefer 3 apply (fast)
apply (case_tac "Finite s")
@@ -154,7 +154,7 @@
lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P (f x) " and x1 = "s" in
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P (f x) " and x1 = "s" in
take_lemma_less_induct [THEN mp])
prefer 3 apply (fast)
apply (case_tac "Finite s")
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:52:00 2015 +0100
@@ -24,8 +24,8 @@
Init :: "'a predicate => 'a temporal" ("<_>" [0] 1000)
-Box :: "'a temporal => 'a temporal" ("\<box> (_)" [80] 80)
-Diamond :: "'a temporal => 'a temporal" ("\<diamond> (_)" [80] 80)
+Box :: "'a temporal => 'a temporal" ("\<box>(_)" [80] 80)
+Diamond :: "'a temporal => 'a temporal" ("\<diamond>(_)" [80] 80)
Next :: "'a temporal => 'a temporal"
Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 22)
@@ -51,25 +51,25 @@
"(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
Diamond_def:
- "\<diamond>P == .~ (\<box>(.~ P))"
+ "\<diamond>P == \<^bold>\<not> (\<box>(\<^bold>\<not> P))"
Leadsto_def:
- "P \<leadsto> Q == (\<box>(P .--> (\<diamond>Q)))"
+ "P \<leadsto> Q == (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
validT_def:
- "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
+ "validT P == ! s. s~=UU & s~=nil --> (s \<Turnstile> P)"
-lemma simple: "\<box>\<diamond>(.~ P) = (.~ \<diamond>\<box>P)"
+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
-lemma Boxnil: "nil |= \<box>P"
+lemma Boxnil: "nil \<Turnstile> \<box>P"
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
done
-lemma Diamondnil: "~(nil |= \<diamond>P)"
+lemma Diamondnil: "~(nil \<Turnstile> \<diamond>P)"
apply (simp add: Diamond_def satisfies_def NOT_def)
apply (cut_tac Boxnil)
apply (simp add: satisfies_def)
@@ -89,7 +89,7 @@
apply auto
done
-lemma reflT: "s~=UU & s~=nil --> (s |= \<box>F .--> F)"
+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)
@@ -105,7 +105,7 @@
apply (simp (no_asm) add: Conc_assoc)
done
-lemma transT: "s |= \<box>F .--> \<box>\<box>F"
+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)
@@ -115,7 +115,7 @@
done
-lemma normalT: "s |= \<box>(F .--> G) .--> \<box>F .--> \<box>G"
+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
@@ -136,7 +136,7 @@
done
(* Note that unlift and HD is not at all used !!! *)
-lemma STL4: "valid (P .--> Q) ==> validT (\<box>(Init P) .--> \<box>(Init Q))"
+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
@@ -156,13 +156,13 @@
declare split_if [split del]
lemma LTL1:
- "s~=UU & s~=nil --> (s |= \<box>F .--> (F .& (Next (\<box>F))))"
+ "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 .--> F *)
+(* \<box>F \<^bold>\<longrightarrow> F *)
apply (erule_tac x = "s" in allE)
apply (simp add: tsuffix_def suffix_refl)
-(* \<box>F .--> Next \<box>F *)
+(* \<box>F \<^bold>\<longrightarrow> Next \<box>F *)
apply (simp split add: split_if)
apply auto
apply (drule tsuffix_TL2)
@@ -173,25 +173,25 @@
lemma LTL2a:
- "s |= .~ (Next F) .--> (Next (.~ F))"
+ "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 LTL2b:
- "s |= (Next (.~ F)) .--> (.~ (Next F))"
+ "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 |= (Next (F .--> G)) .--> (Next F) .--> (Next G)"
+"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 .--> Q); validT P |] ==> validT Q"
+lemma ModusPonens: "[| validT (P \<^bold>\<longrightarrow> Q); validT P |] ==> validT Q"
apply (simp add: validT_def satisfies_def IMPLIES_def)
done
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:52:00 2015 +0100
@@ -24,7 +24,7 @@
option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
plift :: "('a => bool) => ('a option => bool)"
-temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "|==" 22)
+temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "\<TTurnstile>" 22)
xt1 :: "'s predicate => ('a,'s)step_pred"
xt2 :: "'a option predicate => ('a,'s)step_pred"
@@ -52,7 +52,7 @@
"plift P == option_lift P False"
temp_sat_def:
- "ex |== P == ((ex2seq ex) |= P)"
+ "ex \<TTurnstile> P == ((ex2seq ex) \<Turnstile> P)"
xt1_def:
"xt1 P tr == P (fst tr)"
@@ -72,10 +72,10 @@
)))"
validTE_def:
- "validTE P == ! ex. (ex |== P)"
+ "validTE P == ! ex. (ex \<TTurnstile> P)"
validIOA_def:
- "validIOA A P == ! ex : executions A . (ex |== P)"
+ "validIOA A P == ! ex : executions A . (ex \<TTurnstile> P)"
axiomatization where
@@ -164,8 +164,8 @@
lemma TL_TLS:
"[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]
- ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t)
- .--> (Next (Init (%(s,a,t).Q s))))"
+ ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s -a--A-> t)
+ \<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
apply clarify
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:52:00 2015 +0100
@@ -155,7 +155,7 @@
is_wfair_def:
"is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
- | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
+ | inf_often (%x. ~ Enabled A W (snd x)) (snd ex))"
sfair_ex_def:
"sfair_ex A ex == ! W : sfair_of A.