src/HOL/TLA/Init.thy

--- a/src/HOL/TLA/Init.thy	Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Init.thy	Fri Jun 26 14:53:15 2015 +0200
@@ -18,22 +18,22 @@
 
 
 consts
-  Initial     :: "('w::world => bool) => temporal"
-  first_world :: "behavior => ('w::world)"
-  st1         :: "behavior => state"
-  st2         :: "behavior => state"
+  Initial     :: "('w::world \<Rightarrow> bool) \<Rightarrow> temporal"
+  first_world :: "behavior \<Rightarrow> ('w::world)"
+  st1         :: "behavior \<Rightarrow> state"
+  st2         :: "behavior \<Rightarrow> state"
 
 syntax
-  "_TEMP"    :: "lift => 'a"                          ("(TEMP _)")
-  "_Init"    :: "lift => lift"                        ("(Init _)"[40] 50)
+  "_TEMP"    :: "lift \<Rightarrow> 'a"                          ("(TEMP _)")
+  "_Init"    :: "lift \<Rightarrow> lift"                        ("(Init _)"[40] 50)
 
 translations
-  "TEMP F"   => "(F::behavior => _)"
+  "TEMP F"   => "(F::behavior \<Rightarrow> _)"
   "_Init"    == "CONST Initial"
   "sigma |= Init F"  <= "_Init F sigma"
 
 defs
-  Init_def:    "sigma |= Init F  ==  (first_world sigma) |= F"
+  Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
 
 defs (overloaded)
   fw_temp_def: "first_world == \<lambda>sigma. sigma"
@@ -41,37 +41,37 @@
   fw_act_def:  "first_world == \<lambda>sigma. (st1 sigma, st2 sigma)"
 
 lemma const_simps [int_rewrite, simp]:
-  "|- (Init #True) = #True"
-  "|- (Init #False) = #False"
+  "\<turnstile> (Init #True) = #True"
+  "\<turnstile> (Init #False) = #False"
   by (auto simp: Init_def)
 
 lemma Init_simps1 [int_rewrite]:
-  "\<And>F. |- (Init \<not>F) = (\<not> Init F)"
-  "|- (Init (P --> Q)) = (Init P --> Init Q)"
-  "|- (Init (P & Q)) = (Init P & Init Q)"
-  "|- (Init (P | Q)) = (Init P | Init Q)"
-  "|- (Init (P = Q)) = ((Init P) = (Init Q))"
-  "|- (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
-  "|- (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
-  "|- (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
+  "\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
+  "\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
+  "\<turnstile> (Init (P & Q)) = (Init P & Init Q)"
+  "\<turnstile> (Init (P | Q)) = (Init P | Init Q)"
+  "\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))"
+  "\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
+  "\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
+  "\<turnstile> (Init (\<exists>!x. F x)) = (\<exists>!x. (Init F x))"
   by (auto simp: Init_def)
 
-lemma Init_stp_act: "|- (Init $P) = (Init P)"
+lemma Init_stp_act: "\<turnstile> (Init $P) = (Init P)"
   by (auto simp add: Init_def fw_act_def fw_stp_def)
 
 lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
 lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
 
-lemma Init_temp: "|- (Init F) = F"
+lemma Init_temp: "\<turnstile> (Init F) = F"
   by (auto simp add: Init_def fw_temp_def)
 
 lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
 
 (* Trivial instances of the definitions that avoid introducing lambda expressions. *)
-lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
+lemma Init_stp: "(sigma \<Turnstile> Init P) = P (st1 sigma)"
   by (simp add: Init_def fw_stp_def)
 
-lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
+lemma Init_act: "(sigma \<Turnstile> Init A) = A (st1 sigma, st2 sigma)"
   by (simp add: Init_def fw_act_def)
 
 lemmas Init_defs = Init_stp Init_act Init_temp [int_use]