src/ZF/UNITY/SubstAx.thy

 (*Resembles the previous definition of LeadsTo*)
 
 (* Equivalence with the HOL-like definition *)
 lemma LeadsTo_eq:
 "st_set(B)\<Longrightarrow> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
 done
 
 lemma LeadsTo_type: "A \<longmapsto>w B <=program"
 by (unfold LeadsTo_def, auto)

 (** Conjoining an Always property **)
 lemma Always_LeadsTo_pre: "F \<in> Always(I) \<Longrightarrow> (F:(I \<inter> A) \<longmapsto>w A') \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
 by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
 
 lemma Always_LeadsTo_post: "F \<in> Always(I) \<Longrightarrow> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
 done
 
 (* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
 lemma Always_LeadsToI: "\<lbrakk>F \<in> Always(C); F \<in> (C \<inter> A) \<longmapsto>w A'\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w A'"

 lemma LeadsTo_state: "F \<in> A \<longmapsto>w state \<longleftrightarrow> F \<in> program"
 by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
 declare LeadsTo_state [iff]
 
 lemma LeadsTo_weaken_R: "\<lbrakk>F \<in> A \<longmapsto>w A';  A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B'"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (auto intro: leadsTo_weaken_R)
 done
 
 lemma LeadsTo_weaken_L: "\<lbrakk>F \<in> A \<longmapsto>w A'; B \<subseteq> A\<rbrakk> \<Longrightarrow> F \<in> B \<longmapsto>w A'"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (auto intro: leadsTo_weaken_L)
 done
 
 lemma LeadsTo_weaken: "\<lbrakk>F \<in> A \<longmapsto>w A'; B<=A; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> B \<longmapsto>w B'"
 by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)

 lemma PSP2: "\<lbrakk>F \<in> A \<longmapsto>w A'; F \<in> B Co B'\<rbrakk>\<Longrightarrow> F:(B' \<inter> A) \<longmapsto>w ((B \<inter> A') \<union> (B' - B))"
 by (simp (no_asm_simp) add: PSP Int_ac)
 
 lemma PSP_Unless:
 "\<lbrakk>F \<in> A \<longmapsto>w A'; F \<in> B Unless B'\<rbrakk>\<Longrightarrow> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
-apply (unfold op_Unless_def)
+  unfolding op_Unless_def
 apply (drule PSP, assumption)
 apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
 done
 
 (*** Induction rules ***)

 
 lemma Stable_completion:
      "\<lbrakk>F \<in> A \<longmapsto>w A';  F \<in> Stable(A');
          F \<in> B \<longmapsto>w B';  F \<in> Stable(B')\<rbrakk>
     \<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
     prefer 5
     apply blast
 apply auto
 done

 lemma Finite_stable_completion:
      "\<lbrakk>I \<in> Fin(X);
          (\<And>i. i \<in> I \<Longrightarrow> F \<in> A(i) \<longmapsto>w A'(i));
          (\<And>i. i \<in> I \<Longrightarrow>F \<in> Stable(A'(i)));   F \<in> program\<rbrakk>
       \<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
 apply (rule_tac [3] subset_refl, auto)
 done
 
 ML \<open>