src/HOL/UNITY/Detects.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Detects.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Detects.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -21,7 +21,8 @@
     1.4  
     1.5  (* Corollary from Sectiom 3.6.4 *)
     1.6  
     1.7 -lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
     1.8 +lemma Always_at_FP:
     1.9 +     "[|F \<in> A LeadsTo B; all_total F|] ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
    1.10  apply (rule LeadsTo_empty)
    1.11  apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
    1.12  apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
    1.13 @@ -36,8 +37,7 @@
    1.14  apply (unfold Detects_def Int_def)
    1.15  apply (simp (no_asm))
    1.16  apply safe
    1.17 -apply (rule_tac [2] LeadsTo_Trans)
    1.18 -apply auto
    1.19 +apply (rule_tac [2] LeadsTo_Trans, auto)
    1.20  apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
    1.21   apply (blast intro: Always_weaken)
    1.22  apply (simp add: Always_Int_distrib)
    1.23 @@ -49,9 +49,7 @@
    1.24  done
    1.25  
    1.26  lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
    1.27 -apply (unfold Equality_def)
    1.28 -apply blast
    1.29 -done
    1.30 +by (unfold Equality_def, blast)
    1.31  
    1.32  (*Not quite antisymmetry: sets A and B agree in all reachable states *)
    1.33  lemma Detects_antisym: 
    1.34 @@ -64,9 +62,9 @@
    1.35  (* Theorem from Section 3.8 *)
    1.36  
    1.37  lemma Detects_Always: 
    1.38 -     "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
    1.39 +     "[|F \<in> A Detects B; all_total F|] ==> F \<in> Always (-(FP F) \<union> (A <==> B))"
    1.40  apply (unfold Detects_def Equality_def)
    1.41 -apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
    1.42 +apply (simp add: Un_Int_distrib Always_Int_distrib)
    1.43  apply (blast dest: Always_at_FP intro: Always_weaken)
    1.44  done
    1.45  
    1.46 @@ -75,7 +73,7 @@
    1.47  lemma Detects_Imp_LeadstoEQ: 
    1.48       "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
    1.49  apply (unfold Detects_def Equality_def)
    1.50 -apply (rule_tac B = "B" in LeadsTo_Diff)
    1.51 +apply (rule_tac B = B in LeadsTo_Diff)
    1.52   apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
    1.53  apply (blast intro: Always_LeadsTo_weaken)
    1.54  done