Union primitives and examples
authorpaulson
Wed Aug 05 10:56:58 1998 +0200 (1998-08-05)
changeset 52521b0f14d11142
parent 5251 fee54d5c511c
child 5253 82a5ca6290aa
Union primitives and examples
src/HOL/UNITY/Handshake.ML
src/HOL/UNITY/Handshake.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Handshake.ML	Wed Aug 05 10:56:58 1998 +0200
     1.3 @@ -0,0 +1,62 @@
     1.4 +(*  Title:      HOL/UNITY/Handshake
     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 +Handshake Protocol
    1.10 +
    1.11 +From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
    1.12 +*)
    1.13 +
    1.14 +(*split_all_tac causes a big blow-up*)
    1.15 +claset_ref() := claset() delSWrapper "split_all_tac";
    1.16 +
    1.17 +(*Simplification for records*)
    1.18 +Addsimps (thms"state.update_defs");
    1.19 +Addsimps [invFG_def];
    1.20 +
    1.21 +
    1.22 +Goalw [prgF_def, Join_def] "id : Acts (Join prgF prgG) ";
    1.23 +by (Simp_tac 1);
    1.24 +qed "id_in_Acts";
    1.25 +AddIffs [id_in_Acts];
    1.26 +
    1.27 +
    1.28 +Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
    1.29 +by (rtac invariantI 1);
    1.30 +by (force_tac (claset(), 
    1.31 +	       simpset() addsimps [Join_def]) 1);
    1.32 +by (auto_tac (claset(), simpset() addsimps [stable_Join]));
    1.33 +by (constrains_tac [prgG_def,cmdG_def] 2);
    1.34 +by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
    1.35 +by (constrains_tac [prgF_def,cmdF_def] 1);
    1.36 +qed "invFG";
    1.37 +
    1.38 +Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
    1.39 +br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    1.40 +by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
    1.41 +by (constrains_tac [prgF_def,cmdF_def] 1);
    1.42 +qed "lemma2_1";
    1.43 +
    1.44 +Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
    1.45 +br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
    1.46 +by (constrains_tac [prgG_def,cmdG_def] 2);
    1.47 +by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
    1.48 +qed "lemma2_2";
    1.49 +
    1.50 +
    1.51 +Goal "LeadsTo (Join prgF prgG) {s. NF s = k} {s. k < NF s}";
    1.52 +br LeadsTo_Diff 1;
    1.53 +br lemma2_2 2;
    1.54 +br LeadsTo_Trans 1;
    1.55 +br lemma2_2 2;
    1.56 +br (lemma2_1 RS LeadsTo_weaken_L) 1;
    1.57 +by Auto_tac;
    1.58 +val lemma = result();
    1.59 +
    1.60 +
    1.61 +Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
    1.62 +by (res_inst_tac [("f", "NF")] R_lessThan_induct 1);
    1.63 +auto();
    1.64 +br (lemma RS LeadsTo_weaken) 1;
    1.65 +auto();
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/Handshake.thy	Wed Aug 05 10:56:58 1998 +0200
     2.3 @@ -0,0 +1,39 @@
     2.4 +(*  Title:      HOL/UNITY/Handshake.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 +Handshake Protocol
    2.10 +
    2.11 +From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
    2.12 +*)
    2.13 +
    2.14 +Handshake = Union +
    2.15 +
    2.16 +record state =
    2.17 +  BB :: bool
    2.18 +  NF :: nat
    2.19 +  NG :: nat
    2.20 +
    2.21 +constdefs
    2.22 +  (*F's program*)
    2.23 +  cmdF :: "(state*state) set"
    2.24 +    "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
    2.25 +
    2.26 +  prgF :: "state program"
    2.27 +    "prgF == (|Init = {s. NF s = 0 & BB s},
    2.28 +	       Acts = {id, cmdF}|)"
    2.29 +
    2.30 +  (*G's program*)
    2.31 +  cmdG :: "(state*state) set"
    2.32 +    "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
    2.33 +
    2.34 +  prgG :: "state program"
    2.35 +    "prgG == (|Init = {s. NG s = 0 & BB s},
    2.36 +	       Acts = {id, cmdG}|)"
    2.37 +
    2.38 +  (*the joint invariant*)
    2.39 +  invFG :: "state set"
    2.40 +    "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
    2.41 +
    2.42 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Union.ML	Wed Aug 05 10:56:58 1998 +0200
     3.3 @@ -0,0 +1,117 @@
     3.4 +(*  Title:      HOL/UNITY/Union.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1998  University of Cambridge
     3.8 +
     3.9 +Unions of programs
    3.10 +
    3.11 +From Misra's Chapter 5: Asynchronous Compositions of Programs
    3.12 +
    3.13 +NOT CLEAR WHETHER ALL THESE FORMS ARE NEEDED: 
    3.14 +    Maybe Join instead of Un, and JOIN for UNION
    3.15 +*)
    3.16 +
    3.17 +(*** Safety: constrains, stable, FP ***)
    3.18 +
    3.19 +Goalw [constrains_def]
    3.20 +    "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
    3.21 +by (Blast_tac 1);
    3.22 +qed "constrains_UN";
    3.23 +
    3.24 +Goalw [constrains_def]
    3.25 +    "constrains (actsF Un actsG) A B =  \
    3.26 +\    (constrains actsF A B & constrains actsG A B)";
    3.27 +by (simp_tac (simpset() addsimps [ball_Un]) 1);
    3.28 +qed "constrains_Un";
    3.29 +
    3.30 +(*Provable by constrains_Un and constrains_weaken, but why bother?*)
    3.31 +Goalw [constrains_def]
    3.32 +     "[| constrains actsF A A';  constrains actsG B B' |] \
    3.33 +\     ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
    3.34 +by (Blast_tac 1);
    3.35 +qed "constrains_Un_weaken";
    3.36 +
    3.37 +Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
    3.38 +by (simp_tac (simpset() addsimps [constrains_UN]) 1);
    3.39 +qed "stable_UN";
    3.40 +
    3.41 +Goalw [stable_def]
    3.42 +    "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
    3.43 +by (simp_tac (simpset() addsimps [constrains_Un]) 1);
    3.44 +qed "stable_Un";
    3.45 +
    3.46 +Goal "stable (Acts (Join prgF prgG)) A = \
    3.47 +\     (stable (Acts prgF) A & stable (Acts prgG) A)";
    3.48 +by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
    3.49 +qed "stable_Join";
    3.50 +
    3.51 +Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
    3.52 +by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
    3.53 +qed "FP_UN";
    3.54 +
    3.55 +
    3.56 +(*** Progress: transient, ensures ***)
    3.57 +
    3.58 +Goalw [transient_def]
    3.59 +    "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
    3.60 +by (Simp_tac 1);
    3.61 +qed "transient_UN";
    3.62 +
    3.63 +Goalw [ensures_def,transient_def]
    3.64 +    "ensures (UN i:I. acts i) A B = \
    3.65 +\    ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
    3.66 +\     (EX i:I. ensures (acts i) A B))";
    3.67 +by (simp_tac (simpset() addsimps [constrains_UN]) 1);
    3.68 +by Auto_tac;
    3.69 +qed "ensures_UN";
    3.70 +
    3.71 +(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
    3.72 +Goal "ensures (actsF Un actsG) A B =     \
    3.73 +\     (constrains actsF (A-B) (A Un B) & \
    3.74 +\      constrains actsG (A-B) (A Un B) & \
    3.75 +\      (ensures actsF A B | ensures actsG A B))";
    3.76 +by (simp_tac (simpset() addcongs [conj_cong]
    3.77 +			addsimps [ensures_UN, Un_eq_UN,
    3.78 +				  all_bool_eq, ex_bool_eq]) 1);
    3.79 +qed "ensures_Un";
    3.80 +
    3.81 +(*Or a longer proof via constrains_imp_subset*)
    3.82 +Goalw [stable_def, constrains_def]
    3.83 +     "[| stable actsF A;  constrains actsG A A';  id: actsG |] \
    3.84 +\     ==> constrains (actsF Un actsG) A A'";
    3.85 +by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
    3.86 +by (Blast_tac 1);
    3.87 +qed "stable_constrains_Un";
    3.88 +
    3.89 +Goalw [Join_def]
    3.90 +      "[| stable (Acts prgF) A;  invariant prgG A |]     \
    3.91 +\      ==> invariant (Join prgF prgG) A";
    3.92 +by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
    3.93 +by (Blast_tac 1);
    3.94 +qed "stable_Join_invariant";
    3.95 +
    3.96 +Goal "[| stable actsF A;  ensures actsG A B |]     \
    3.97 +\     ==> ensures (actsF Un actsG) A B";
    3.98 +by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
    3.99 +by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
   3.100 +by (etac constrains_weaken 1);
   3.101 +by Auto_tac;
   3.102 +qed "ensures_stable_Un1";
   3.103 +
   3.104 +Goal "[| stable (Acts prgF) A;  ensures (Acts prgG) A B |]     \
   3.105 +\     ==> ensures (Acts (Join prgF prgG)) A B";
   3.106 +by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
   3.107 +qed "ensures_stable_Join1";
   3.108 +
   3.109 +(*As above, but exchanging the roles of F and G*)
   3.110 +Goal "[| ensures actsF A B;  stable actsG A |]     \
   3.111 +\     ==> ensures (actsF Un actsG) A B";
   3.112 +by (stac Un_commute 1);
   3.113 +by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
   3.114 +qed "ensures_stable_Un2";
   3.115 +
   3.116 +Goal "[| ensures (Acts prgF) A B;  stable (Acts prgG) A |]     \
   3.117 +\     ==> ensures (Acts (Join prgF prgG)) A B";
   3.118 +by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
   3.119 +qed "ensures_stable_Join2";
   3.120 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 10:56:58 1998 +0200
     4.3 @@ -0,0 +1,19 @@
     4.4 +(*  Title:      HOL/UNITY/Union.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1998  University of Cambridge
     4.8 +
     4.9 +Unions of programs
    4.10 +
    4.11 +From Misra's Chapter 5: Asynchronous Compositions of Programs
    4.12 +*)
    4.13 +
    4.14 +Union = SubstAx + FP +
    4.15 +
    4.16 +constdefs
    4.17 +
    4.18 +   Join :: "['a program, 'a program] => 'a program"
    4.19 +    "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    4.20 +			 Acts = Acts prgF Un Acts prgG|)"
    4.21 +
    4.22 +end