src/HOL/UNITY/Constrains.thy
changeset 45605 a89b4bc311a5
parent 44870 0d23a8ae14df
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -86,8 +86,7 @@
     1.4  
     1.5  (*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
     1.6  lemmas constrains_reachable_Int =  
     1.7 -    subset_refl [THEN stable_reachable [unfolded stable_def], 
     1.8 -                 THEN constrains_Int, standard]
     1.9 +    subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
    1.10  
    1.11  (*Resembles the previous definition of Constrains*)
    1.12  lemma Constrains_eq_constrains: 
    1.13 @@ -263,8 +262,7 @@
    1.14  apply (blast intro: stable_imp_Stable)
    1.15  done
    1.16  
    1.17 -lemmas Increasing_constant =  
    1.18 -    increasing_constant [THEN increasing_imp_Increasing, standard, iff]
    1.19 +lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
    1.20  
    1.21  
    1.22  subsection{*The Elimination Theorem*}
    1.23 @@ -294,8 +292,8 @@
    1.24  lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
    1.25  by (simp add: Always_def)
    1.26  
    1.27 -lemmas AlwaysE = AlwaysD [THEN conjE, standard]
    1.28 -lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
    1.29 +lemmas AlwaysE = AlwaysD [THEN conjE]
    1.30 +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
    1.31  
    1.32  
    1.33  (*The set of all reachable states is Always*)
    1.34 @@ -312,8 +310,7 @@
    1.35  apply (blast intro: constrains_imp_Constrains)
    1.36  done
    1.37  
    1.38 -lemmas Always_reachable =
    1.39 -    invariant_reachable [THEN invariant_imp_Always, standard]
    1.40 +lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
    1.41  
    1.42  lemma Always_eq_invariant_reachable:
    1.43       "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
    1.44 @@ -355,10 +352,10 @@
    1.45                Constrains_eq_constrains Int_assoc [symmetric])
    1.46  
    1.47  (* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
    1.48 -lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
    1.49 +lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]
    1.50  
    1.51  (* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
    1.52 -lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
    1.53 +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
    1.54  
    1.55  (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
    1.56  lemma Always_Constrains_weaken:
    1.57 @@ -390,7 +387,7 @@
    1.58  
    1.59  (*Delete the nearest invariance assumption (which will be the second one
    1.60    used by Always_Int_I) *)
    1.61 -lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
    1.62 +lemmas Always_thin = thin_rl [of "F \<in> Always A"]
    1.63  
    1.64  
    1.65  subsection{*Totalize*}