src/ZF/UNITY/Guar.thy

 
   (*Existential and Universal properties.  We formalize the two-program
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
 definition
-   ex_prop :: "i => o"  where
+   ex_prop :: "i \<Rightarrow> o"  where
    "ex_prop(X) \<equiv> X<=program \<and>
     (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X)"
 
 definition
-  strict_ex_prop  :: "i => o"  where
+  strict_ex_prop  :: "i \<Rightarrow> o"  where
   "strict_ex_prop(X) \<equiv> X<=program \<and>
    (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X))"
 
 definition
-  uv_prop  :: "i => o"  where
+  uv_prop  :: "i \<Rightarrow> o"  where
    "uv_prop(X) \<equiv> X<=program \<and>
     (SKIP \<in> X \<and> (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X \<and> G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X))"
   
 definition
- strict_uv_prop  :: "i => o"  where
+ strict_uv_prop  :: "i \<Rightarrow> o"  where
    "strict_uv_prop(X) \<equiv> X<=program \<and>
     (SKIP \<in> X \<and> (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X \<and> G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"
 
 definition
-  guar :: "[i, i] => i" (infixl \<open>guarantees\<close> 55)  where
+  guar :: "[i, i] \<Rightarrow> i" (infixl \<open>guarantees\<close> 55)  where
               (*higher than membership, lower than Co*)
   "X guarantees Y \<equiv> {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X \<longrightarrow> F \<squnion> G \<in> Y}"
   
 definition
   (* Weakest guarantees *)
-   wg :: "[i,i] => i"  where
+   wg :: "[i,i] \<Rightarrow> i"  where
   "wg(F,Y) \<equiv> \<Union>({X \<in> Pow(program). F:(X guarantees Y)})"
 
 definition
   (* Weakest existential property stronger than X *)
-   wx :: "i =>i"  where
+   wx :: "i \<Rightarrow>i"  where
    "wx(X) \<equiv> \<Union>({Y \<in> Pow(program). Y<=X \<and> ex_prop(Y)})"
 
 definition
   (*Ill-defined programs can arise through "\<squnion>"*)
   welldef :: i  where
   "welldef \<equiv> {F \<in> program. Init(F) \<noteq> 0}"
   
 definition
-  refines :: "[i, i, i] => o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10)  where
+  refines :: "[i, i, i] \<Rightarrow> o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10)  where
   "G refines F wrt X \<equiv>
    \<forall>H \<in> program. (F ok H  \<and> G ok H \<and> F \<squnion> H \<in> welldef \<inter> X)
     \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
 
 definition
-  iso_refines :: "[i,i, i] => o"  (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10)  where
+  iso_refines :: "[i,i, i] \<Rightarrow> o"  (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10)  where
   "G iso_refines F wrt X \<equiv>  F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
 
 
 (*** existential properties ***)
 
 lemma ex_imp_subset_program: "ex_prop(X) \<Longrightarrow> X\<subseteq>program"
 by (simp add: ex_prop_def)
 
 lemma ex1 [rule_format]: 
  "GG \<in> Fin(program) 
-  \<Longrightarrow> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (%G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
+  \<Longrightarrow> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (\<lambda>G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
 apply (unfold ex_prop_def)
 apply (erule Fin_induct)
 apply (simp_all add: OK_cons_iff)
 apply (safe elim!: not_emptyE, auto) 
 done
 
 lemma ex2 [rule_format]: 
 "X \<subseteq> program \<Longrightarrow>  
- (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X) 
+ (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(\<lambda>G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X) 
    \<longrightarrow> ex_prop(X)"
 apply (unfold ex_prop_def, clarify)
 apply (drule_tac x = "{F,G}" in bspec)
 apply (simp_all add: OK_iff_ok)
 apply (auto intro: ok_sym)

 
 (*Chandy \<and> Sanders take this as a definition*)
 
 lemma ex_prop_finite:
      "ex_prop(X) \<longleftrightarrow> (X\<subseteq>program \<and>  
-  (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<and> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))"
+  (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<and> OK(GG,(\<lambda>G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))"
 apply auto
 apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+
 done
 
 (* Equivalent definition of ex_prop given at the end of section 3*)

 apply (simp (no_asm_simp))
 done
 
 lemma uv1 [rule_format]: 
      "GG \<in> Fin(program) \<Longrightarrow>  
-      (uv_prop(X)\<longrightarrow> GG \<subseteq> X \<and> OK(GG, (%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
+      (uv_prop(X)\<longrightarrow> GG \<subseteq> X \<and> OK(GG, (\<lambda>G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
 apply (unfold uv_prop_def)
 apply (erule Fin_induct)
 apply (auto simp add: OK_cons_iff)
 done
 
 lemma uv2 [rule_format]: 
      "X\<subseteq>program  \<Longrightarrow> 
-      (\<forall>GG \<in> Fin(program). GG \<subseteq> X \<and> OK(GG,(%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)
+      (\<forall>GG \<in> Fin(program). GG \<subseteq> X \<and> OK(GG,(\<lambda>G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)
       \<longrightarrow> uv_prop(X)"
 apply (unfold uv_prop_def, auto)
 apply (drule_tac x = 0 in bspec, simp+) 
 apply (drule_tac x = "{F,G}" in bspec, simp) 
 apply (force dest: ok_sym simp add: OK_iff_ok) 
 done
 
 (*Chandy \<and> Sanders take this as a definition*)
 lemma uv_prop_finite: 
 "uv_prop(X) \<longleftrightarrow> X\<subseteq>program \<and>  
-  (\<forall>GG \<in> Fin(program). GG \<subseteq> X \<and> OK(GG, %G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in>  X)"
+  (\<forall>GG \<in> Fin(program). GG \<subseteq> X \<and> OK(GG, \<lambda>G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in>  X)"
 apply auto
 apply (blast dest: uv_imp_subset_program)
 apply (blast intro: uv1)
 apply (blast intro!: uv2 dest:)
 done

 lemma component_of_wg: 
     "F component_of H \<Longrightarrow> H \<in> wg(F,X) \<longleftrightarrow> (H \<in> X \<and> F \<in> program \<and> H \<in> program)"
 by (simp (no_asm_simp) add: wg_equiv)
 
 lemma wg_finite [rule_format]: 
-"\<forall>FF \<in> Fin(program). FF \<inter> X \<noteq> 0 \<longrightarrow> OK(FF, %F. F)  
+"\<forall>FF \<in> Fin(program). FF \<inter> X \<noteq> 0 \<longrightarrow> OK(FF, \<lambda>F. F)  
    \<longrightarrow> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in>  wg(F,X)) \<longleftrightarrow> ((\<Squnion>F \<in> FF. F) \<in> X))"
 apply clarify
 apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
 apply (drule_tac X = X in component_of_wg)
 apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])