--- a/src/HOL/UNITY/Alloc.ML Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML Tue Aug 31 15:56:56 1999 +0200
@@ -6,6 +6,18 @@
Specification of Chandy and Charpentier's Allocator
*)
+
+Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
+
+(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *)
+Goal "[| b:A; a=b |] ==> a:A";
+by (etac ssubst 1);
+by (assume_tac 1);
+qed "subst_elem";
+
+
+
+
(*Generalized version allowing different clients*)
Goal "[| Alloc : alloc_spec; \
\ Client : (lessThan Nclients) funcset client_spec; \
@@ -32,6 +44,20 @@
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
+val bij_sysOfAlloc = [inj_sysOfAlloc, surj_sysOfAlloc] MRS bijI;
+
+(*MUST BE AUTOMATED: even the statement of such results*)
+Goal "!!s. inv sysOfAlloc s = \
+\ ((| allocGiv = allocGiv s, \
+\ allocAsk = allocAsk s, \
+\ allocRel = allocRel s|), \
+\ client s)";
+by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper,
+ simpset() addsimps [sysOfAlloc_def]));
+qed "inv_sysOfAlloc_eq";
+
+
(**SHOULD NOT BE NECESSARY: The various injections into the system
state need to be treated symmetrically or done automatically*)
Goalw [sysOfClient_def] "inj sysOfClient";
@@ -49,6 +75,7 @@
AddIffs [inj_sysOfClient, surj_sysOfClient];
+val bij_sysOfClient = [inj_sysOfClient, surj_sysOfClient] MRS bijI;
(*MUST BE AUTOMATED: even the statement of such results*)
Goal "!!s. inv sysOfClient s = \
@@ -57,8 +84,8 @@
\ allocAsk = allocAsk s, \
\ allocRel = allocRel s|) )";
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
-by (rewrite_goals_tac [sysOfAlloc_def, sysOfClient_def]);
-by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
+by (auto_tac (claset() addSWrapper record_split_wrapper,
+ simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
qed "inv_sysOfClient_eq";
@@ -128,20 +155,21 @@
(*Not sure what to say about the other components because they involve
extend*)
-Goalw [System_def] "Network component System";
+Goalw [System_def] "Network <= System";
by (blast_tac (claset() addIs [componentI]) 1);
qed "Network_component_System";
-AddIffs [Network_component_System];
-
+Goalw [System_def] "(extend sysOfAlloc Alloc) <= System";
+by (blast_tac (claset() addIs [componentI]) 1);
+qed "Alloc_component_System";
-val project_guarantees' =
- [surj_sysOfClient, inj_sysOfClient] MRS export project_guarantees;
+AddIffs [Network_component_System, Alloc_component_System];
+
(* F : UNIV guarantees Increasing func
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
-val extend_guar_Increasing' =
- [surj_sysOfClient, inj_sysOfClient] MRS export extend_guar_Increasing
+val extend_Client_guar_Increasing =
+ bij_sysOfClient RS export extend_guar_Increasing
|> simplify (simpset() addsimps [inv_sysOfClient_eq]);
@@ -154,7 +182,7 @@
MRS guaranteesD) 1);
by (asm_simp_tac
(simpset() addsimps [guarantees_PLam_I,
- extend_guar_Increasing' RS guaranteesD,
+ extend_Client_guar_Increasing RS guaranteesD,
lift_prog_guar_Increasing]) 1);
qed "System_Increasing_rel";
@@ -169,13 +197,81 @@
System_Increasing_rel, Network]) 1);
qed "System_Increasing_allocRel";
-Goal "i < Nclients \
-\ ==> System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
-\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
-fr component_guaranteesD;
+
+(*NEED TO PROVE something like this (maybe without premise)*)
+Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
-val extend_guar_Increasing'' =
- [surj_sysOfAlloc, inj_sysOfAlloc] MRS export extend_guar_Increasing
+fun alloc_export th = bij_sysOfAlloc RS export th;
+
+val extend_Alloc_guar_Increasing =
+ alloc_export extend_guar_Increasing
|> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
+Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
+\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
+by (res_inst_tac
+ [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
+\ Int Increasing (sub i o allocRel))")]
+ component_guaranteesD 1);;
+br Alloc_component_System 3;
+br project_guarantees 1;
+br Alloc_Safety 1;
+by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2
+ THEN
+ full_simp_tac
+ (simpset() addsimps [inv_sysOfAlloc_eq,
+ alloc_export Collect_eq_extend_set RS sym]) 2);
+auto();
+by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 3);
+
+bd bspec 1;
+by (Blast_tac 1);
+
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+ [| i < Nclients;
+ extend sysOfAlloc Alloc Join G
+ : (sub i o allocRel) localTo Network &
+ extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
+ ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
+
+
+ [| i < Nclients;
+ H : (sub i o allocRel) localTo Network &
+ H : Increasing (sub i o allocRel) |]
+ ==> project sysOfAlloc H : Increasing (sub i o allocRel)
+
+Open_locale"Extend";
+
+Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
+by (asm_full_simp_tac
+ (simpset() addsimps [localTo_def,
+ project_extend_Join RS sym,
+ Diff_project_stable,
+ Collect_eq_extend_set RS sym]) 1);
+auto();
+br Diff_project_stable 1;
+PROBABLY FALSE;
+
+by (Clarify_tac 1);
+by (dres_inst_tac [("x","z")] spec 1);
+
+br (alloc_export project_Always_D) 2;
+
+by (rtac (alloc_export extend_Always RS iffD2) 2);
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+br guaranteesI 1;
+
+by (res_inst_tac
+ [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")]
+ component_guaranteesD 1);;
+
+
by (rtac (Alloc_Safety RS component_guaranteesD) 1);
+
+
+br (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1;
+br Alloc_Safety 1;
--- a/src/HOL/UNITY/Client.thy Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Client.thy Tue Aug 31 15:56:56 1999 +0200
@@ -6,7 +6,7 @@
Distributed Resource Management System: the Client
*)
-Client = Comp +
+Client = Guar +
consts
Max :: nat (*Maximum number of tokens*)
--- a/src/HOL/UNITY/Comp.ML Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML Tue Aug 31 15:56:56 1999 +0200
@@ -11,7 +11,7 @@
(*** component ***)
Goalw [component_def]
- "H component F | H component G ==> H component (F Join G)";
+ "H <= F | H <= G ==> H <= (F Join G)";
by Auto_tac;
by (res_inst_tac [("x", "G Join Ga")] exI 1);
by (res_inst_tac [("x", "G Join F")] exI 2);
@@ -19,349 +19,61 @@
qed "componentI";
Goalw [component_def]
- "(F component G) = (Init G <= Init F & Acts F <= Acts G)";
+ "(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
by (force_tac (claset() addSIs [exI, program_equalityI],
simpset() addsimps [Acts_Join]) 1);
qed "component_eq_subset";
-Goalw [component_def] "SKIP component F";
+Goalw [component_def] "SKIP <= F";
by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
qed "component_SKIP";
-Goalw [component_def] "F component F";
+Goalw [component_def] "F <= (F :: 'a program)";
by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
qed "component_refl";
AddIffs [component_SKIP, component_refl];
-Goal "F component SKIP ==> F = SKIP";
+Goal "F <= SKIP ==> F = SKIP";
by (auto_tac (claset() addSIs [program_equalityI],
simpset() addsimps [component_eq_subset]));
qed "SKIP_minimal";
-Goalw [component_def] "F component (F Join G)";
+Goalw [component_def] "F <= (F Join G)";
by (Blast_tac 1);
qed "component_Join1";
-Goalw [component_def] "G component (F Join G)";
+Goalw [component_def] "G <= (F Join G)";
by (simp_tac (simpset() addsimps [Join_commute]) 1);
by (Blast_tac 1);
qed "component_Join2";
-Goalw [component_def] "i : I ==> (F i) component (JN i:I. (F i))";
+Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
by (blast_tac (claset() addIs [JN_absorb]) 1);
qed "component_JN";
-Goalw [component_def] "[| F component G; G component H |] ==> F component H";
+Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)";
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
qed "component_trans";
-Goal "[| F component G; G component F |] ==> F=G";
+Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)";
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
by (blast_tac (claset() addSIs [program_equalityI]) 1);
qed "component_antisym";
Goalw [component_def]
- "F component H = (EX G. F Join G = H & Disjoint F G)";
+ "F <= H = (EX G. F Join G = H & Disjoint F G)";
by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
qed "component_eq";
-Goal "((F Join G) component H) = (F component H & G component H)";
+Goal "((F Join G) <= H) = (F <= H & G <= H)";
by (simp_tac (simpset() addsimps [component_eq_subset, Acts_Join]) 1);
by (Blast_tac 1);
qed "Join_component_iff";
-Goal "[| F component G; G : A co B |] ==> F : A co B";
+Goal "[| F <= G; G : A co B |] ==> F : A co B";
by (auto_tac (claset(),
simpset() addsimps [constrains_def, component_eq_subset]));
qed "component_constrains";
-(*** existential properties ***)
-
-Goalw [ex_prop_def]
- "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
-by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
-qed_spec_mp "ex1";
-
-Goalw [ex_prop_def]
- "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X";
-by (Clarify_tac 1);
-by (dres_inst_tac [("x", "{F,G}")] spec 1);
-by Auto_tac;
-qed "ex2";
-
-(*Chandy & Sanders take this as a definition*)
-Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
-by (blast_tac (claset() addIs [ex1,ex2]) 1);
-qed "ex_prop_finite";
-
-(*Their "equivalent definition" given at the end of section 3*)
-Goal "ex_prop X = (ALL G. G:X = (ALL H. G component H --> H: X))";
-by Auto_tac;
-by (rewrite_goals_tac [ex_prop_def, component_def]);
-by (Blast_tac 1);
-by Safe_tac;
-by (stac Join_commute 2);
-by (ALLGOALS Blast_tac);
-qed "ex_prop_equiv";
-
-
-(*** universal properties ***)
-
-Goalw [uv_prop_def]
- "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
-by (etac finite_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
-qed_spec_mp "uv1";
-
-Goalw [uv_prop_def]
- "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X ==> uv_prop X";
-by (rtac conjI 1);
-by (Clarify_tac 2);
-by (dres_inst_tac [("x", "{F,G}")] spec 2);
-by (dres_inst_tac [("x", "{}")] spec 1);
-by Auto_tac;
-qed "uv2";
-
-(*Chandy & Sanders take this as a definition*)
-Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
-by (blast_tac (claset() addIs [uv1,uv2]) 1);
-qed "uv_prop_finite";
-
-
-(*** guarantees ***)
-
-val prems = Goal
- "(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \
-\ ==> F : X guarantees Y";
-by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "guaranteesI";
-
-Goalw [guar_def, component_def]
- "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y";
-by (Blast_tac 1);
-qed "guaranteesD";
-
-(*This version of guaranteesD matches more easily in the conclusion*)
-Goalw [guar_def]
- "[| F : X guarantees Y; H : X; F component H |] ==> H : Y";
-by (Blast_tac 1);
-qed "component_guaranteesD";
-
-(*This equation is more intuitive than the official definition*)
-Goal "(F : X guarantees Y) = \
-\ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
-by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
-by (Blast_tac 1);
-qed "guarantees_eq";
-
-Goalw [guar_def]
- "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
-by (Blast_tac 1);
-qed "guarantees_weaken";
-
-Goalw [guar_def]
- "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y";
-by (blast_tac (claset() addIs [component_trans]) 1);
-qed "guarantees_weaken_prog";
-
-Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
-by (Blast_tac 1);
-qed "subset_imp_guarantees_UNIV";
-
-(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
-by (Blast_tac 1);
-qed "subset_imp_guarantees";
-
-(*Remark at end of section 4.1*)
-Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees 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 [guar_def]
- "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
-by (Blast_tac 1);
-qed "guarantees_UN_left";
-
-Goalw [guar_def]
- "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
-by (Blast_tac 1);
-qed "guarantees_Un_left";
-
-Goalw [guar_def]
- "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
-by (Blast_tac 1);
-qed "guarantees_INT_right";
-
-Goalw [guar_def]
- "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
-by (Blast_tac 1);
-qed "guarantees_Int_right";
-
-Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
-by (Blast_tac 1);
-qed "shunting";
-
-Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
-by (Blast_tac 1);
-qed "contrapositive";
-
-(** The following two can be expressed using intersection and subset, which
- is more faithful to the text but looks cryptic.
-**)
-
-Goalw [guar_def]
- "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\
-\ ==> F : (V Int Y) guarantees Z";
-by (Blast_tac 1);
-qed "combining1";
-
-Goalw [guar_def]
- "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\
-\ ==> F : V guarantees (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) *)
-Goalw [guar_def]
- "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
-by (Blast_tac 1);
-qed "all_guarantees";
-
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
-Goalw [guar_def]
- "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
-by (Blast_tac 1);
-qed "ex_guarantees";
-
-(*** Additional guarantees laws, by lcp ***)
-
-Goalw [guar_def]
- "[| F: U guarantees V; G: X guarantees Y |] \
-\ ==> F Join G: (U Int X) guarantees (V Int Y)";
-by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
-by (Blast_tac 1);
-qed "guarantees_Join_Int";
-
-Goalw [guar_def]
- "[| F: U guarantees V; G: X guarantees Y |] \
-\ ==> F Join G: (U Un X) guarantees (V Un Y)";
-by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
-by (Blast_tac 1);
-qed "guarantees_Join_Un";
-
-Goal "((JOIN I F) component H) = (ALL i: I. F i component H)";
-by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1);
-by (Blast_tac 1);
-qed "JN_component_iff";
-
-Goalw [guar_def]
- "[| ALL i:I. F i : X i guarantees Y i |] \
-\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
-by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
-by (Blast_tac 1);
-bind_thm ("guarantees_JN_INT", ballI RS result());
-
-Goalw [guar_def]
- "[| ALL i:I. F i : X i guarantees Y i |] \
-\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
-by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
-by (Blast_tac 1);
-bind_thm ("guarantees_JN_UN", ballI RS result());
-
-
-(*** guarantees laws for breaking down the program, by lcp ***)
-
-Goalw [guar_def]
- "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y";
-by (simp_tac (simpset() addsimps [Join_component_iff]) 1);
-by (Blast_tac 1);
-qed "guarantees_Join_I";
-
-Goalw [guar_def]
- "[| i : I; F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
-by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
-by (Blast_tac 1);
-qed "guarantees_JN_I";
-
-
-(*** well-definedness ***)
-
-Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
-by Auto_tac;
-qed "Join_welldef_D1";
-
-Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
-by Auto_tac;
-qed "Join_welldef_D2";
-
-(*** refinement ***)
-
-Goalw [refines_def] "F refines F wrt X";
-by (Blast_tac 1);
-qed "refines_refl";
-
-Goalw [refines_def]
- "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X";
-by Auto_tac;
-qed "refines_trans";
-
-Goalw [strict_ex_prop_def]
- "strict_ex_prop X \
-\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
-by (Blast_tac 1);
-qed "strict_ex_refine_lemma";
-
-Goalw [strict_ex_prop_def]
- "strict_ex_prop X \
-\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
-\ (F: welldef Int X --> G:X)";
-by Safe_tac;
-by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
-by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
-qed "strict_ex_refine_lemma_v";
-
-Goal "[| strict_ex_prop X; \
-\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
-\ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-by (res_inst_tac [("x","SKIP")] allE 1
- THEN assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [refines_def, iso_refines_def,
- strict_ex_refine_lemma_v]) 1);
-qed "ex_refinement_thm";
-
-
-Goalw [strict_uv_prop_def]
- "strict_uv_prop X \
-\ ==> (ALL H. F Join H : X --> G Join H : X) = (F:X --> G:X)";
-by (Blast_tac 1);
-qed "strict_uv_refine_lemma";
-
-Goalw [strict_uv_prop_def]
- "strict_uv_prop X \
-\ ==> (ALL H. F Join H : welldef & F Join H : X --> G Join H : X) = \
-\ (F: welldef Int X --> G:X)";
-by Safe_tac;
-by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
-by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
- simpset()));
-qed "strict_uv_refine_lemma_v";
-
-Goal "[| strict_uv_prop X; \
-\ ALL H. F Join H : welldef Int X --> G Join H : welldef |] \
-\ ==> (G refines F wrt X) = (G iso_refines F wrt X)";
-by (res_inst_tac [("x","SKIP")] allE 1
- THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
- strict_uv_refine_lemma_v]) 1);
-qed "uv_refinement_thm";
+bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
--- a/src/HOL/UNITY/Comp.thy Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Comp.thy Tue Aug 31 15:56:56 1999 +0200
@@ -10,42 +10,13 @@
Comp = Union +
-constdefs
-
- (*Existential and Universal properties. I formalize the two-program
- case, proving equivalence with Chandy and Sanders's n-ary definitions*)
-
- ex_prop :: 'a program set => bool
- "ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X"
-
- strict_ex_prop :: 'a program set => bool
- "strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)"
-
- uv_prop :: 'a program set => bool
- "uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)"
-
- strict_uv_prop :: 'a program set => bool
- "strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))"
+instance
+ program :: (term)ord
- (*Ill-defined programs can arise through "Join"*)
- welldef :: 'a program set
- "welldef == {F. Init F ~= {}}"
-
- component :: ['a program, 'a program] => bool (infixl 50)
- "F component H == EX G. F Join G = H"
+defs
- guar :: ['a program set, 'a program set] => 'a program set
- (infixl "guarantees" 55) (*higher than membership, lower than Co*)
- "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
+ component_def "F <= H == EX G. F Join G = H"
- refines :: ['a program, 'a program, 'a program set] => bool
- ("(3_ refines _ wrt _)" [10,10,10] 10)
- "G refines F wrt X ==
- ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X"
-
- iso_refines :: ['a program, 'a program, 'a program set] => bool
- ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
- "G iso_refines F wrt X ==
- F : welldef Int X --> G : welldef Int X"
+ strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)"
end
--- a/src/HOL/UNITY/Extend.ML Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Tue Aug 31 15:56:56 1999 +0200
@@ -300,8 +300,7 @@
(*Opposite direction fails because Diff in the extended state may remove
fewer actions, i.e. those that affect other state variables.*)
-Goal "Diff (project h G) acts component \
-\ project h (Diff G (extend_act h `` acts))";
+Goal "Diff (project h G) acts <= project h (Diff G (extend_act h `` acts))";
by (force_tac (claset(),
simpset() addsimps [component_eq_subset, Diff_def]) 1);
qed "Diff_project_component_project_Diff";
--- a/src/HOL/UNITY/Extend.thy Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Tue Aug 31 15:56:56 1999 +0200
@@ -8,7 +8,7 @@
function g (forgotten) maps the extended state to the "extending part"
*)
-Extend = Union + Comp +
+Extend = Guar +
constdefs
--- a/src/HOL/UNITY/Lift_prog.ML Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML Tue Aug 31 15:56:56 1999 +0200
@@ -68,12 +68,12 @@
(** These monotonicity results look natural but are UNUSED **)
-Goal "F component G ==> lift_prog i F component lift_prog i G";
+Goal "F <= G ==> lift_prog i F <= lift_prog i G";
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
by Auto_tac;
qed "lift_prog_mono";
-Goal "F component G ==> drop_prog i F component drop_prog i G";
+Goal "F <= G ==> drop_prog i F <= drop_prog i G";
by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1);
by Auto_tac;
qed "drop_prog_mono";
@@ -218,6 +218,8 @@
(*** Diff, needed for localTo ***)
+(** THESE PROOFS CAN BE GENERALIZED AS IN EXTEND.ML **)
+
Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B) \
\ ==> Diff (drop_prog i G) (Acts F) : A co B";
by (auto_tac (claset(),
@@ -382,7 +384,10 @@
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1);
qed "lift_prog_guarantees";
-(*Weak precondition and postcondition; this is the good one!*)
+(*Weak precondition and postcondition; this is the good one!
+CAN WEAKEN 2ND PREMISE TO
+ !!G. extend h F Join G : XX ==> F Join project h G : X;
+*)
val [xguary,drop_prog,lift_prog] =
Goal "[| F : X guarantees Y; \
\ !!H. H : XX ==> drop_prog i H : X; \
--- a/src/HOL/UNITY/Lift_prog.thy Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Tue Aug 31 15:56:56 1999 +0200
@@ -6,7 +6,7 @@
lift_prog, etc: replication of components
*)
-Lift_prog = Union + Comp +
+Lift_prog = Guar +
constdefs
--- a/src/HOL/UNITY/PPROD.ML Mon Aug 30 23:19:13 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML Tue Aug 31 15:56:56 1999 +0200
@@ -40,7 +40,7 @@
by Auto_tac;
qed "PLam_insert";
-Goalw [PLam_def] "i : I ==> (lift_prog i (F i)) component (PLam I F)";
+Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
(*blast_tac doesn't use HO unification*)
by (fast_tac (claset() addIs [component_JN]) 1);
qed "component_PLam";