--- a/src/HOL/UNITY/Comp.ML Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Sun Jun 13 13:52:50 1999 +0200
@@ -111,42 +111,54 @@
(*** guarantees ***)
(*This equation is more intuitive than the official definition*)
-Goal "(F : X guarantees Y) = \
+Goal "(F : X guar Y) = \
\ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
by (Blast_tac 1);
qed "guarantees_eq";
-Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
+Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV";
by (Blast_tac 1);
qed "subset_imp_guarantees_UNIV";
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guarantees_def] "X <= Y ==> F : X guarantees Y";
+Goalw [guarantees_def] "X <= Y ==> F : X guar Y";
by (Blast_tac 1);
qed "subset_imp_guarantees";
(*Remark at end of section 4.1*)
-Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
+Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)";
by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
by (blast_tac (claset() addEs [equalityE]) 1);
qed "ex_prop_equiv2";
+(** Distributive laws. Re-orient to perform miniscoping **)
+
Goalw [guarantees_def]
- "(INT X:XX. X guarantees Y) = (UN X:XX. X) guarantees Y";
+ "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)";
by (Blast_tac 1);
-qed "INT_guarantees_left";
+qed "guarantees_UN_left";
Goalw [guarantees_def]
- "(INT Y:YY. X guarantees Y) = X guarantees (INT Y:YY. Y)";
+ "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)";
+by (Blast_tac 1);
+qed "guarantees_Un_left";
+
+Goalw [guarantees_def]
+ "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)";
by (Blast_tac 1);
-qed "INT_guarantees_right";
+qed "guarantees_INT_right";
-Goalw [guarantees_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
+Goalw [guarantees_def]
+ "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)";
+by (Blast_tac 1);
+qed "guarantees_Int_right";
+
+Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))";
by (Blast_tac 1);
qed "shunting";
-Goalw [guarantees_def] "(X guarantees Y) = -Y guarantees -X";
+Goalw [guarantees_def] "(X guar Y) = -Y guar -X";
by (Blast_tac 1);
qed "contrapositive";
@@ -155,41 +167,41 @@
**)
Goalw [guarantees_def]
- "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
-\ ==> F : (V Int Y) guarantees Z";
+ "[| F : V guar X; F : (X Int Y) guar Z |]\
+\ ==> F : (V Int Y) guar Z";
by (Blast_tac 1);
qed "combining1";
Goalw [guarantees_def]
- "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\
-\ ==> F : V guarantees (X Un Z)";
+ "[| F : V guar (X Un Y); F : Y guar Z |]\
+\ ==> F : V guar (X Un Z)";
by (Blast_tac 1);
qed "combining2";
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
does not suit Isabelle... **)
-(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+(*Premise should be (!!i. i: I ==> F: X guar Y i) *)
Goalw [guarantees_def]
- "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
+ "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)";
by (Blast_tac 1);
qed "all_guarantees";
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F: X guar Y i; i: I |] *)
Goalw [guarantees_def]
- "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
+ "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)";
by (Blast_tac 1);
qed "ex_guarantees";
val prems = Goal
"(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \
-\ ==> F : X guarantees Y";
+\ ==> F : X guar Y";
by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1);
by (blast_tac (claset() addIs prems) 1);
qed "guaranteesI";
Goalw [guarantees_def, component_def]
- "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y";
+ "[| F : X guar Y; F Join G : X |] ==> F Join G : Y";
by (Blast_tac 1);
qed "guaranteesD";
--- a/src/HOL/UNITY/Comp.thy Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Comp.thy Sun Jun 13 13:52:50 1999 +0200
@@ -34,8 +34,9 @@
component :: ['a program, 'a program] => bool (infixl 50)
"F component H == EX G. F Join G = H"
- guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
- "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
+ guarantees :: ['a program set, 'a program set] => 'a program set
+ (infixl "guar" 65)
+ "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
refines :: ['a program, 'a program, 'a program set] => bool
("(3_ refines _ wrt _)" [10,10,10] 10)
--- a/src/HOL/UNITY/Extend.ML Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Sun Jun 13 13:52:50 1999 +0200
@@ -367,15 +367,13 @@
(simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1);
qed "extend_Join_eq_extend_D";
-Goal "F : X guarantees Y \
-\ ==> extend h F : (extend h `` X) guarantees (extend h `` Y)";
+Goal "F : X guar Y ==> extend h F : (extend h `` X) guar (extend h `` Y)";
by (rtac guaranteesI 1);
by Auto_tac;
by (blast_tac (claset() addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
-Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
-\ ==> F : X guarantees Y";
+Goal "extend h F : (extend h `` X) guar (extend h `` Y) ==> F : X guar Y";
by (rtac guaranteesI 1);
by (rewrite_goals_tac [guarantees_def, component_def]);
by Auto_tac;
@@ -386,8 +384,7 @@
by Auto_tac;
qed "extend_guarantees_imp_guarantees";
-Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) \
-\ = (F : X guarantees Y)";
+Goal "(extend h F : (extend h `` X) guar (extend h `` Y)) = (F : X guar Y)";
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
extend_guarantees_imp_guarantees]) 1);
qed "extend_guarantees_eq";