src/HOL/UNITY/FP.thy
changeset 15481 fc075ae929e4
parent 13812 91713a1915ee
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/FP.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/UNITY/FP.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -19,20 +19,19 @@
     1.4      "FP F == {s. F : stable {s}}"
     1.5  
     1.6  lemma stable_FP_Orig_Int: "F : stable (FP_Orig F Int B)"
     1.7 -apply (unfold FP_Orig_def stable_def)
     1.8 -apply (subst Int_Union2)
     1.9 +apply (simp only: FP_Orig_def stable_def Int_Union2)
    1.10  apply (blast intro: constrains_UN)
    1.11  done
    1.12  
    1.13  lemma FP_Orig_weakest:
    1.14      "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
    1.15 -by (unfold FP_Orig_def stable_def, blast)
    1.16 +by (simp add: FP_Orig_def stable_def, blast)
    1.17  
    1.18  lemma stable_FP_Int: "F : stable (FP F Int B)"
    1.19  apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
    1.20  prefer 2 apply blast
    1.21  apply (simp (no_asm_simp) add: Int_insert_right)
    1.22 -apply (unfold FP_def stable_def)
    1.23 +apply (simp add: FP_def stable_def)
    1.24  apply (rule constrains_UN)
    1.25  apply (simp (no_asm))
    1.26  done
    1.27 @@ -40,7 +39,7 @@
    1.28  lemma FP_equivalence: "FP F = FP_Orig F"
    1.29  apply (rule equalityI) 
    1.30   apply (rule stable_FP_Int [THEN FP_Orig_weakest])
    1.31 -apply (unfold FP_Orig_def FP_def, clarify)
    1.32 +apply (simp add: FP_Orig_def FP_def, clarify)
    1.33  apply (drule_tac x = "{x}" in spec)
    1.34  apply (simp add: Int_insert_right)
    1.35  done