--- a/src/HOL/UNITY/FP.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/FP.ML Thu Oct 15 11:35:07 1998 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
+Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)";
by (stac Int_Union2 1);
by (rtac ball_constrains_UN 1);
by (Simp_tac 1);
@@ -16,13 +16,13 @@
val prems = goalw thy [FP_Orig_def, stable_def]
- "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
+ "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F";
by (blast_tac (claset() addIs prems) 1);
qed "FP_Orig_weakest";
-Goal "stable Acts (FP Acts Int B)";
-by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1);
+Goal "F : stable (FP F Int B)";
+by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1);
by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
by (rewrite_goals_tac [FP_def, stable_def]);
@@ -30,31 +30,31 @@
by (Simp_tac 1);
qed "stable_FP_Int";
-Goal "FP Acts <= FP_Orig Acts";
+Goal "FP F <= FP_Orig F";
by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
val lemma1 = result();
-Goalw [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
+Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F";
by (Clarify_tac 1);
by (dres_inst_tac [("x", "{x}")] spec 1);
by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
val lemma2 = result();
-Goal "FP Acts = FP_Orig Acts";
+Goal "FP F = FP_Orig F";
by (rtac ([lemma1,lemma2] MRS equalityI) 1);
qed "FP_equivalence";
val [prem] = goal thy
- "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
+ "(!!B. F : stable (A Int B)) ==> A <= FP F";
by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
qed "FP_weakest";
Goalw [FP_def, stable_def, constrains_def]
- "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})";
+ "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})";
by (Blast_tac 1);
qed "Compl_FP";
-Goal "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
+Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})";
by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
qed "Diff_FP";