composition theory
authorpaulson
Thu Oct 01 18:28:47 1998 +0200 (1998-10-01)
changeset 5597a12b25c53df1
parent 5596 b29d18d8c4d2
child 5598 6b8dee1a6ebb
composition theory
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Comp.ML	Thu Oct 01 18:28:47 1998 +0200
     1.3 @@ -0,0 +1,109 @@
     1.4 +(*  Title:      HOL/UNITY/Comp.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Composition
    1.10 +
    1.11 +From Chandy and Sanders, "Reasoning About Program Composition"
    1.12 +*)
    1.13 +
    1.14 +Addsimps [Join_SKIP, Join_absorb];
    1.15 +
    1.16 +(*split_all_tac causes a big blow-up*)
    1.17 +claset_ref() := claset() delSWrapper "split_all_tac";
    1.18 +
    1.19 +Delsimps [split_paired_All];
    1.20 +
    1.21 +
    1.22 +(*** component ***)
    1.23 +
    1.24 +Goalw [component_def] "component F F";
    1.25 +by (blast_tac (claset() addIs [Join_SKIP]) 1);
    1.26 +qed "component_refl";
    1.27 +
    1.28 +AddIffs [component_refl];
    1.29 +
    1.30 +Goalw [component_def] "[| component F G; component G H |] ==> component F H";
    1.31 +by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    1.32 +qed "component_trans";
    1.33 +
    1.34 +Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
    1.35 +auto();
    1.36 +qed "componet_Acts";
    1.37 +
    1.38 +Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
    1.39 +auto();
    1.40 +qed "componet_Init";
    1.41 +
    1.42 +Goal "[| component F G; component G F |] ==> F=G";
    1.43 +by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
    1.44 +				      componet_Acts, componet_Init]) 1);
    1.45 +qed "component_anti_sym";
    1.46 +
    1.47 +
    1.48 +(*** existential properties ***)
    1.49 +
    1.50 +Goalw [ex_prop_def]
    1.51 +     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
    1.52 +by (etac finite_induct 1);
    1.53 +by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    1.54 +qed_spec_mp "ex1";
    1.55 +
    1.56 +Goalw [ex_prop_def]
    1.57 +     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X  \
    1.58 +\      ==> ex_prop X";
    1.59 +by (Clarify_tac 1);
    1.60 +by (dres_inst_tac [("x", "{F,G}")] spec 1);
    1.61 +auto();
    1.62 +qed "ex2";
    1.63 +
    1.64 +(*Chandy & Sanders take this as a definition*)
    1.65 +Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
    1.66 +by (blast_tac (claset() addIs [ex1,ex2]) 1);
    1.67 +qed "ex_prop_finite";
    1.68 +
    1.69 +(*Their "equivalent definition" given at the end of section 3*)
    1.70 +Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))";
    1.71 +auto();
    1.72 +bws [ex_prop_def, component_def];
    1.73 +by (Blast_tac 1);
    1.74 +by Safe_tac;
    1.75 +by (stac Join_commute 2);
    1.76 +by (ALLGOALS Blast_tac);
    1.77 +qed "ex_prop_equiv";
    1.78 +
    1.79 +
    1.80 +(*** universal properties ***)
    1.81 +
    1.82 +Goalw [uv_prop_def]
    1.83 +     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
    1.84 +by (etac finite_induct 1);
    1.85 +by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
    1.86 +qed_spec_mp "uv1";
    1.87 +
    1.88 +Goalw [uv_prop_def]
    1.89 +     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
    1.90 +br conjI 1;
    1.91 +by (Clarify_tac 2);
    1.92 +by (dres_inst_tac [("x", "{F,G}")] spec 2);
    1.93 +by (dres_inst_tac [("x", "{}")] spec 1);
    1.94 +auto();
    1.95 +qed "uv2";
    1.96 +
    1.97 +(*Chandy & Sanders take this as a definition*)
    1.98 +Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
    1.99 +by (blast_tac (claset() addIs [uv1,uv2]) 1);
   1.100 +qed "uv_prop_finite";
   1.101 +
   1.102 +
   1.103 +(*** guarantees ***)
   1.104 +
   1.105 +Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
   1.106 +by (Blast_tac 1);
   1.107 +qed "subset_imp_guarantees";
   1.108 +
   1.109 +Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
   1.110 +ex_prop_equiv
   1.111 +by (Blast_tac 1);
   1.112 +qed "subset_imp_guarantees";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Comp.thy	Thu Oct 01 18:28:47 1998 +0200
     2.3 @@ -0,0 +1,39 @@
     2.4 +(*  Title:      HOL/UNITY/Comp.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1998  University of Cambridge
     2.8 +
     2.9 +Composition
    2.10 +
    2.11 +From Chandy and Sanders, "Reasoning About Program Composition"
    2.12 +*)
    2.13 +
    2.14 +Comp = Union +
    2.15 +
    2.16 +constdefs
    2.17 +
    2.18 +  (*Existential and Universal properties.  I formalize the two-program
    2.19 +    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    2.20 +
    2.21 +  ex_prop  :: 'a program set => bool
    2.22 +   "ex_prop X == ALL F G. F:X | G: X --> (Join F G) : X"
    2.23 +
    2.24 +  strict_ex_prop  :: 'a program set => bool
    2.25 +   "strict_ex_prop X == ALL F G. (F:X | G: X) = (Join F G : X)"
    2.26 +
    2.27 +  uv_prop  :: 'a program set => bool
    2.28 +   "uv_prop X == SKIP: X & (ALL F G. F:X & G: X --> (Join F G) : X)"
    2.29 +
    2.30 +  strict_uv_prop  :: 'a program set => bool
    2.31 +   "strict_uv_prop X == SKIP: X & (ALL F G. (F:X & G: X) = (Join F G : X))"
    2.32 +
    2.33 +  compatible :: ['a program, 'a program] => bool
    2.34 +   "compatible F G == Init F Int Init G ~= {}"
    2.35 +
    2.36 +  component :: ['a program, 'a program] => bool
    2.37 +   "component F H == EX G. Join F G = H"
    2.38 +
    2.39 +  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    2.40 +   "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
    2.41 +
    2.42 +end