src/HOL/UNITY/Comp.ML
changeset 6646 3ea726909fff
parent 6299 1a88db6e7c7e
child 6703 8103c1fb092d
     1.1 --- a/src/HOL/UNITY/Comp.ML	Mon May 17 10:37:07 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Mon May 17 10:38:08 1999 +0200
     1.3 @@ -16,48 +16,48 @@
     1.4  
     1.5  (*** component ***)
     1.6  
     1.7 -Goalw [component_def] "component SKIP F";
     1.8 +Goalw [component_def] "SKIP component F";
     1.9  by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    1.10  qed "component_SKIP";
    1.11  
    1.12 -Goalw [component_def] "component F F";
    1.13 +Goalw [component_def] "F component F";
    1.14  by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
    1.15  qed "component_refl";
    1.16  
    1.17  AddIffs [component_SKIP, component_refl];
    1.18  
    1.19 -Goalw [component_def] "component F (F Join G)";
    1.20 +Goalw [component_def] "F component (F Join G)";
    1.21  by (Blast_tac 1);
    1.22  qed "component_Join1";
    1.23  
    1.24 -Goalw [component_def] "component G (F Join G)";
    1.25 +Goalw [component_def] "G component (F Join G)";
    1.26  by (simp_tac (simpset() addsimps [Join_commute]) 1);
    1.27  by (Blast_tac 1);
    1.28  qed "component_Join2";
    1.29  
    1.30 -Goalw [component_def] "i : I ==> component (F i) (JN i:I. (F i))";
    1.31 +Goalw [component_def] "i : I ==> (F i) component (JN i:I. (F i))";
    1.32  by (blast_tac (claset() addIs [JN_absorb]) 1);
    1.33  qed "component_JN";
    1.34  
    1.35 -Goalw [component_def] "[| component F G; component G H |] ==> component F H";
    1.36 +Goalw [component_def] "[| F component G; G component H |] ==> F component H";
    1.37  by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    1.38  qed "component_trans";
    1.39  
    1.40 -Goalw [component_def] "component F G ==> Acts F <= Acts G";
    1.41 +Goalw [component_def] "F component G ==> Acts F <= Acts G";
    1.42  by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1);
    1.43  qed "component_Acts";
    1.44  
    1.45 -Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
    1.46 +Goalw [component_def,Join_def] "F component G ==> Init G <= Init F";
    1.47  by Auto_tac;
    1.48  qed "component_Init";
    1.49  
    1.50 -Goal "[| component F G; component G F |] ==> F=G";
    1.51 +Goal "[| F component G; G component F |] ==> F=G";
    1.52  by (blast_tac (claset() addSIs [program_equalityI, 
    1.53  				component_Init, component_Acts]) 1);
    1.54  qed "component_anti_sym";
    1.55  
    1.56  Goalw [component_def]
    1.57 -      "component F H = (EX G. F Join G = H & Disjoint F G)";
    1.58 +      "F component H = (EX G. F Join G = H & Disjoint F G)";
    1.59  by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
    1.60  qed "component_eq";
    1.61  
    1.62 @@ -83,7 +83,7 @@
    1.63  qed "ex_prop_finite";
    1.64  
    1.65  (*Their "equivalent definition" given at the end of section 3*)
    1.66 -Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))";
    1.67 +Goal "ex_prop X = (ALL G. G:X = (ALL H. G component H --> H: X))";
    1.68  by Auto_tac;
    1.69  by (rewrite_goals_tac [ex_prop_def, component_def]);
    1.70  by (Blast_tac 1);
    1.71 @@ -127,6 +127,11 @@
    1.72  
    1.73  Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
    1.74  by (Blast_tac 1);
    1.75 +qed "subset_imp_guarantees_UNIV";
    1.76 +
    1.77 +(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
    1.78 +Goalw [guarantees_def] "X <= Y ==> F : X guarantees Y";
    1.79 +by (Blast_tac 1);
    1.80  qed "subset_imp_guarantees";
    1.81  
    1.82  (*Remark at end of section 4.1*)
    1.83 @@ -153,21 +158,32 @@
    1.84  by (Blast_tac 1);
    1.85  qed "contrapositive";
    1.86  
    1.87 +(** The following two can be expressed using intersection and subset, which
    1.88 +    is more faithful to the text but looks cryptic.
    1.89 +**)
    1.90 +
    1.91  Goalw [guarantees_def]
    1.92 -    "V guarantees X Int ((X Int Y) guarantees Z) <= (V Int Y) guarantees Z";
    1.93 +    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
    1.94 +\    ==> F : (V Int Y) guarantees Z";
    1.95  by (Blast_tac 1);
    1.96  qed "combining1";
    1.97  
    1.98  Goalw [guarantees_def]
    1.99 -    "V guarantees (X Un Y) Int (Y guarantees Z) <= V guarantees (X Un Z)";
   1.100 +    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
   1.101 +\    ==> F : V guarantees (X Un Z)";
   1.102  by (Blast_tac 1);
   1.103  qed "combining2";
   1.104  
   1.105 +(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   1.106 +    does not suit Isabelle... **)
   1.107 +
   1.108 +(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   1.109  Goalw [guarantees_def]
   1.110       "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
   1.111  by (Blast_tac 1);
   1.112  qed "all_guarantees";
   1.113  
   1.114 +(*Premises should be [| F: X guarantees Y i; i: I |] *)
   1.115  Goalw [guarantees_def]
   1.116       "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   1.117  by (Blast_tac 1);
   1.118 @@ -181,8 +197,7 @@
   1.119  qed "guaranteesI";
   1.120  
   1.121  Goalw [guarantees_def, component_def]
   1.122 -     "[| F : X guarantees Y;  F Join G : X |] \
   1.123 -\     ==> F Join G : Y";
   1.124 +     "[| F : X guarantees Y;  F Join G : X |] ==> F Join G : Y";
   1.125  by (Blast_tac 1);
   1.126  qed "guaranteesD";
   1.127