src/ZF/UNITY/FP.thy

--- a/src/ZF/UNITY/FP.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/UNITY/FP.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -13,11 +13,11 @@
 
 definition   
   FP_Orig :: "i=>i"  where
-    "FP_Orig(F) == \<Union>({A \<in> Pow(state). \<forall>B. F \<in> stable(A \<inter> B)})"
+    "FP_Orig(F) \<equiv> \<Union>({A \<in> Pow(state). \<forall>B. F \<in> stable(A \<inter> B)})"
 
 definition
   FP :: "i=>i"  where
-    "FP(F) == {s\<in>state. F \<in> stable({s})}"
+    "FP(F) \<equiv> {s\<in>state. F \<in> stable({s})}"
 
 
 lemma FP_Orig_type: "FP_Orig(F) \<subseteq> state"
@@ -36,18 +36,18 @@
 apply (rule FP_type)
 done
 
-lemma stable_FP_Orig_Int: "F \<in> program ==> F \<in> stable(FP_Orig(F) \<inter> B)"
+lemma stable_FP_Orig_Int: "F \<in> program \<Longrightarrow> F \<in> stable(FP_Orig(F) \<inter> B)"
 apply (simp only: FP_Orig_def stable_def Int_Union2)
 apply (blast intro: constrains_UN)
 done
 
 lemma FP_Orig_weakest2: 
-    "[| \<forall>B. F \<in> stable (A \<inter> B); st_set(A) |]  ==> A \<subseteq> FP_Orig(F)"
+    "\<lbrakk>\<forall>B. F \<in> stable (A \<inter> B); st_set(A)\<rbrakk>  \<Longrightarrow> A \<subseteq> FP_Orig(F)"
 by (unfold FP_Orig_def stable_def st_set_def, blast)
 
 lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2]
 
-lemma stable_FP_Int: "F \<in> program ==> F \<in> stable (FP(F) \<inter> B)"
+lemma stable_FP_Int: "F \<in> program \<Longrightarrow> F \<in> stable (FP(F) \<inter> B)"
 apply (subgoal_tac "FP (F) \<inter> B = (\<Union>x\<in>B. FP (F) \<inter> {x}) ")
  prefer 2 apply blast
 apply (simp (no_asm_simp) add: Int_cons_right)
@@ -56,10 +56,10 @@
 apply (auto simp add: cons_absorb)
 done
 
-lemma FP_subset_FP_Orig: "F \<in> program ==> FP(F) \<subseteq> FP_Orig(F)"
+lemma FP_subset_FP_Orig: "F \<in> program \<Longrightarrow> FP(F) \<subseteq> FP_Orig(F)"
 by (rule stable_FP_Int [THEN FP_Orig_weakest], auto)
 
-lemma FP_Orig_subset_FP: "F \<in> program ==> FP_Orig(F) \<subseteq> FP(F)"
+lemma FP_Orig_subset_FP: "F \<in> program \<Longrightarrow> FP_Orig(F) \<subseteq> FP(F)"
 apply (unfold FP_Orig_def FP_def, clarify)
 apply (drule_tac x = "{x}" in spec)
 apply (simp add: Int_cons_right)
@@ -67,17 +67,17 @@
 apply (auto simp add: cons_absorb st_set_def)
 done
 
-lemma FP_equivalence: "F \<in> program ==> FP(F) = FP_Orig(F)"
+lemma FP_equivalence: "F \<in> program \<Longrightarrow> FP(F) = FP_Orig(F)"
 by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig)
 
 lemma FP_weakest [rule_format]:
-     "[| \<forall>B. F \<in> stable(A \<inter> B); F \<in> program; st_set(A) |] ==> A \<subseteq> FP(F)"
+     "\<lbrakk>\<forall>B. F \<in> stable(A \<inter> B); F \<in> program; st_set(A)\<rbrakk> \<Longrightarrow> A \<subseteq> FP(F)"
 by (simp add: FP_equivalence FP_Orig_weakest)
 
 
 lemma Diff_FP: 
-     "[| F \<in> program;  st_set(A) |] 
-      ==> A-FP(F) = (\<Union>act \<in> Acts(F). A - {s \<in> state. act``{s} \<subseteq> {s}})"
+     "\<lbrakk>F \<in> program;  st_set(A)\<rbrakk> 
+      \<Longrightarrow> A-FP(F) = (\<Union>act \<in> Acts(F). A - {s \<in> state. act``{s} \<subseteq> {s}})"
 by (unfold FP_def stable_def constrains_def st_set_def, blast)
 
 end