# HG changeset patch # User paulson # Date 912678306 -3600 # Node ID 1894bfc4aee96c30423d08655c5a70d87833fdc4 # Parent c48050d6928dc73d2036f57233f29bdf2bd1064f Addition of the States component; parts of Comp not working diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Client.ML --- a/src/HOL/UNITY/Client.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Client.ML Thu Dec 03 10:45:06 1998 +0100 @@ -90,7 +90,8 @@ (*** Towards proving the liveness property ***) -Goal "Cli_prg Join G \ +Goal "States Cli_prg = States G \ +\ ==> Cli_prg Join G \ \ : transient {s. size (giv s) = Suc k & \ \ size (rel s) = k & ask s ! k <= giv s ! k}"; by (res_inst_tac [("act", "rel_act")] transient_mem 1); @@ -130,11 +131,13 @@ by (Clarify_tac 1); by (rtac Stable_transient_reachable_LeadsTo 1); by (res_inst_tac [("k", "k")] transient_lemma 2); +be Disjoint_States_eq 2; by (force_tac (claset() addDs [impOfSubs Increasing_size, impOfSubs Increasing_Stable_less], simpset()) 1); by (rtac (make_elim (lemma1 RS guaranteesD)) 1); by (Blast_tac 1); +be Disjoint_States_eq 1; by (auto_tac (claset(), simpset() addsimps [Invariant_eq_always, giv_meets_ask_def])); by (ALLGOALS Force_tac); diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Client.thy --- a/src/HOL/UNITY/Client.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Client.thy Thu Dec 03 10:45:06 1998 +0100 @@ -48,7 +48,8 @@ size (ask s) = size (rel s))}" Cli_prg :: state program - "Cli_prg == mk_program ({s. tok s : atMost Max & + "Cli_prg == mk_program (UNIV, + {s. tok s : atMost Max & giv s = [] & ask s = [] & rel s = []}, diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Common.ML --- a/src/HOL/UNITY/Common.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Common.ML Thu Dec 03 10:45:06 1998 +0100 @@ -30,13 +30,13 @@ (*** Some programs that implement the safety property above ***) -Goal "SKIP : constrains {m} (maxfg m)"; +Goal "SKIP UNIV : constrains {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, fasc]) 1); result(); (*This one is t := ftime t || t := gtime t*) -Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ +Goal "mk_program (UNIV, UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \ \ : constrains {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, fasc]) 1); @@ -44,7 +44,7 @@ result(); (*This one is t := max (ftime t) (gtime t)*) -Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ +Goal "mk_program (UNIV, UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \ \ : constrains {m} (maxfg m)"; by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); @@ -52,7 +52,8 @@ result(); (*This one is t := t+1 if t component F (F Join G)"; by (Blast_tac 1); qed "component_Join1"; -Goalw [component_def] "component G (F Join G)"; +Goalw [component_def] "States F = States G ==> component G (F Join G)"; by (simp_tac (simpset() addsimps [Join_commute]) 1); +by (dtac sym 1); by (Blast_tac 1); qed "component_Join2"; -Goalw [component_def] "i : I ==> component (F i) (JN i:I. (F i))"; -by (blast_tac (claset() addIs [JN_absorb]) 1); +Goalw [component_def, eqStates_def] + "[| i : I; eqStates I F |] ==> component (F i) (JN i:I. (F i))"; +by (force_tac (claset() addIs [JN_absorb], simpset()) 1); qed "component_JN"; Goalw [component_def] "[| component F G; component G H |] ==> component F H"; -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); +by (force_tac (claset() addIs [Join_assoc RS sym], simpset()) 1); qed "component_trans"; -Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G"; -by Auto_tac; +Goalw [component_def] "component F G ==> Acts F <= Acts G"; +by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); qed "component_Acts"; Goalw [component_def,Join_def] "component F G ==> Init G <= Init F"; by Auto_tac; qed "component_Init"; +Goalw [component_def] "component F G ==> States F = States G"; +by Auto_tac; +qed "component_States"; + Goal "[| component F G; component G F |] ==> F=G"; -by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, - component_Acts, component_Init]) 1); +by (blast_tac (claset() addSIs [program_equalityI, component_States, + component_Init, component_Acts]) 1); qed "component_anti_sym"; Goalw [component_def] "component F H = (EX G. F Join G = H & Disjoint F G)"; -by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1); +by (blast_tac (claset() addSIs [Disjoint_States_eq, + Diff_Disjoint, Join_Diff2]) 1); qed "component_eq"; (*** existential properties ***) Goalw [ex_prop_def] - "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X"; + "[| ex_prop X; finite GG |] \ +\ ==> eqStates GG (%x. x) --> GG Int X ~= {} --> (JN G:GG. G) : X"; by (etac finite_induct 1); -by (auto_tac (claset(), simpset() addsimps [Int_insert_left])); +by (Simp_tac 1); +by (rename_tac "GG J" 1); +by (full_simp_tac (simpset() addsimps [Int_insert_left]) 1); +by (dres_inst_tac [("x","J")] spec 1); +by (Force_tac 1); qed_spec_mp "ex1"; Goalw [ex_prop_def] - "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X ==> ex_prop X"; + "ALL GG. finite GG & eqStates GG (%x. x) & 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)"; +Goal "ex_prop X = \ +\ (ALL GG. finite GG & eqStates GG (%x. x) & GG Int X ~= {} \ +\ --> (JN G:GG. G) : X)"; by (blast_tac (claset() addIs [ex1,ex2]) 1); qed "ex_prop_finite"; @@ -88,6 +103,7 @@ by (Blast_tac 1); by Safe_tac; by (stac Join_commute 2); +by (dtac sym 2); by (ALLGOALS Blast_tac); qed "ex_prop_equiv"; @@ -95,13 +111,15 @@ (*** universal properties ***) Goalw [uv_prop_def] - "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X"; + "[| uv_prop X; finite GG |] \ +\ ==> eqStates GG (%x. x) --> 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"; + "ALL GG. finite GG & eqStates GG (%x. x) & 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); @@ -110,7 +128,8 @@ qed "uv2"; (*Chandy & Sanders take this as a definition*) -Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)"; +Goal "uv_prop X = (ALL GG. finite GG & eqStates GG (%x. x) & GG <= X \ +\ --> (JN G:GG. G) : X)"; by (blast_tac (claset() addIs [uv1,uv2]) 1); qed "uv_prop_finite"; @@ -180,7 +199,8 @@ qed "guaranteesI"; Goalw [guarantees_def, component_def] - "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y"; + "[| F : X guarantees Y; F Join G : X; States F = States G |] \ +\ ==> F Join G : Y"; by (Blast_tac 1); qed "guaranteesD"; @@ -203,36 +223,46 @@ Goalw [refines_def] "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; -by (Blast_tac 1); +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)"; + "[| strict_ex_prop X; States F = States G |] \ +\ ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = \ +\ (F:X --> G:X)"; +by Safe_tac; by (Blast_tac 1); +auto(); 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) = \ + "[| strict_ex_prop X; States F = States G |] \ +\ ==> (ALL H. States F = States 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 (eres_inst_tac [("x","SKIP ?A"), ("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 |] \ +Goal "[| strict_ex_prop X; States F = States G; \ +\ ALL H. States F = States 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 +bd sym 1; +by (res_inst_tac [("x","SKIP (States G)")] 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)"; +\ ==> (ALL H. States F = States H & F Join H : X --> G Join H : X) = (F:X --> G:X)"; by (Blast_tac 1); qed "strict_uv_refine_lemma"; @@ -254,3 +284,4 @@ by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, strict_uv_refine_lemma_v]) 1); qed "uv_refinement_thm"; +***) diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Comp.thy Thu Dec 03 10:45:06 1998 +0100 @@ -16,23 +16,29 @@ 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" + "ex_prop X == + ALL F G. (F:X | G: X) & States F = States G --> (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)" + "strict_ex_prop X == + ALL F G. States F = States 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)" + "uv_prop X == + SKIP UNIV : X & + (ALL F G. F:X & G: X & States F = States G --> (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))" + "strict_uv_prop X == + SKIP UNIV : X & + (ALL F G. States F = States G --> (F:X & G: X) = (F Join G : X))" (*Ill-defined programs can arise through "Join"*) welldef :: 'a program set "welldef == {F. Init F ~= {}}" component :: ['a program, 'a program] => bool - "component F H == EX G. F Join G = H" + "component F H == EX G. F Join G = H & States F = States G" guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65) "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}" @@ -40,7 +46,9 @@ 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" + States F = States G & + (ALL H. States F = States 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) diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Constrains.ML Thu Dec 03 10:45:06 1998 +0100 @@ -89,19 +89,27 @@ by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "ball_Constrains_INT"; -Goal "F : Constrains A A' ==> reachable F Int A <= A'"; +Goal "[| F : Constrains A A'; A <= reachable F |] ==> A <= A'"; by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); by (dtac constrains_imp_subset 1); -by (ALLGOALS - (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]))); +by (auto_tac (claset() addIs [impOfSubs reachable_subset_States], + simpset() addsimps [Int_subset_iff, Int_lower1])); qed "Constrains_imp_subset"; Goalw [Constrains_def] "[| F : Constrains A B; F : Constrains B C |] \ \ ==> F : Constrains A C"; -by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); +by (blast_tac (claset() addIs [impOfSubs reachable_subset_States, + constrains_trans, constrains_weaken]) 1); qed "Constrains_trans"; +Goal "[| F : Constrains A (A' Un B); F : Constrains B B' |] \ +\ ==> F : Constrains A (A' Un B')"; +by (asm_full_simp_tac (simpset() addsimps [Constrains_def, Int_Un_distrib]) 1); +by (blast_tac (claset() addIs [impOfSubs reachable_subset_States, + constrains_cancel]) 1); +qed "Constrains_cancel"; + (*** Stable ***) @@ -193,13 +201,6 @@ by (Blast_tac 1); qed "Elimination_sing"; -Goalw [Constrains_def, constrains_def] - "[| F : Constrains A (A' Un B); F : Constrains B B' |] \ -\ ==> F : Constrains A (A' Un B')"; -by (Clarify_tac 1); -by (Blast_tac 1); -qed "Constrains_cancel"; - (*** Specialized laws for handling Invariants ***) diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Handshake.ML --- a/src/HOL/UNITY/Handshake.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Handshake.ML Thu Dec 03 10:45:06 1998 +0100 @@ -11,6 +11,7 @@ (*split_all_tac causes a big blow-up*) claset_ref() := claset() delSWrapper record_split_name; +Addsimps [F_def RS def_prg_States, G_def RS def_prg_States]; Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; program_defs_ref := [F_def, G_def]; @@ -20,7 +21,6 @@ Addsimps (thms"state.update_defs"); Addsimps [simp_of_set invFG_def]; - Goal "(F Join G) : Invariant invFG"; by (rtac InvariantI 1); by (Force_tac 1); @@ -36,12 +36,14 @@ by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (ensures_tac "cmdG" 2); by (constrains_tac 1); +by Auto_tac; qed "lemma2_1"; Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}"; by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (constrains_tac 2); by (ensures_tac "cmdF" 1); +by Auto_tac; qed "lemma2_2"; diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Handshake.thy --- a/src/HOL/UNITY/Handshake.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Handshake.thy Thu Dec 03 10:45:06 1998 +0100 @@ -21,14 +21,14 @@ "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" F :: "state program" - "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})" + "F == mk_program (UNIV, {s. NF s = 0 & BB s}, {cmdF})" (*G's program*) cmdG :: "(state*state) set" "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" G :: "state program" - "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})" + "G == mk_program (UNIV, {s. NG s = 0 & BB s}, {cmdG})" (*the joint invariant*) invFG :: "state set" diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Lift.thy --- a/src/HOL/UNITY/Lift.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Lift.thy Thu Dec 03 10:45:06 1998 +0100 @@ -116,7 +116,8 @@ Lprg :: state program (*for the moment, we OMIT button_press*) - "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s & + "Lprg == mk_program (UNIV, + {s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, {request_act, open_act, close_act, req_up, req_down, move_up, move_down})" diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Mutex.thy --- a/src/HOL/UNITY/Mutex.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Mutex.thy Thu Dec 03 10:45:06 1998 +0100 @@ -52,7 +52,8 @@ "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}" Mprg :: state program - "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, + "Mprg == mk_program (UNIV, + {s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})" diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/NSP_Bad.thy --- a/src/HOL/UNITY/NSP_Bad.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/NSP_Bad.thy Thu Dec 03 10:45:06 1998 +0100 @@ -54,6 +54,6 @@ constdefs Nprg :: state program (*Initial trace is empty*) - "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})" + "Nprg == mk_program(UNIV, {[]}, {Fake, NS1, NS2, NS3})" end diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/PPROD.ML --- a/src/HOL/UNITY/PPROD.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/PPROD.ML Thu Dec 03 10:45:06 1998 +0100 @@ -4,11 +4,6 @@ Copyright 1998 University of Cambridge *) - Addsimps [image_id]; - - -val rinst = read_instantiate_sg (sign_of thy); - (*** General lemmas ***) Goal "x:C ==> (A Times C <= B Times C) = (A <= B)"; @@ -23,9 +18,9 @@ by (Blast_tac 1); qed "Times_Union2"; -Goal "Domain (Union S) = (UN A:S. Domain A)"; -by (Blast_tac 1); -qed "Domain_Union"; + Goal "Domain (Union S) = (UN A:S. Domain A)"; + by (Blast_tac 1); + qed "Domain_Union"; (** RTimes: the product of two relations **) @@ -65,17 +60,6 @@ qed "Image_RTimes"; -Goal "- (UNIV Times A) = UNIV Times (-A)"; -by Auto_tac; -qed "Compl_Times_UNIV1"; - -Goal "- (A Times UNIV) = (-A) Times UNIV"; -by Auto_tac; -qed "Compl_Times_UNIV2"; - -Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; - - (**** Lcopy ****) (*** Basic properties ***) @@ -84,9 +68,9 @@ by (simp_tac (simpset() addsimps [Lcopy_def]) 1); qed "Init_Lcopy"; -Goal "Id : (%act. act RTimes Id) `` Acts F"; +Goal "diag (States F Times UNIV) : (%act. act RTimes diag UNIV) `` Acts F"; by (rtac image_eqI 1); -by (rtac Id_in_Acts 2); +by (rtac diag_in_Acts 2); by Auto_tac; val lemma = result(); @@ -234,7 +218,7 @@ Addsimps [Init_lift_prog]; Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; -by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); +by (auto_tac (claset() addIs [diag_in_Acts RSN (2,image_eqI)], simpset())); qed "Acts_lift_prog"; Goalw [PPROD_def] "Init (PPROD I F) = {f. ALL i:I. f i : Init (F i)}"; diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/PPROD.thy Thu Dec 03 10:45:06 1998 +0100 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -General products of programs (Pi operation). +General products of programs (Pi operation), for replicating components. Also merging of state sets. *) @@ -11,7 +11,7 @@ constdefs (*Cartesian product of two relations*) - RTimes :: "[('a*'a) set, ('b*'b) set] => (('a*'b) * ('a*'b)) set" + RTimes :: "[('a*'b) set, ('c*'d) set] => (('a*'c) * ('b*'d)) set" ("_ RTimes _" [81, 80] 80) "R RTimes S == {((x,y),(x',y')). (x,x'):R & (y,y'):S}" @@ -26,8 +26,9 @@ "fst_act act == (%((x,y),(x',y')). (x,x')) `` act" Lcopy :: "'a program => ('a*'b) program" - "Lcopy F == mk_program (Init F Times UNIV, - (%act. act RTimes Id) `` Acts F)" + "Lcopy F == mk_program (UNIV, + Init F Times UNIV, + (%act. act RTimes (diag UNIV)) `` Acts F)" lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set" "lift_act i act == {(f,f'). EX s'. f' = f(i:=s') & (f i, s') : act}" @@ -36,7 +37,8 @@ "drop_act i act == (%(f,f'). (f i, f' i)) `` act" lift_prog :: "['a, 'b program] => ('a => 'b) program" - "lift_prog i F == mk_program ({f. f i : Init F}, lift_act i `` Acts F)" + "lift_prog i F == + mk_program (UNIV, {f. f i : Init F}, lift_act i `` Acts F)" (*products of programs*) PPROD :: ['a set, 'a => 'b program] => ('a => 'b) program diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/ROOT.ML Thu Dec 03 10:45:06 1998 +0100 @@ -11,6 +11,8 @@ writeln"Root file for HOL/UNITY"; set proof_timing; + + loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*) time_use_thy"UNITY"; @@ -27,7 +29,9 @@ time_use_thy "Lift"; time_use_thy "Comp"; time_use_thy "Client"; -time_use_thy "PPROD"; +(** +time_use_thy "PPX"; +**) loadpath := "../Auth" :: !loadpath; (*to find Public.thy*) use_thy"NSP_Bad"; diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Reach.thy --- a/src/HOL/UNITY/Reach.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Reach.thy Thu Dec 03 10:45:06 1998 +0100 @@ -24,7 +24,7 @@ "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" Rprg :: state program - "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})" + "Rprg == mk_program (UNIV, {%v. v=init}, UN (u,v): edges. {asgt u v})" reach_invariant :: state set "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Traces.ML --- a/src/HOL/UNITY/Traces.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Traces.ML Thu Dec 03 10:45:06 1998 +0100 @@ -12,73 +12,161 @@ (*** The abstract type of programs ***) +Goalw [restrict_rel_def] "restrict_rel A Id = diag A"; +by (Blast_tac 1); +qed "restrict_rel_Id"; +Addsimps [restrict_rel_Id]; + +Goalw [restrict_rel_def] "restrict_rel A (diag B) = diag (A Int B)"; +by (Blast_tac 1); +qed "restrict_rel_diag"; +Addsimps [restrict_rel_diag]; + +Goalw [restrict_rel_def] + "restrict_rel A (restrict_rel B r) = restrict_rel (A Int B) r"; +by (Blast_tac 1); +qed "restrict_rel_restrict_rel"; +Addsimps [restrict_rel_restrict_rel]; + +Goalw [restrict_rel_def] "restrict_rel A r <= A Times A"; +by (Blast_tac 1); +qed "restrict_rel_subset"; +Addsimps [restrict_rel_subset]; + +Goalw [restrict_rel_def] + "((x,y) : restrict_rel A r) = ((x,y): r & x: A & y: A)"; +by (Blast_tac 1); +qed "restrict_rel_iff"; +Addsimps [restrict_rel_iff]; + +Goalw [restrict_rel_def] "r <= A Times A ==> restrict_rel A r = r"; +by (Blast_tac 1); +qed "restrict_rel_eq"; +Addsimps [restrict_rel_eq]; + +Goal "acts <= Pow (A Times A) ==> restrict_rel A `` acts = acts"; +by Auto_tac; +by (rtac image_eqI 1); +by (assume_tac 2); +by (set_mp_tac 1); +by (Force_tac 1); +qed "restrict_rel_image"; + +Goalw [restrict_rel_def] "Domain (restrict_rel A r) <= A Int Domain r"; +by (Blast_tac 1); +qed "Domain_restrict_rel"; + +Goalw [restrict_rel_def] "restrict_rel A r ^^ B <= A Int (r ^^ B)"; +by (Blast_tac 1); +qed "Image_restrict_rel"; + +Addsimps [diag_iff]; + val rep_ss = simpset() addsimps - [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, + [Int_lower1, image_subset_iff, diag_subset_Times, + States_def, Init_def, Acts_def, + mk_program_def, Program_def, Rep_Program, Rep_Program_inverse, Abs_Program_inverse]; -Goal "Id: Acts F"; +(** Basic laws guaranteed by the abstract type "program" **) + +Goal "Init F <= States F"; by (cut_inst_tac [("x", "F")] Rep_Program 1); by (auto_tac (claset(), rep_ss)); -qed "Id_in_Acts"; -AddIffs [Id_in_Acts]; +qed "Init_subset_States"; + +Goal "Acts F <= Pow(States F Times States F)"; +by (cut_inst_tac [("x", "F")] Rep_Program 1); +by (force_tac (claset(),rep_ss) 1); +qed "Acts_subset_Pow_States"; + +Goal "diag (States F) : Acts F"; +by (cut_inst_tac [("x", "F")] Rep_Program 1); +by (auto_tac (claset(), rep_ss)); +qed "diag_in_Acts"; +AddIffs [diag_in_Acts]; -Goal "Init (mk_program (init,acts)) = init"; +(** Inspectors for type "program" **) + +Goal "States (mk_program (states,init,acts)) = states"; +by (auto_tac (claset(), rep_ss)); +qed "States_eq"; + +Goal "Init (mk_program (states,init,acts)) = states Int init"; by (auto_tac (claset(), rep_ss)); qed "Init_eq"; -Goal "Acts (mk_program (init,acts)) = insert Id acts"; +Goal "Acts (mk_program (states,init,acts)) = \ +\ insert (diag states) (restrict_rel states `` acts)"; by (auto_tac (claset(), rep_ss)); +qed "Acts_eq_raw"; + +Goal "acts <= Pow(states Times states) \ +\ ==> Acts (mk_program (states,init,acts)) = insert (diag states) acts"; +by (asm_simp_tac (simpset() addsimps [Acts_eq_raw, restrict_rel_image]) 1); qed "Acts_eq"; -Addsimps [Acts_eq, Init_eq]; +Addsimps [States_eq, Acts_eq, Init_eq]; -Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G"; -by (cut_inst_tac [("p", "Rep_Program F")] surjective_pairing 1); +(** The notation of equality for type "program" **) + +Goal "[| States F = States G; Init F = Init G; Acts F = Acts G |] ==> F = G"; +by (subgoals_tac ["EX x. Rep_Program F = x", + "EX x. Rep_Program G = x"] 1); +by (REPEAT (Blast_tac 2)); +by (Clarify_tac 1); by (auto_tac (claset(), rep_ss)); -by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1); -by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1); +by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1)); +by (asm_full_simp_tac rep_ss 1); qed "program_equalityI"; val [major,minor] = -Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P"; +Goal "[| F = G; \ +\ [| States F = States G; Init F = Init G; Acts F = Acts G |] ==> P \ +\ |] ==> P"; by (rtac minor 1); by (auto_tac (claset(), simpset() addsimps [major])); qed "program_equalityE"; -(*** These rules allow "lazy" definition expansion ***) +(*** These rules allow "lazy" definition expansion + They avoid expanding the full program, which is a large expression +***) -(*The program is not expanded, but its Init is*) -val [rew] = goal thy - "[| F == mk_program (init,acts) |] \ -\ ==> Init F = init"; -by (rewtac rew); +Goal "[| F == mk_program (states,init,acts) |] \ +\ ==> States F = states"; +by Auto_tac; +qed "def_prg_States"; + +Goal "[| F == mk_program (states,init,acts); init <= states |] \ +\ ==> Init F = init"; by Auto_tac; qed "def_prg_Init"; +Goal "[| F == mk_program (states,init,acts); \ +\ acts <= Pow(states Times states) |] \ +\ ==> Acts F = insert (diag states) acts"; +by (asm_simp_tac (simpset() addsimps [restrict_rel_image]) 1); +qed "def_prg_Acts"; + (*The program is not expanded, but its Init and Acts are*) -val [rew] = goal thy - "[| F == mk_program (init,acts) |] \ -\ ==> Init F = init & Acts F = insert Id acts"; -by (rewtac rew); -by Auto_tac; +Goal "[| F == mk_program (states,init,acts); \ +\ init <= states; acts <= Pow(states Times states) |] \ +\ ==> Init F = init & Acts F = insert (diag states) acts"; +by (asm_simp_tac (HOL_ss addsimps [def_prg_Init, def_prg_Acts]) 1); qed "def_prg_simps"; (*An action is expanded only if a pair of states is being tested against it*) -val [rew] = goal thy - "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; -by (rewtac rew); +Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"; by Auto_tac; qed "def_act_simp"; fun simp_of_act def = def RS def_act_simp; (*A set is expanded only if an element is being tested against it*) -val [rew] = goal thy - "A == B ==> (x : A) = (x : B)"; -by (rewtac rew); +Goal "A == B ==> (x : A) = (x : B)"; by Auto_tac; qed "def_set_simp"; @@ -87,6 +175,13 @@ (*** traces and reachable ***) +Goal "reachable F <= States F"; +by Safe_tac; +by (etac reachable.induct 1); +by (blast_tac (claset() addDs [impOfSubs Acts_subset_Pow_States]) 2); +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1); +qed "reachable_subset_States"; + Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"; by Safe_tac; by (etac traces.induct 2); diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Traces.thy --- a/src/HOL/UNITY/Traces.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Traces.thy Thu Dec 03 10:45:06 1998 +0100 @@ -25,17 +25,32 @@ typedef (Program) - 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}" + 'a program = "{(states :: 'a set, + init :: 'a set, + acts :: ('a * 'a)set set). + init <= states & + acts <= Pow(states Times states) & + diag states : acts}" constdefs - mk_program :: "('a set * ('a * 'a)set set) => 'a program" - "mk_program == %(init, acts). Abs_Program (init, insert Id acts)" + restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set" + "restrict_rel A r == (A Times A) Int r" - Init :: "'a program => 'a set" - "Init F == fst (Rep_Program F)" + mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program" + "mk_program == + %(states, init, acts). + Abs_Program (states, + states Int init, + restrict_rel states `` (insert Id acts))" - Acts :: "'a program => ('a * 'a)set set" - "Acts F == snd (Rep_Program F)" + States :: "'a program => 'a set" + "States F == (%(states, init, acts). states) (Rep_Program F)" + + Init :: "'a program => 'a set" + "Init F == (%(states, init, acts). init) (Rep_Program F)" + + Acts :: "'a program => ('a * 'a)set set" + "Acts F == (%(states, init, acts). acts) (Rep_Program F)" consts reachable :: "'a program => 'a set" diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/UNITY.ML Thu Dec 03 10:45:06 1998 +0100 @@ -12,6 +12,29 @@ HOL_quantifiers := false; +(*** General lemmas ***) + + Goal "Pow UNIV = UNIV"; + by (Blast_tac 1); + qed "Pow_UNIV"; + Addsimps [Pow_UNIV]; + +Goal "UNIV Times UNIV = UNIV"; +by Auto_tac; +qed "UNIV_Times_UNIV"; +Addsimps [UNIV_Times_UNIV]; + +Goal "- (UNIV Times A) = UNIV Times (-A)"; +by Auto_tac; +qed "Compl_Times_UNIV1"; + +Goal "- (A Times UNIV) = (-A) Times UNIV"; +by Auto_tac; +qed "Compl_Times_UNIV2"; + +Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; + + (*** constrains ***) overload_1st_set "UNITY.constrains"; @@ -83,16 +106,25 @@ by (Blast_tac 1); qed "ball_constrains_INT"; -Goalw [constrains_def] "[| F : constrains A A' |] ==> A<=A'"; -by (Blast_tac 1); +Goalw [constrains_def] "[| F : constrains A A'; A <= States F |] ==> A <= A'"; +by (Force_tac 1); qed "constrains_imp_subset"; -Goalw [constrains_def] - "[| F : constrains A B; F : constrains B C |] \ +(*The reasoning is by subsets since "constrains" refers to single actions + only. So this rule isn't that useful.*) +Goal "[| F : constrains A B; F : constrains B C; B <= States F |] \ \ ==> F : constrains A C"; -by (Blast_tac 1); +by (etac constrains_weaken_R 1); +by (etac constrains_imp_subset 1); +by (assume_tac 1); qed "constrains_trans"; +Goal "[| F : constrains A (A' Un B); F : constrains B B'; B <= States F|] \ +\ ==> F : constrains A (A' Un B')"; +by (etac constrains_weaken_R 1); +by (blast_tac (claset() addDs [impOfSubs constrains_imp_subset]) 1); +qed "constrains_cancel"; + (*** stable ***) @@ -212,14 +244,6 @@ qed "elimination_sing"; -Goalw [constrains_def] - "[| F : constrains A (A' Un B); F : constrains B B' |] \ -\ ==> F : constrains A (A' Un B')"; -by (Clarify_tac 1); -by (Blast_tac 1); -qed "constrains_cancel"; - - (*** Theoretical Results from Section 6 ***) diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Union.ML Thu Dec 03 10:45:06 1998 +0100 @@ -8,55 +8,124 @@ From Misra's Chapter 5: Asynchronous Compositions of Programs *) +Goal "k:I ==> (INT i:I. A i) Int A k = (INT i:I. A i)"; +by (Blast_tac 1); +qed "INT_absorb2"; + + +val rinst = read_instantiate_sg (sign_of thy); + +Addcongs [UN_cong, INT_cong]; (** SKIP **) -Goal "Init SKIP = UNIV"; +Goal "States (SKIP A) = A"; +by (simp_tac (simpset() addsimps [SKIP_def]) 1); +qed "States_SKIP"; + +Goal "Init (SKIP A) = A"; by (simp_tac (simpset() addsimps [SKIP_def]) 1); qed "Init_SKIP"; -Goal "Acts SKIP = {Id}"; +Goal "Acts (SKIP A) = {diag A}"; by (simp_tac (simpset() addsimps [SKIP_def]) 1); qed "Acts_SKIP"; -Addsimps [Init_SKIP, Acts_SKIP]; +Addsimps [States_SKIP, Init_SKIP, Acts_SKIP]; -Goal "reachable SKIP = UNIV"; -by (force_tac (claset() addIs reachable.intrs, simpset()) 1); +Goal "reachable (SKIP A) = A"; +by (force_tac (claset() addEs [reachable.induct] + addIs reachable.intrs, simpset()) 1); qed "reachable_SKIP"; Addsimps [reachable_SKIP]; -(** Join and JN **) +(** Join **) + +Goal "States (F Join G) = States F Int States G"; +by (simp_tac (simpset() addsimps [Join_def]) 1); +qed "States_Join"; Goal "Init (F Join G) = Init F Int Init G"; -by (simp_tac (simpset() addsimps [Join_def]) 1); +by (auto_tac (claset() addIs [impOfSubs Init_subset_States], + simpset() addsimps [Join_def])); qed "Init_Join"; -Goal "Acts (F Join G) = Acts F Un Acts G"; +Goal "States F = States G ==> Acts (F Join G) = Acts F Un Acts G"; +by (subgoal_tac "Acts F Un Acts G <= Pow (States G Times States G)" 1); +by (blast_tac (claset() addEs [equalityE] + addDs [impOfSubs Acts_subset_Pow_States]) 2); by (auto_tac (claset(), simpset() addsimps [Join_def])); qed "Acts_Join"; + +(** JN **) + +Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = (SKIP UNIV)"; +by Auto_tac; +qed "JN_empty"; +Addsimps [JN_empty]; + +Goal "States (JN i:I. F i) = (INT i:I. States (F i))"; +by (simp_tac (simpset() addsimps [JOIN_def]) 1); +qed "States_JN"; + Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))"; -by (simp_tac (simpset() addsimps [JOIN_def]) 1); +by (auto_tac (claset() addIs [impOfSubs Init_subset_States], + simpset() addsimps [JOIN_def])); qed "Init_JN"; -Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"; +Goalw [eqStates_def] + "[| i: I; eqStates I F |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))"; +by (Clarify_tac 1); +by (subgoal_tac "(UN i:I. Acts (F i)) <= Pow (St Times St)" 1); +by (blast_tac (claset() addEs [equalityE] + addDs [impOfSubs Acts_subset_Pow_States]) 2); by (auto_tac (claset(), simpset() addsimps [JOIN_def])); qed "Acts_JN"; -Addsimps [Init_Join, Init_JN]; +Goal "eqStates I F \ +\ ==> Acts (JN i:I. F i) = \ +\ (if I={} then {diag UNIV} else (UN i:I. Acts (F i)))"; +by (force_tac (claset(), simpset() addsimps [Acts_JN]) 1); +qed "Acts_JN_if"; + +Addsimps [States_Join, Init_Join, States_JN, Init_JN]; + -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP"; -by Auto_tac; -qed "JN_empty"; +Goal "(JN x:insert j I. F x) = (F j) Join (JN x:I. F x)"; +by (rtac program_equalityI 1); +by (ALLGOALS Asm_simp_tac); +by (asm_simp_tac + (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw, + image_UNION, image_Un, image_image, Int_assoc]) 1); +qed "JN_insert"; +Addsimps[JN_insert]; -Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)"; -by (rtac program_equalityI 1); -by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def]))); -qed "JN_insert"; -Addsimps[JN_empty, JN_insert]; +Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)"; +by (stac (JN_insert RS sym) 1); +by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); +qed "JN_absorb"; + + +Goalw [eqStates_def] "eqStates {} F"; +by (Simp_tac 1); +qed "eqStates_empty"; + +Goalw [eqStates_def] + "[| eqStates I F; States (F i) = (INT i: I. States (F i)) |] \ +\ ==> eqStates (insert i I) F"; +by Auto_tac; +qed "eqStates_insertI"; + +Goalw [eqStates_def] + "eqStates (insert i I) F = \ +\ (eqStates I F & (I={} | States (F i) = (INT i: I. States (F i))))"; +by Auto_tac; +qed "eqStates_insert_eq"; + +Addsimps [eqStates_empty, eqStates_insert_eq]; (** Algebraic laws **) @@ -66,170 +135,224 @@ qed "Join_commute"; Goal "(F Join G) Join H = F Join (G Join H)"; -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1); +by (rtac program_equalityI 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps Un_ac@[Int_assoc]))); +by (asm_simp_tac + (simpset() addsimps Un_ac@Int_ac@[Join_def, Acts_eq_raw, + image_Un, image_image]) 1); +by (Blast_tac 1); qed "Join_assoc"; -Goalw [Join_def, SKIP_def] "SKIP Join F = F"; +Goalw [Join_def, SKIP_def] "States F <= A ==> (SKIP A) Join F = F"; by (rtac program_equalityI 1); -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); +by (ALLGOALS + (asm_simp_tac (simpset() addsimps + Int_ac@[Acts_subset_Pow_States RS restrict_rel_image, + Acts_eq_raw, insert_absorb, Int_absorb1]))); +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1); qed "Join_SKIP_left"; -Goalw [Join_def, SKIP_def] "F Join SKIP = F"; -by (rtac program_equalityI 1); -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); +Goal "States F <= A ==> F Join (SKIP A) = F"; +by (stac Join_commute 1); +by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1); qed "Join_SKIP_right"; Addsimps [Join_SKIP_left, Join_SKIP_right]; Goalw [Join_def] "F Join F = F"; by (rtac program_equalityI 1); -by Auto_tac; +by (ALLGOALS + (asm_simp_tac (simpset() addsimps + [insert_absorb, Acts_subset_Pow_States RS Acts_eq]))); +by (blast_tac (claset() addIs [impOfSubs Init_subset_States]) 1); qed "Join_absorb"; Addsimps [Join_absorb]; - -Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)"; -by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [Acts_JN, Acts_Join])); -qed "JN_Join_miniscope"; - -Goal "k:I ==> A k Join (JN i:I. A i) = (JN i:I. A i)"; -by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [Acts_JN, Acts_Join])); -qed "JN_absorb"; - Goal "(JN i: I Un J. A i) = ((JN i: I. A i) Join (JN i:J. A i))"; -by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [Acts_JN, Acts_Join])); +by (rtac program_equalityI 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Un]))); +by (asm_simp_tac + (simpset() addsimps Int_ac@ + [JOIN_def, Join_def, Acts_eq_raw, UN_Un, INT_Un, + image_UNION, image_Un, image_image]) 1); qed "JN_Join"; Goal "i: I ==> (JN i:I. c) = c"; by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [Acts_JN])); + simpset() addsimps [Acts_JN, eqStates_def])); qed "JN_constant"; Goal "(JN i:I. A i Join B i) = (JN i:I. A i) Join (JN i:I. B i)"; -by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [Acts_JN, Acts_Join])); +by (rtac program_equalityI 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [INT_Int_distrib]))); +by (asm_simp_tac + (simpset() addsimps [JOIN_def, Join_def, Acts_eq_raw, image_UNION, + rinst [("A","%x. States (A x) Int States (B x)")] + INT_absorb2, + image_Un, image_image]) 1); +by (asm_simp_tac (simpset() addsimps [INT_Int_distrib RS sym] @ Int_ac) 1); +by (Blast_tac 1); qed "JN_Join_distrib"; +Goal "i : I ==> (JN i:I. A i Join B) = ((JN i:I. A i) Join B)"; +by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1); +qed "JN_Join_miniscope"; + (*** Safety: constrains, stable, FP ***) -Goalw [constrains_def, JOIN_def] - "i : I ==> \ -\ (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "constrains_JN"; +Goal "[| F : constrains A B; G : constrains A B |] \ +\ ==> F Join G : constrains A B"; +by (auto_tac (claset(), + simpset() addsimps [constrains_def, Join_def, Acts_eq_raw, + image_Un])); +by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1)); +qed "constrains_imp_Join_constrains"; -Goal "F Join G : constrains A B = \ -\ (F : constrains A B & G : constrains A B)"; -by (auto_tac - (claset(), - simpset() addsimps [constrains_def, Join_def])); +Goal "States F = States G ==> \ +\ F Join G : constrains A B = (F : constrains A B & G : constrains A B)"; +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join])); qed "constrains_Join"; -(**FAILS, I think; see 5.4.1, Substitution Axiom. - The problem is to relate reachable (F Join G) with - reachable F and reachable G +Goal "[| i : I; ALL i:I. F i : constrains A B |] \ +\ ==> (JN i:I. F i) : constrains A B"; +by (full_simp_tac (simpset() addsimps [constrains_def, JOIN_def, Acts_eq_raw, + image_Un]) 1); +by Safe_tac; +by (REPEAT (force_tac (claset() addSEs [ballE], simpset()) 1)); +qed "constrains_imp_JN_constrains"; -Goalw [Constrains_def] - "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)"; -by (simp_tac (simpset() addsimps [constrains_JN]) 1); -by (Blast_tac 1); -qed "Constrains_JN"; +Goal "[| i : I; eqStates I F |] \ +\ ==> (JN i:I. F i) : constrains A B = (ALL i:I. F i : constrains A B)"; +by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_JN])); +qed "constrains_JN"; + + (**FAILS, I think; see 5.4.1, Substitution Axiom. + The problem is to relate reachable (F Join G) with + reachable F and reachable G -Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)"; -by (auto_tac - (claset(), - simpset() addsimps [Constrains_def, constrains_Join])); -qed "Constrains_Join"; -**) + Goalw [Constrains_def] + "(JN i:I. F i) : Constrains A B = (ALL i:I. F i : Constrains A B)"; + by (simp_tac (simpset() addsimps [constrains_JN]) 1); + by (Blast_tac 1); + qed "Constrains_JN"; -Goal "[| F : constrains A A'; G : constrains B B' |] \ + Goal "F Join G : Constrains A B = (Constrains F A B & Constrains G A B)"; + by (auto_tac + (claset(), + simpset() addsimps [Constrains_def, constrains_Join])); + qed "Constrains_Join"; + **) + +Goal "[| F : constrains A A'; G : constrains B B'; States F = States G |] \ \ ==> F Join G : constrains (A Int B) (A' Un B')"; -by (simp_tac (simpset() addsimps [constrains_Join]) 1); +by (asm_simp_tac (simpset() addsimps [constrains_Join]) 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "constrains_Join_weaken"; -Goal "i : I ==> \ -\ (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"; +Goal "[| i : I; eqStates I F |] \ +\ ==> (JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"; by (asm_simp_tac (simpset() addsimps [stable_def, constrains_JN]) 1); qed "stable_JN"; -Goal "[| ALL i:I. F i : invariant A; i : I |] \ +Goal "[| ALL i:I. F i : invariant A; i : I; eqStates I F |] \ \ ==> (JN i:I. F i) : invariant A"; by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_JN]) 1); by (Blast_tac 1); bind_thm ("invariant_JN_I", ballI RS result()); -Goal "F Join G : stable A = \ -\ (F : stable A & G : stable A)"; -by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); +Goal "States F = States G \ +\ ==> F Join G : stable A = (F : stable A & G : stable A)"; +by (asm_simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1); qed "stable_Join"; -Goal "[| F : invariant A; G : invariant A |] \ +Goal "[| F : invariant A; G : invariant A; States F = States G |] \ \ ==> F Join G : invariant A"; -by (full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1); +by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Join]) 1); by (Blast_tac 1); qed "invariant_JoinI"; -Goal "i : I ==> FP (JN i:I. F i) = (INT i:I. FP (F i))"; +Goal "[| i : I; eqStates I F |] \ +\ ==> FP (JN i:I. F i) = (INT i:I. FP (F i))"; by (asm_simp_tac (simpset() addsimps [FP_def, stable_JN, INTER_def]) 1); qed "FP_JN"; (*** Progress: transient, ensures ***) -Goal "i : I ==> \ -\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"; -by (auto_tac (claset(), - simpset() addsimps [transient_def, JOIN_def])); + +Goal "[| (JN i:I. F i) : transient A; i: I |] ==> EX i:I. F i : transient A"; +by (full_simp_tac (simpset() addsimps [transient_def, JOIN_def, Acts_eq_raw, + Int_absorb1, restrict_rel_def]) 1); +by Safe_tac; +by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1)); +qed "transient_JN_imp_transient"; + +Goal "[| i : I; eqStates I F |] \ +\ ==> (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"; +by (auto_tac (claset() addSIs [transient_JN_imp_transient], simpset())); +by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_JN])); qed "transient_JN"; -Goal "F Join G : transient A = \ -\ (F : transient A | G : transient A)"; -by (auto_tac (claset(), - simpset() addsimps [bex_Un, transient_def, - Join_def])); +Goal "F Join G : transient A ==> \ +\ F : transient A | G : transient A"; +by (full_simp_tac (simpset() addsimps [transient_def, Join_def, Acts_eq_raw, + restrict_rel_def]) 1); +by Safe_tac; +(*delete act:Acts F possibility*) +by (rtac FalseE 3); +(*delete act:Acts G possibility*) +by (thin_tac "~ (EX act:Acts G. ?P act)" 2); +by (REPEAT (blast_tac (claset() addSIs [rev_bexI]) 1)); +qed "transient_Join_imp_transient"; + +Goal "States F = States G \ +\ ==> (F Join G : transient A) = (F : transient A | G : transient A)"; +by (auto_tac (claset() addSIs [transient_Join_imp_transient], simpset())); +by (auto_tac (claset(), simpset() addsimps [transient_def, Acts_Join])); qed "transient_Join"; -Goal "i : I ==> \ -\ (JN i:I. F i) : ensures A B = \ -\ ((ALL i:I. F i : constrains (A-B) (A Un B)) & \ -\ (EX i:I. F i : ensures A B))"; +Goal "[| i : I; eqStates I F |] \ +\ ==> (JN i:I. F i) : ensures A B = \ +\ ((ALL i:I. F i : constrains (A-B) (A Un B)) & \ +\ (EX i:I. F i : ensures A B))"; by (auto_tac (claset(), simpset() addsimps [ensures_def, constrains_JN, transient_JN])); qed "ensures_JN"; Goalw [ensures_def] - "F Join G : ensures A B = \ -\ (F : constrains (A-B) (A Un B) & \ -\ G : constrains (A-B) (A Un B) & \ -\ (F : ensures A B | G : ensures A B))"; + "States F = States G \ +\ ==> F Join G : ensures A B = \ +\ (F : constrains (A-B) (A Un B) & \ +\ G : constrains (A-B) (A Un B) & \ +\ (F : ensures A B | G : ensures A B))"; by (auto_tac (claset(), simpset() addsimps [constrains_Join, transient_Join])); qed "ensures_Join"; -Goalw [stable_def, constrains_def, Join_def] - "[| F : stable A; G : constrains A A' |] \ +Goal "[| F : stable A; G : constrains A A'; \ +\ States F = States G; A <= States G |] \ \ ==> F Join G : constrains A A'"; -by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); +by (forward_tac [constrains_imp_subset] 1); +by (assume_tac 1); +by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, + ball_Un, Acts_Join]) 1); by (Blast_tac 1); qed "stable_constrains_Join"; (*Premise for G cannot use Invariant because Stable F A is weaker than G : stable A *) -Goal "[| F : stable A; G : invariant A |] ==> F Join G : Invariant A"; -by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, - Stable_eq_stable, stable_Join]) 1); +Goal "[| F : stable A; G : invariant A; \ +\ States F = States G |] ==> F Join G : Invariant A"; +by (asm_full_simp_tac (simpset() addsimps [Invariant_def, invariant_def, + Stable_eq_stable, stable_Join]) 1); by (force_tac(claset() addIs [stable_reachable, stable_Int], simpset() addsimps [Acts_Join]) 1); qed "stable_Join_Invariant"; -Goal "[| F : stable A; G : ensures A B |] ==> F Join G : ensures A B"; +Goal "[| F : stable A; G : ensures A B; \ +\ States F = States G |] ==> F Join G : ensures A B"; by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1); by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); by (etac constrains_weaken 1); @@ -237,35 +360,61 @@ qed "ensures_stable_Join1"; (*As above, but exchanging the roles of F and G*) -Goal "[| F : ensures A B; G : stable A |] ==> F Join G : ensures A B"; +Goal "[| F : ensures A B; G : stable A; \ +\ States F = States G |] ==> F Join G : ensures A B"; by (stac Join_commute 1); +by (dtac sym 1); by (blast_tac (claset() addIs [ensures_stable_Join1]) 1); qed "ensures_stable_Join2"; (** Diff and localTo **) -Goalw [Join_def, Diff_def] "F Join (Diff G (Acts F)) = F Join G"; + +Goal "States (Diff F acts) = States F"; +by (simp_tac (simpset() addsimps [Diff_def]) 1); +qed "States_Diff"; + +Goal "Init (Diff F acts) = Init F"; +by (auto_tac (claset() addIs [impOfSubs Init_subset_States], + simpset() addsimps [Diff_def])); +qed "Init_Diff"; + +Goal "Acts (Diff F acts) = insert (diag (States F)) (Acts F - acts)"; +by (subgoal_tac "Acts F - acts <= Pow (States F Times States F)" 1); +by (blast_tac (claset() addEs [equalityE] + addDs [impOfSubs Acts_subset_Pow_States]) 2); +by (auto_tac (claset(), simpset() addsimps [Diff_def])); +qed "Acts_Diff"; + +Addsimps [States_Diff, Init_Diff, Acts_Diff]; + + +Goalw [Join_def] "States F = States G ==> F Join (Diff G (Acts F)) = F Join G"; by (rtac program_equalityI 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [insert_absorb])); qed "Join_Diff2"; -Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))"; +Goalw [Disjoint_def] "States F = States G ==> Disjoint F (Diff G (Acts F))"; by Auto_tac; qed "Diff_Disjoint"; +Goalw [Disjoint_def] "Disjoint F G ==> States F = States G"; +by Auto_tac; +qed "Disjoint_States_eq"; + Goal "[| F Join G : v localTo F; Disjoint F G |] \ \ ==> G : (INT z. stable {s. v s = z})"; by (asm_full_simp_tac - (simpset() addsimps [localTo_def, Diff_def, Disjoint_def, + (simpset() addsimps [localTo_def, Disjoint_def, Acts_Join, stable_def, constrains_def]) 1); by (Blast_tac 1); qed "localTo_imp_stable"; Goal "[| F Join G : v localTo F; (s,s') : act; \ -\ act : Acts G; Disjoint F G |] ==> v s' = v s"; +\ act : Acts G; Disjoint F G |] ==> v s' = v s"; by (asm_full_simp_tac - (simpset() addsimps [localTo_def, Diff_def, Disjoint_def, + (simpset() addsimps [localTo_def, Disjoint_def, Acts_Join, stable_def, constrains_def]) 1); by (Blast_tac 1); qed "localTo_imp_equals"; @@ -284,9 +433,15 @@ \ F Join G : w localTo F; \ \ Disjoint F G |] \ \ ==> F Join G : constrains {s. P (v s) (w s)} {s. P' (v s) (w s)}"; -by (auto_tac (claset(), simpset() addsimps [constrains_def, Acts_Join])); +by (auto_tac (claset(), + simpset() addsimps [constrains_def, + Disjoint_States_eq RS Acts_Join])); by (REPEAT_FIRST (dtac localTo_imp_equals THEN' REPEAT1 o atac)); -by Auto_tac; +by (subgoal_tac "xa : States F" 1); +by (force_tac + (claset() addSDs [Disjoint_States_eq,impOfSubs Acts_subset_Pow_States], + simpset()) 2); +by (Force_tac 1); qed "constrains_localTo_constrains2"; Goalw [stable_def] @@ -316,7 +471,8 @@ by (rtac ballI 1); by (subgoal_tac "F Join G : constrains ({s. v s = k} Int {s. v s <= w s}) \ \ ({s. v s = k} Un {s. v s <= w s})" 1); -by (asm_simp_tac (simpset() addsimps [constrains_Join]) 2); +by (asm_simp_tac + (simpset() addsimps [Disjoint_States_eq RS constrains_Join]) 2); by (blast_tac (claset() addIs [constrains_weaken]) 2); by (dtac (constrains_imp_Constrains RS Constrains_Int) 1 THEN etac INT_D 1); by (etac Constrains_weaken 2); diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/Union.thy Thu Dec 03 10:45:06 1998 +0100 @@ -11,25 +11,33 @@ Union = SubstAx + FP + constdefs + eqStates :: ['a set, 'a => 'b program] => bool + "eqStates I F == EX St. ALL i:I. States (F i) = St" + JOIN :: ['a set, 'a => 'b program] => 'b program - "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))" + "JOIN I F == mk_program (INT i:I. States (F i), + INT i:I. Init (F i), + UN i:I. Acts (F i))" Join :: ['a program, 'a program] => 'a program (infixl 65) - "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)" + "F Join G == mk_program (States F Int States G, + Init F Int Init G, + Acts F Un Acts G)" - SKIP :: 'a program - "SKIP == mk_program (UNIV, {})" + SKIP :: 'a set => 'a program + "SKIP states == mk_program (states, states, {})" Diff :: "['a program, ('a * 'a)set set] => 'a program" - "Diff F acts == mk_program (Init F, Acts F - acts)" + "Diff F acts == mk_program (States F, Init F, Acts F - acts)" (*The set of systems that regard "v" as local to F*) localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80) "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}" - (*Two programs with disjoint actions, except for Id (idling)*) + (*Two programs with disjoint actions, except for identity actions *) Disjoint :: ['a program, 'a program] => bool - "Disjoint F G == Acts F Int Acts G <= {Id}" + "Disjoint F G == States F = States G & + Acts F Int Acts G <= {diag (States G)}" syntax "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Wed Dec 02 16:14:09 1998 +0100 +++ b/src/HOL/UNITY/WFair.ML Thu Dec 03 10:45:06 1998 +0100 @@ -8,6 +8,10 @@ From Misra, "A Logic for Concurrent Programming", 1994 *) + Goal "[| x:A; P(x) |] ==> ? x:A. P(x)"; + by (Blast_tac 1); + qed "rev_bexI"; + overload_1st_set "WFair.transient"; overload_1st_set "WFair.ensures"; @@ -23,8 +27,7 @@ Goalw [transient_def] "[| F : transient A; B<=A |] ==> F : transient B"; by (Clarify_tac 1); -by (rtac bexI 1 THEN assume_tac 2); -by (Blast_tac 1); +by (blast_tac (claset() addSIs [rev_bexI]) 1); qed "transient_strengthen"; Goalw [transient_def]