# HG changeset patch # User paulson # Date 930127175 -7200 # Node ID 56e08e2649617e1d7c78a1f77ecc98424897f412 # Parent 5a557122bb62eb46b9dd333d6c12a4979bf4ede0 renamed PPI to plam simplified the definition of lift_act diff -r 5a557122bb62 -r 56e08e264961 src/HOL/UNITY/PPROD.ML --- a/src/HOL/UNITY/PPROD.ML Wed Jun 23 10:38:49 1999 +0200 +++ b/src/HOL/UNITY/PPROD.ML Wed Jun 23 10:39:35 1999 +0200 @@ -31,6 +31,9 @@ Goalw [lift_act_def] "lift_act i Id = Id"; by Auto_tac; +be rev_mp 1; +bd sym 1; +by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1); qed "lift_act_Id"; Addsimps [lift_act_Id]; @@ -110,10 +113,32 @@ by (rtac lift_set_inverse 1); qed "inj_lift_set"; +(*Because A and B could differ outside i, cannot generalize result to + drop_set i (A Int B) = drop_set i A Int drop_set i B +*) +Goalw [lift_set_def, drop_set_def] + "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; +by Auto_tac; +qed "drop_set_lift_set_Int"; + +Goalw [lift_set_def, drop_set_def] + "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A"; +by Auto_tac; +qed "drop_set_lift_set_Int2"; + +Goalw [drop_set_def] + "i : I ==> drop_set i (INT j:I. lift_set j A) = A"; +by Auto_tac; +qed "drop_set_INT"; + Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act"; by Auto_tac; -by (REPEAT_FIRST (resolve_tac [exI, conjI])); -by Auto_tac; +by (res_inst_tac [("x", "f(i:=a)")] exI 1); +by (Asm_simp_tac 1); +by (res_inst_tac [("x", "f(i:=b)")] exI 1); +by (Asm_simp_tac 1); +br ext 1; +by (Asm_simp_tac 1); qed "lift_act_inverse"; Addsimps [lift_act_inverse]; @@ -136,43 +161,47 @@ qed "inj_lift_prog"; -(** PPROD **) +(** PLam **) -Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))"; +Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"; by Auto_tac; -qed "Init_PPROD"; -Addsimps [Init_PPROD]; +qed "Init_PLam"; +Addsimps [Init_PLam]; +(*For compatibility with the original definition and perhaps simpler proofs*) Goalw [lift_act_def] "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; -by (Blast_tac 1); +by Auto_tac; +br exI 1; +by Auto_tac; qed "lift_act_eq"; AddIffs [lift_act_eq]; -Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; + +Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; by (auto_tac (claset(), - simpset() addsimps [PPROD_def, Acts_JN])); -qed "Acts_PPROD"; + simpset() addsimps [PLam_def, Acts_JN])); +qed "Acts_PLam"; -Goal "PPROD {} F = SKIP"; -by (simp_tac (simpset() addsimps [PPROD_def]) 1); -qed "PPROD_empty"; +Goal "PLam {} F = SKIP"; +by (simp_tac (simpset() addsimps [PLam_def]) 1); +qed "PLam_empty"; -Goal "(PPI i: I. SKIP) = SKIP"; -by (simp_tac (simpset() addsimps [PPROD_def,lift_prog_SKIP,JN_constant]) 1); -qed "PPROD_SKIP"; +Goal "(plam i: I. SKIP) = SKIP"; +by (simp_tac (simpset() addsimps [PLam_def,lift_prog_SKIP,JN_constant]) 1); +qed "PLam_SKIP"; -Addsimps [PPROD_SKIP, PPROD_empty]; +Addsimps [PLam_SKIP, PLam_empty]; -Goalw [PPROD_def] - "PPROD (insert i I) F = (lift_prog i (F i)) Join (PPROD I F)"; +Goalw [PLam_def] + "PLam (insert i I) F = (lift_prog i (F i)) Join (PLam I F)"; by Auto_tac; -qed "PPROD_insert"; +qed "PLam_insert"; -Goalw [PPROD_def] "i : I ==> (lift_prog i (F i)) component (PPROD I F)"; +Goalw [PLam_def] "i : I ==> (lift_prog i (F i)) component (PLam I F)"; (*blast_tac doesn't use HO unification*) by (fast_tac (claset() addIs [component_JN]) 1); -qed "component_PPROD"; +qed "component_PLam"; (*** Safety: co, stable, invariant ***) @@ -219,19 +248,19 @@ neq_imp_lift_prog_stable RS stable_imp_Stable); -(** Safety and PPROD **) +(** Safety and PLam **) Goal "i : I ==> \ -\ (PPROD I F : (lift_set i A) co (lift_set i B)) = \ +\ (PLam I F : (lift_set i A) co (lift_set i B)) = \ \ (F i : A co B)"; -by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); +by (asm_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1); by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, constrains_imp_lift_prog_constrains]) 1); -qed "PPROD_constrains"; +qed "PLam_constrains"; -Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)"; -by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); -qed "PPROD_stable"; +Goal "i : I ==> (PLam I F : stable (lift_set i A)) = (F i : stable A)"; +by (asm_simp_tac (simpset() addsimps [stable_def, PLam_constrains]) 1); +qed "PLam_stable"; (** Safety, lift_prog + drop_set **) @@ -244,51 +273,50 @@ simpset()) 1); qed "lift_prog_constrains_projection"; -Goal "[| PPROD I F : AA co BB; i: I |] \ +Goal "[| PLam I F : AA co BB; i: I |] \ \ ==> F i : (drop_set i AA) co (drop_set i BB)"; by (rtac lift_prog_constrains_projection 1); (*rotate this assumption to be last*) -by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); -by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); -qed "PPROD_constrains_projection"; +by (dres_inst_tac [("psi", "PLam I F : ?C")] asm_rl 1); +by (asm_full_simp_tac (simpset() addsimps [PLam_def, constrains_JN]) 1); +qed "PLam_constrains_projection"; (** invariant **) -(*UNUSED*) Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)"; by (auto_tac (claset(), simpset() addsimps [invariant_def, lift_prog_stable_eq])); qed "lift_prog_invariant_eq"; Goal "[| F i : invariant A; i : I |] \ -\ ==> PPROD I F : invariant (lift_set i A)"; +\ ==> PLam I F : invariant (lift_set i A)"; by (auto_tac (claset(), - simpset() addsimps [invariant_def, PPROD_stable])); -qed "invariant_imp_PPROD_invariant"; + simpset() addsimps [invariant_def, PLam_stable])); +qed "invariant_imp_PLam_invariant"; (*The f0 premise ensures that the product is well-defined.*) -Goal "[| PPROD I F : invariant (lift_set i A); i : I; \ -\ f0: Init (PPROD I F) |] ==> F i : invariant A"; +Goal "[| PLam I F : invariant (lift_set i A); i : I; \ +\ f0: Init (PLam I F) |] ==> F i : invariant A"; by (auto_tac (claset(), - simpset() addsimps [invariant_def, PPROD_stable])); + simpset() addsimps [invariant_def, PLam_stable])); by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); by Auto_tac; -qed "PPROD_invariant_imp_invariant"; +qed "PLam_invariant_imp_invariant"; -Goal "[| i : I; f0: Init (PPROD I F) |] \ -\ ==> (PPROD I F : invariant (lift_set i A)) = (F i : invariant A)"; -by (blast_tac (claset() addIs [invariant_imp_PPROD_invariant, - PPROD_invariant_imp_invariant]) 1); -qed "PPROD_invariant"; +Goal "[| i : I; f0: Init (PLam I F) |] \ +\ ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"; +by (blast_tac (claset() addIs [invariant_imp_PLam_invariant, + PLam_invariant_imp_invariant]) 1); +qed "PLam_invariant"; (*The f0 premise isn't needed if F is a constant program because then we get an initial state by replicating that of F*) Goal "i : I \ -\ ==> ((PPI x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; +\ ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; by (auto_tac (claset(), - simpset() addsimps [invariant_def, PPROD_stable])); -qed "PFUN_invariant"; + simpset() addsimps [invariant_def, PLam_stable])); +qed "const_PLam_invariant"; (*** Substitution Axiom versions: Co, Stable ***) @@ -330,163 +358,150 @@ qed "lift_prog_Stable_eq"; -(** Reachability for PPROD **) +(** Reachability for PLam **) -Goal "[| f : reachable (PPROD I F); i : I |] ==> f i : reachable (F i)"; +Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)"; by (etac reachable.induct 1); by (auto_tac (claset() addIs reachable.intrs, - simpset() addsimps [Acts_PPROD])); -qed "reachable_PPROD"; + simpset() addsimps [Acts_PLam])); +qed "reachable_PLam"; -Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable (F i)}"; -by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1); -qed "reachable_PPROD_subset1"; +(*Result to justify a re-organization of this file*) +Goal "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"; +auto(); +result(); + +Goal "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"; +by (force_tac (claset() addSDs [reachable_PLam], simpset()) 1); +qed "reachable_PLam_subset1"; (*simplify using reachable_lift_prog??*) Goal "[| i ~: I; A : reachable (F i) |] \ -\ ==> ALL f. f : reachable (PPROD I F) \ -\ --> f(i:=A) : reachable (lift_prog i (F i) Join PPROD I F)"; +\ ==> ALL f. f : reachable (PLam I F) \ +\ --> f(i:=A) : reachable (lift_prog i (F i) Join PLam I F)"; by (etac reachable.induct 1); by (ALLGOALS Clarify_tac); by (etac reachable.induct 1); (*Init, Init case*) by (force_tac (claset() addIs reachable.intrs, simpset()) 1); -(*Init of F, action of PPROD F case*) +(*Init of F, action of PLam F case*) by (rtac reachable.Acts 1); by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); by (assume_tac 1); -by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); +by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); (*induction over the 2nd "reachable" assumption*) by (eres_inst_tac [("xa","f")] reachable.induct 1); -(*Init of PPROD F, action of F case*) +(*Init of PLam F, action of F case*) by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); by (force_tac (claset() addIs [reachable.Init], simpset()) 1); by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); -(*last case: an action of PPROD I F*) +(*last case: an action of PLam I F*) by (rtac reachable.Acts 1); by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); by (assume_tac 1); -by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); -qed_spec_mp "reachable_lift_Join_PPROD"; +by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1); +qed_spec_mp "reachable_lift_Join_PLam"; (*The index set must be finite: otherwise infinitely many copies of F can - perform actions, and PPROD can never catch up in finite time.*) + perform actions, and PLam can never catch up in finite time.*) Goal "finite I \ -\ ==> {f. ALL i:I. f i : reachable (F i)} <= reachable (PPROD I F)"; +\ ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"; by (etac finite_induct 1); by (Simp_tac 1); -by (force_tac (claset() addDs [reachable_lift_Join_PPROD], - simpset() addsimps [PPROD_insert]) 1); -qed "reachable_PPROD_subset2"; +by (force_tac (claset() addDs [reachable_lift_Join_PLam], + simpset() addsimps [PLam_insert]) 1); +qed "reachable_PLam_subset2"; Goal "finite I ==> \ -\ reachable (PPROD I F) = {f. ALL i:I. f i : reachable (F i)}"; +\ reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"; by (REPEAT_FIRST (ares_tac [equalityI, - reachable_PPROD_subset1, - reachable_PPROD_subset2])); -qed "reachable_PPROD_eq"; + reachable_PLam_subset1, + reachable_PLam_subset2])); +qed "reachable_PLam_eq"; (** Co **) Goal "[| F i : A Co B; i: I; finite I |] \ -\ ==> PPROD I F : (lift_set i A) Co (lift_set i B)"; +\ ==> PLam I F : (lift_set i A) Co (lift_set i B)"; by (auto_tac (claset(), simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, - reachable_PPROD_eq])); + reachable_PLam_eq])); by (auto_tac (claset(), - simpset() addsimps [constrains_def, PPROD_def, Acts_JN])); + simpset() addsimps [constrains_def, PLam_def, Acts_JN])); by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); -qed "Constrains_imp_PPROD_Constrains"; +qed "Constrains_imp_PLam_Constrains"; -Goal "[| ALL i:I. f0 i : R i; i: I |] \ -\ ==> drop_set i ({f. (ALL i:I. f i : R i)} Int lift_set i A) = R i Int A"; +Goal "[| ALL j:I. f0 j : A j; i: I |] \ +\ ==> drop_set i (INT j:I. lift_set j (A j)) = A i"; by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], - simpset() addsimps [drop_set_def, lift_set_def]) 1); -qed "drop_set_Int_depend"; + simpset() addsimps [drop_set_def]) 1); +qed "drop_set_INT_lift_set"; -(*Again, we need the f0 premise so that PPROD I F has an initial state; +(*Again, we need the f0 premise so that PLam I F has an initial state; otherwise its Co-property is vacuous.*) -Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B); \ -\ i: I; finite I; f0: Init (PPROD I F) |] \ +Goal "[| PLam I F : (lift_set i A) Co (lift_set i B); \ +\ i: I; finite I; f0: Init (PLam I F) |] \ \ ==> F i : A Co B"; by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1); by (blast_tac (claset() addIs [reachable.Init]) 2); -by (dtac PPROD_constrains_projection 1); +by (dtac PLam_constrains_projection 1); by (assume_tac 1); by (asm_full_simp_tac - (simpset() addsimps [drop_set_Int_depend, reachable_PPROD_eq]) 1); -qed "PPROD_Constrains_imp_Constrains"; + (simpset() addsimps [drop_set_lift_set_Int2, + drop_set_INT_lift_set, reachable_PLam_eq]) 1); +qed "PLam_Constrains_imp_Constrains"; -Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ -\ ==> (PPROD I F : (lift_set i A) Co (lift_set i B)) = \ +Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ +\ ==> (PLam I F : (lift_set i A) Co (lift_set i B)) = \ \ (F i : A Co B)"; -by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, - PPROD_Constrains_imp_Constrains]) 1); -qed "PPROD_Constrains"; +by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, + PLam_Constrains_imp_Constrains]) 1); +qed "PLam_Constrains"; -Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ -\ ==> (PPROD I F : Stable (lift_set i A)) = (F i : Stable A)"; -by (asm_simp_tac (simpset() delsimps [Init_PPROD] - addsimps [Stable_def, PPROD_Constrains]) 1); -qed "PPROD_Stable"; +Goal "[| i: I; finite I; f0: Init (PLam I F) |] \ +\ ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"; +by (asm_simp_tac (simpset() delsimps [Init_PLam] + addsimps [Stable_def, PLam_Constrains]) 1); +qed "PLam_Stable"; -(** PFUN (no dependence on i) doesn't require the f0 premise **) +(** const_PLam (no dependence on i) doesn't require the f0 premise **) -Goal "i: I \ -\ ==> drop_set i ({f. (ALL i:I. f i : R)} Int lift_set i A) = R Int A"; -by (force_tac (claset(), simpset() addsimps [drop_set_def]) 1); -qed "drop_set_Int"; - -Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B); \ +Goal "[| (plam x:I. F) : (lift_set i A) Co (lift_set i B); \ \ i: I; finite I |] \ \ ==> F : A Co B"; by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); -by (dtac PPROD_constrains_projection 1); +by (dtac PLam_constrains_projection 1); by (assume_tac 1); by (asm_full_simp_tac - (simpset() addsimps [drop_set_Int, Collect_conj_eq RS sym, - reachable_PPROD_eq]) 1); -qed "PFUN_Constrains_imp_Constrains"; + (simpset() addsimps [drop_set_INT, + drop_set_lift_set_Int2, Collect_conj_eq RS sym, + reachable_PLam_eq]) 1); +qed "const_PLam_Constrains_imp_Constrains"; Goal "[| i: I; finite I |] \ -\ ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) = \ +\ ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) = \ \ (F : A Co B)"; -by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, - PFUN_Constrains_imp_Constrains]) 1); -qed "PFUN_Constrains"; +by (blast_tac (claset() addIs [Constrains_imp_PLam_Constrains, + const_PLam_Constrains_imp_Constrains]) 1); +qed "const_PLam_Constrains"; Goal "[| i: I; finite I |] \ -\ ==> ((PPI x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; -by (asm_simp_tac (simpset() addsimps [Stable_def, PFUN_Constrains]) 1); -qed "PFUN_Stable"; +\ ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; +by (asm_simp_tac (simpset() addsimps [Stable_def, const_PLam_Constrains]) 1); +qed "const_PLam_Stable"; (*** guarantees properties ***) -Goal "drop_act i (lift_act i act) = act"; -by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], - simpset() addsimps [drop_act_def, lift_act_def]) 1); -qed "lift_act_inverse"; -Addsimps [lift_act_inverse]; - - -(*Because A and B could differ outside i, cannot generalize result to - drop_set i (A Int B) = drop_set i A Int drop_set i B -*) -Goalw [lift_set_def, drop_set_def] - "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; -by Auto_tac; -qed "drop_set_lift_set_Int"; - Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)"; by (rtac program_equalityI 1); by (simp_tac (simpset() addsimps [Acts_Join, image_Un, @@ -508,16 +523,16 @@ by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); qed "lift_prog_guarantees"; -Goalw [PPROD_def] +Goalw [PLam_def] "[| ALL i:I. F i : X guar Y |] \ -\ ==> (PPROD I F) : (INT i: I. lift_prog i `` X) \ +\ ==> (PLam I F) : (INT i: I. lift_prog i `` X) \ \ guar (INT i: I. lift_prog i `` Y)"; by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1); -qed "guarantees_PPROD_INT"; +qed "guarantees_PLam_INT"; -Goalw [PPROD_def] +Goalw [PLam_def] "[| ALL i:I. F i : X guar Y |] \ -\ ==> (PPROD I F) : (UN i: I. lift_prog i `` X) \ +\ ==> (PLam I F) : (UN i: I. lift_prog i `` X) \ \ guar (UN i: I. lift_prog i `` Y)"; by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1); -qed "guarantees_PPROD_UN"; +qed "guarantees_PLam_UN"; diff -r 5a557122bb62 -r 56e08e264961 src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Wed Jun 23 10:38:49 1999 +0200 +++ b/src/HOL/UNITY/PPROD.thy Wed Jun 23 10:39:35 1999 +0200 @@ -17,7 +17,7 @@ "drop_set i A == (%f. f i) `` A" 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}" + "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}" drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set" "drop_act i act == (%(f,f'). (f i, f' i)) `` act" @@ -33,13 +33,13 @@ drop_act i `` (Acts F))" (*products of programs*) - PPROD :: ['a set, 'a => 'b program] => ('a => 'b) program - "PPROD I F == JN i:I. lift_prog i (F i)" + PLam :: ['a set, 'a => 'b program] => ('a => 'b) program + "PLam I F == JN i:I. lift_prog i (F i)" syntax - "@PPROD" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3PPI _:_./ _)" 10) + "@PLam" :: [pttrn, 'a set, 'b set] => ('a => 'b) set ("(3plam _:_./ _)" 10) translations - "PPI x:A. B" == "PPROD A (%x. B)" + "plam x:A. B" == "PLam A (%x. B)" end