src/HOL/UNITY/Follows.thy
changeset 56248 67dc9549fa15
parent 54859 64ff7f16d5b7
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/UNITY/Follows.thy	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5  apply (simp add: Follows_def Increasing_def Stable_def, auto)
     1.6  apply (erule_tac [3] Always_LeadsTo_weaken)
     1.7 -apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}" 
     1.8 +apply (erule_tac A = "{s. x \<le> f s}" and A' = "{s. x \<le> f s}" 
     1.9         in Always_Constrains_weaken, auto)
    1.10  apply (drule Always_Int_I, assumption)
    1.11  apply (force intro: Always_weaken)
    1.12 @@ -104,7 +104,7 @@
    1.13       "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
    1.14  apply (simp add: Follows_def Increasing_def Stable_def, auto)
    1.15  apply (erule_tac [3] Always_LeadsTo_weaken)
    1.16 -apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
    1.17 +apply (erule_tac A = "{s. x \<le> g s}" and A' = "{s. x \<le> g s}"
    1.18         in Always_Constrains_weaken, auto)
    1.19  apply (drule Always_Int_I, assumption)
    1.20  apply (force intro: Always_weaken)
    1.21 @@ -114,12 +114,13 @@
    1.22  subsection{*Union properties (with the subset ordering)*}
    1.23  
    1.24  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
    1.25 +
    1.26  lemma increasing_Un: 
    1.27      "[| F \<in> increasing f;  F \<in> increasing g |]  
    1.28       ==> F \<in> increasing (%s. (f s) \<union> (g s))"
    1.29  apply (simp add: increasing_def stable_def constrains_def, auto)
    1.30 -apply (drule_tac x = "f xa" in spec)
    1.31 -apply (drule_tac x = "g xa" in spec)
    1.32 +apply (drule_tac x = "f xb" in spec)
    1.33 +apply (drule_tac x = "g xb" in spec)
    1.34  apply (blast dest!: bspec)
    1.35  done
    1.36  
    1.37 @@ -128,8 +129,8 @@
    1.38       ==> F \<in> Increasing (%s. (f s) \<union> (g s))"
    1.39  apply (auto simp add: Increasing_def Stable_def Constrains_def
    1.40                        stable_def constrains_def)
    1.41 -apply (drule_tac x = "f xa" in spec)
    1.42 -apply (drule_tac x = "g xa" in spec)
    1.43 +apply (drule_tac x = "f xb" in spec)
    1.44 +apply (drule_tac x = "g xb" in spec)
    1.45  apply (blast dest!: bspec)
    1.46  done
    1.47  
    1.48 @@ -172,8 +173,8 @@
    1.49      "[| F \<in> increasing f;  F \<in> increasing g |]  
    1.50       ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
    1.51  apply (simp add: increasing_def stable_def constrains_def, auto)
    1.52 -apply (drule_tac x = "f xa" in spec)
    1.53 -apply (drule_tac x = "g xa" in spec)
    1.54 +apply (drule_tac x = "f xb" in spec)
    1.55 +apply (drule_tac x = "g xb" in spec)
    1.56  apply (drule bspec, assumption) 
    1.57  apply (blast intro: add_mono order_trans)
    1.58  done
    1.59 @@ -183,8 +184,8 @@
    1.60       ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
    1.61  apply (auto simp add: Increasing_def Stable_def Constrains_def
    1.62                        stable_def constrains_def)
    1.63 -apply (drule_tac x = "f xa" in spec)
    1.64 -apply (drule_tac x = "g xa" in spec)
    1.65 +apply (drule_tac x = "f xb" in spec)
    1.66 +apply (drule_tac x = "g xb" in spec)
    1.67  apply (drule bspec, assumption) 
    1.68  apply (blast intro: add_mono order_trans)
    1.69  done