--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:35:21 2015 +0100
@@ -22,17 +22,12 @@
unlift :: "'a lift => 'a"
-Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000)
+Init :: "'a predicate => 'a temporal" ("<_>" [0] 1000)
-Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80)
-Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80)
-Next ::"'a temporal => 'a temporal"
-Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22)
-
-notation (xsymbols)
- Box ("\<box> (_)" [80] 80) and
- Diamond ("\<diamond> (_)" [80] 80) and
- Leadsto (infixr "\<leadsto>" 22)
+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)
defs
@@ -50,37 +45,37 @@
"tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
Box_def:
- "([] P) s == ! s2. tsuffix s2 s --> P s2"
+ "(\<box>P) s == ! s2. tsuffix s2 s --> P s2"
Next_def:
"(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
Diamond_def:
- "<> P == .~ ([] (.~ P))"
+ "\<diamond>P == .~ (\<box>(.~ P))"
Leadsto_def:
- "P ~> Q == ([] (P .--> (<> Q)))"
+ "P \<leadsto> Q == (\<box>(P .--> (\<diamond>Q)))"
validT_def:
"validT P == ! s. s~=UU & s~=nil --> (s |= P)"
-lemma simple: "[] <> (.~ P) = (.~ <> [] P)"
+lemma simple: "\<box>\<diamond>(.~ P) = (.~ \<diamond>\<box>P)"
apply (rule ext)
apply (simp add: Diamond_def NOT_def Box_def)
done
-lemma Boxnil: "nil |= [] P"
+lemma Boxnil: "nil |= \<box>P"
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
done
-lemma Diamondnil: "~(nil |= <> P)"
+lemma Diamondnil: "~(nil |= \<diamond>P)"
apply (simp add: Diamond_def satisfies_def NOT_def)
apply (cut_tac Boxnil)
apply (simp add: satisfies_def)
done
-lemma Diamond_def2: "(<> F) s = (? s2. tsuffix s2 s & F s2)"
+lemma Diamond_def2: "(\<diamond>F) s = (? s2. tsuffix s2 s & F s2)"
apply (simp add: Diamond_def NOT_def Box_def)
done
@@ -94,7 +89,7 @@
apply auto
done
-lemma reflT: "s~=UU & s~=nil --> (s |= [] F .--> F)"
+lemma reflT: "s~=UU & s~=nil --> (s |= \<box>F .--> F)"
apply (simp add: satisfies_def IMPLIES_def Box_def)
apply (rule impI)+
apply (erule_tac x = "s" in allE)
@@ -110,7 +105,7 @@
apply (simp (no_asm) add: Conc_assoc)
done
-lemma transT: "s |= [] F .--> [] [] F"
+lemma transT: "s |= \<box>F .--> \<box>\<box>F"
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)
apply auto
apply (drule suffix_trans)
@@ -120,14 +115,14 @@
done
-lemma normalT: "s |= [] (F .--> G) .--> [] F .--> [] G"
+lemma normalT: "s |= \<box>(F .--> G) .--> \<box>F .--> \<box>G"
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)
done
subsection "TLA Rules by Lamport"
-lemma STL1a: "validT P ==> validT ([] P)"
+lemma STL1a: "validT P ==> validT (\<box>P)"
apply (simp add: validT_def satisfies_def Box_def tsuffix_def)
done
@@ -135,13 +130,13 @@
apply (simp add: valid_def validT_def satisfies_def Init_def)
done
-lemma STL1: "valid P ==> validT ([] (Init P))"
+lemma STL1: "valid P ==> validT (\<box>(Init P))"
apply (rule STL1a)
apply (erule STL1b)
done
(* Note that unlift and HD is not at all used !!! *)
-lemma STL4: "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))"
+lemma STL4: "valid (P .--> Q) ==> validT (\<box>(Init P) .--> \<box>(Init Q))"
apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
done
@@ -161,13 +156,13 @@
declare split_if [split del]
lemma LTL1:
- "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))"
+ "s~=UU & s~=nil --> (s |= \<box>F .--> (F .& (Next (\<box>F))))"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
apply auto
-(* []F .--> F *)
+(* \<box>F .--> F *)
apply (erule_tac x = "s" in allE)
apply (simp add: tsuffix_def suffix_refl)
-(* []F .--> Next [] F *)
+(* \<box>F .--> Next \<box>F *)
apply (simp split add: split_if)
apply auto
apply (drule tsuffix_TL2)