infoflow: minor cleanup

proof/infoflow/FinalCaps.thy

@@ -1084,11 +1084,6 @@ lemma intra_label_cap_is_original_cap[simp]:
   apply(simp add: intra_label_cap_def)
   done
 
-lemma slots_holding_overlapping_caps_is_original_cap[simp]:
-  "slots_holding_overlapping_caps cap (s\<lparr>is_original_cap := X\<rparr>) = slots_holding_overlapping_caps cap s"
-  apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
-  done
-
 lemma silc_inv_is_original_cap[simp]:
   "silc_inv aag st (s\<lparr>is_original_cap := X\<rparr>) = silc_inv aag st s"
   apply(simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)

proof/infoflow/Noninterference_Base_Alternatives.thy

@@ -33,16 +33,16 @@ lemma in_xources_ConsD:
   "x \<in> (xources (a # as) s u) \<Longrightarrow>
    (\<forall> s'. (s,s') \<in> Step a \<longrightarrow> x \<in> xources as s' u) \<or> 
    (x = dom a s \<and> (\<forall> s'. (s,s') \<in> Step a \<longrightarrow> (\<exists> v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)))"
-  by(auto simp: xources_Cons)
+  by auto
 
 lemma in_xources_ConsI1:
   "\<lbrakk>\<forall> s'. (s,s') \<in> Step a \<longrightarrow> x \<in> xources as s' u\<rbrakk> \<Longrightarrow> x \<in> xources (a#as) s u"
-  by(auto simp: xources_Cons)
+  by auto
 
 lemma in_xources_ConsI2:
   "\<lbrakk>x = dom a s; \<forall> s'. (s,s') \<in> Step a \<longrightarrow> (\<exists> v. dom a s \<leadsto> v \<and> v \<in> xources as s' u)\<rbrakk> \<Longrightarrow> 
   x \<in> xources (a#as) s u"
-  by(auto simp: xources_Cons)
+  by auto
 
 
 declare xources_Nil [simp del]     
@@ -665,4 +665,4 @@ lemma Noninfluence_strong_uwr_equiv_Noninfluence_strong_uwr_pg:
 end
 
 
-end (* a comment *)
+end

proof/infoflow/Noninterference_Base_Refinement.thy

@@ -155,5 +155,3 @@ lemma Noninfluence_strong_uwr_quasi_refinement_closed:
   
 end
 end
-
-(* a comment *)