# HG changeset patch # User ehmety # Date 1005850879 -3600 # Node ID 55c0849212401aa2d675ffcf25dd4201c1e82254 # Parent f368821d9c682e743be87fa9a466072cd6cba36a Modified to make the files build with the new changes in ZF diff -r f368821d9c68 -r 55c084921240 src/ZF/UNITY/Constrains.ML --- a/src/ZF/UNITY/Constrains.ML Thu Nov 15 18:37:34 2001 +0100 +++ b/src/ZF/UNITY/Constrains.ML Thu Nov 15 20:01:19 2001 +0100 @@ -137,10 +137,10 @@ qed "Constrains_weaken"; (** Union **) -Goalw [Constrains_def2] +Goalw [Constrains_def2] "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"; by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1); +by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1); by (blast_tac (claset() addIs [constrains_Un]) 1); qed "Constrains_Un"; @@ -149,7 +149,7 @@ by (cut_facts_tac [minor] 1); by (auto_tac (claset() addDs [major] addIs [constrains_UN], - simpset() addsimps [Int_UN_distrib])); + simpset() delsimps UN_simps addsimps [Int_UN_distrib])); qed "Constrains_UN"; (** Intersection **) @@ -170,6 +170,9 @@ by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1); by (force_tac (claset(), simpset() addsimps [Inter_def]) 2); by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); +by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1); +by (Force_tac 2); +by (asm_simp_tac (simpset() delsimps INT_simps) 1); by (rtac constrains_INT 1); by (etac not_emptyE 1); by (dresolve_tac [major] 1); @@ -188,7 +191,7 @@ Goalw [Constrains_def2] "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"; -by (full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1); +by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1); by (blast_tac (claset() addIs [constrains_cancel]) 1); qed "Constrains_cancel"; diff -r f368821d9c68 -r 55c084921240 src/ZF/UNITY/SubstAx.ML --- a/src/ZF/UNITY/SubstAx.ML Thu Nov 15 18:37:34 2001 +0100 +++ b/src/ZF/UNITY/SubstAx.ML Thu Nov 15 20:01:19 2001 +0100 @@ -86,10 +86,9 @@ qed "LeadsTo_Un_duplicate2"; val [major, program] = Goalw [LeadsTo_def] -"[|(!!i. i:I ==> F : A(i) LeadsTo B); F:program|] \ -\ ==> F : (UN i:I. A(i)) LeadsTo B"; +"[|(!!i. i:I ==> F : A(i) LeadsTo B); F:program|]==>F:(UN i:I. A(i)) LeadsTo B"; by (cut_facts_tac [program] 1); -by (asm_simp_tac (simpset() addsimps [Int_Union_Union2]) 1); +by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 1); by (rtac leadsTo_UN 1); by (dtac major 1); by Auto_tac; @@ -342,7 +341,7 @@ \ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"; by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains, - Int_Un_distrib2 RS sym]) 1); + Int_Un_distrib]) 1); by Safe_tac; by (REPEAT(Blast_tac 2)); by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1); @@ -363,7 +362,7 @@ by (Asm_simp_tac 1); by (rtac Completion 1); by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4); -by (Asm_simp_tac 4); +by (asm_simp_tac (simpset() delsimps INT_simps) 4); by (rtac Constrains_INT 4); by (REPEAT(Blast_tac 1)); val lemma = result(); diff -r f368821d9c68 -r 55c084921240 src/ZF/UNITY/UNITYMisc.ML --- a/src/ZF/UNITY/UNITYMisc.ML Thu Nov 15 18:37:34 2001 +0100 +++ b/src/ZF/UNITY/UNITYMisc.ML Thu Nov 15 20:01:19 2001 +0100 @@ -37,7 +37,6 @@ qed "greaterThan_iff"; - (** Needed for WF reasoning in WFair.ML **) Goal "k:A ==>less_than(A)``{k} = greaterThan(k, A)"; @@ -57,38 +56,6 @@ (** Ad-hoc set-theory rules **) -Goal "(C Int A) Un (C Int B) = C Int (A Un B)"; -by (Blast_tac 1); -qed "Int_Un_distrib2"; - -Goal "C Int (A - B) = (C Int A) - (C Int B)"; -by (Blast_tac 1); -qed "Diff_Int_distrib"; - -Goal "(A - B) Int C = (A Int C) - (B Int C)"; -by (Blast_tac 1); -qed "Diff_Int_distrib2"; - -Goal "A Un (A Un B) = A Un B"; -by (Blast_tac 1); -qed "double_Un"; - -Goal "A Un (B Un C) = B Un (A Un C)"; -by (Blast_tac 1); -qed "Un_assoc2"; - - -val Un_ac = [Un_assoc, double_Un, Un_commute, Un_assoc2, Un_absorb]; - -Goal "A Un B = Union({A, B})"; -by (Blast_tac 1); -qed "Un_eq_Union"; - -Goal "(UN x:A. {x}) = A"; -by (Blast_tac 1); -qed "UN_singleton"; - - Goal "Union(B) Int A = (UN b:B. b Int A)"; by Auto_tac; qed "Int_Union_Union"; @@ -97,82 +64,11 @@ by Auto_tac; qed "Int_Union_Union2"; -(** Intersection **) -Goal "A Int (A Int B) = A Int B"; -by (Blast_tac 1); -qed "double_Int"; - -Goal "A Int (B Int C) = B Int (A Int C)"; -by (Blast_tac 1); -qed "Int_assoc2"; - -val Int_ac = [Int_assoc, double_Int, Int_commute, Int_assoc2]; - -Goal "A Int B = 0 ==> A - B = A"; -by (Blast_tac 1); -qed "Diff_triv"; - -Goal "A Int B - C = A Int (B - C)"; -by (Blast_tac 1); -qed "Int_Diff"; - -Goal "f -``B = (UN y:B. f-``{y})"; -by (Blast_tac 1); -qed "vimage_eq_UN"; - Goal "A Un B - (A - B) = B"; by (Blast_tac 1); qed "Un_Diff_Diff"; AddIffs [Un_Diff_Diff]; -(*** INT simps ***) - -Goal -"i:I ==> (INT i:I. A(i)) Un B = (INT i:I. A(i) Un B)"; -by Auto_tac; -qed "INT_Un_distrib"; - -Goal - "!!C. c: C ==> (INT x:C. cons(a, B(x))) = cons(a, (INT x:C. B(x)))"; -by Auto_tac; -qed "INT_cons"; - -Goal -"i:I ==> (INT i:I. A(i)) Int B = (INT i:I. A(i) Int B)"; -by Auto_tac; -qed "INT_Int_distrib2"; - -Goal -"i:I ==> B Int (INT i:I. A(i)) = (INT i:I. B Int A(i))"; -by Auto_tac; -qed "Int_INT_distrib"; - -val INT_simps = [Un_INT_distrib, Un_INT_distrib2, - INT_constant, INT_Int_distrib, Diff_INT, - INT_Un_distrib,INT_cons, INT_Int_distrib2, Int_INT_distrib, Inter_0]; - - -(*** UN ***) -Goal -"!!C. c: C ==> cons(a, (UN x:C. B(x))) = (UN x:C. cons(a, B(x)))"; -by Auto_tac; -qed "UN_cons"; - -Goal - "!!C. c: C ==> B Un (UN x:C. A(x)) = (UN x:C. B Un A(x))"; -by Auto_tac; -qed "Un_UN_distrib"; - -Goal -"!!C. c: C ==> (UN x:C. B(x)) Un A = (UN x:C. B(x) Un A)"; -by Auto_tac; -qed "UN_Un_distrib2"; - -Goal "(UN x:C. B(x)) Int A = (UN x:C. B(x) Int A)"; -by Auto_tac; -qed "UN_Int_distrib"; - -val UN_simps = [UN_cons, Un_UN_distrib, UN_Un_distrib2, UN_Un_distrib, UN_Int_distrib, UN_0]; (** Needed in State theory for the current definition of variables where they are indexed by lists **) diff -r f368821d9c68 -r 55c084921240 src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Thu Nov 15 18:37:34 2001 +0100 +++ b/src/ZF/UNITY/Union.ML Thu Nov 15 20:01:19 2001 +0100 @@ -86,7 +86,7 @@ Goal "Acts(F Join G) = Acts(F) Un Acts(G)"; by (simp_tac (simpset() - addsimps [Int_Un_distrib,cons_absorb,Join_def]) 1); + addsimps [Int_Un_distrib2,cons_absorb,Join_def]) 1); qed "Acts_Join"; Goal "AllowedActs(F Join G) = \ @@ -105,12 +105,12 @@ Goal "A Join (B Join C) = B Join (A Join C)"; by (asm_simp_tac (simpset() addsimps - Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1); + Un_ac@Int_ac@[Join_def,Int_Un_distrib2, cons_absorb]) 1); qed "Join_left_commute"; Goal "(F Join G) Join H = F Join (G Join H)"; by (asm_simp_tac (simpset() addsimps - Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib]) 1); + Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib2]) 1); qed "Join_assoc"; (* Needed below *) @@ -168,22 +168,24 @@ Goalw [JOIN_def] "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))"; -by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib2])); +by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib])); qed "Init_JN"; Goalw [JOIN_def] "Acts(JOIN(I,F)) = cons(id(state), UN i:I. Acts(F(i)))"; -by (auto_tac (claset(), simpset() addsimps [ UN_Int_distrib])); +by (auto_tac (claset(), simpset() delsimps (INT_simps@UN_simps))); +by (rtac equalityI 1); +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "Acts_JN"; Goalw [JOIN_def] "AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))"; -by (auto_tac (claset(), - simpset() addsimps [INT_cons RS sym, INT_Int_distrib2])); +by Auto_tac; +by (rtac equalityI 1); +by (auto_tac (claset() addDs [AllowedActs_type RS subsetD], simpset())); qed "AllowedActs_JN"; AddIffs [Init_JN, Acts_JN, AllowedActs_JN]; - Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))"; by (rtac program_equalityI 1); by Auto_tac; @@ -216,11 +218,11 @@ by (rtac program_equalityI 1); by (ALLGOALS(Asm_full_simp_tac)); by Safe_tac; -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [Int_absorb, INT_Int_distrib2, - Int_INT_distrib, UN_cons, INT_cons]))); -by (ALLGOALS(Clarify_tac)); -by (REPEAT(Blast_tac 1)); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Int_absorb]))); +by (ALLGOALS(rtac equalityI)); +by (auto_tac (claset() addDs [Init_type RS subsetD, + Acts_type RS subsetD, + AllowedActs_type RS subsetD], simpset())); qed "JN_Un"; Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))"; @@ -375,15 +377,16 @@ \ (EX i:I. programify(F(i)) : transient(A))"; by (auto_tac (claset(), simpset() addsimps [transient_def, JOIN_def])); -by (auto_tac (claset(), simpset() addsimps - [st_set_def,UN_Int_distrib, INT_Int_distrib])); +by (rewrite_goals_tac [st_set_def]); +by (dres_inst_tac [("x", "xb")] bspec 2); +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "JN_transient"; Goal "F Join G : transient(A) <-> \ \ (programify(F) : transient(A) | programify(G):transient(A))"; by (auto_tac (claset(), simpset() addsimps [transient_def, - Join_def, Int_Un_distrib])); + Join_def, Int_Un_distrib2])); qed "Join_transient"; AddIffs [Join_transient]; @@ -485,7 +488,7 @@ Goal "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"; by (asm_full_simp_tac (simpset() addsimps [ok_def, Join_def, OK_def, - Int_assoc, cons_absorb, Int_Un_distrib, Ball_def]) 1); + Int_assoc, cons_absorb, Int_Un_distrib2, Ball_def]) 1); by (rtac iffI 1); by Safe_tac; by (REPEAT(Force_tac 1)); @@ -582,8 +585,13 @@ Goal "safety_prop(X) ==> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X"; -by (asm_full_simp_tac (simpset() addsimps [Allowed_def, - UN_Int_distrib, safety_prop_Acts_iff]) 1); +by (subgoal_tac "cons(id(state), Union(RepFun(X, Acts)) Int Pow(state * state)) = \ +\ Union(RepFun(X, Acts))" 1); +by (rtac equalityI 2); +by (REPEAT(force_tac (claset() addDs [Acts_type RS subsetD], + simpset() addsimps [safety_prop_def]) 2)); +by (asm_full_simp_tac (simpset() delsimps UN_simps + addsimps [Allowed_def, safety_prop_Acts_iff]) 1); by (rewrite_goals_tac [safety_prop_def]); by Auto_tac; qed "Allowed_eq"; @@ -596,7 +604,7 @@ (*For safety_prop to hold, the property must be satisfiable!*) Goal "safety_prop(A co B) <-> (A <= B & st_set(A))"; by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1); -by Auto_tac; +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); by (REPEAT(Blast_tac 1)); qed "safety_prop_constrains"; AddIffs [safety_prop_constrains]; @@ -643,10 +651,14 @@ by (REPEAT(Blast_tac 1)); qed "safety_prop_Inter"; -Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X) |] \ +Goalw [ok_def] +"[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X) |] \ \ ==> F ok G <-> (programify(G):X & acts Int Pow(state*state) <= AllowedActs(G))"; -by (auto_tac (claset(), - simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib])); +by (dres_inst_tac [("G", "G")] safety_prop_Acts_iff 1); +by Safe_tac; +by (ALLGOALS(cut_inst_tac [("F", "G")] AllowedActs_type)); +by (ALLGOALS(cut_inst_tac [("F", "G")] Acts_type)); +by Auto_tac; qed "def_UNION_ok_iff"; diff -r f368821d9c68 -r 55c084921240 src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Thu Nov 15 18:37:34 2001 +0100 +++ b/src/ZF/UNITY/WFair.ML Thu Nov 15 20:01:19 2001 +0100 @@ -100,12 +100,11 @@ addIs [transient_strengthen, constrains_weaken]) 1); qed "ensures_weaken_R"; -(*The L-version (precondition strengthening) fails, but we have this*) +(*The L-version (precondition strengthening) fails, but we have this*) Goalw [ensures_def] "[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)"; -by (asm_full_simp_tac (simpset() addsimps [ensures_def, - Int_Un_distrib2, - Diff_Int_distrib RS sym]) 1); -by (Clarify_tac 1); +by (simp_tac (simpset() addsimps [ensures_def, + Int_Un_distrib RS sym, + Diff_Int_distrib RS sym]) 1); by (blast_tac (claset() addIs [transient_strengthen, stable_constrains_Int, constrains_weaken]) 1); @@ -185,11 +184,12 @@ by (auto_tac (claset() addDs [leads_left], simpset())); qed "leadsTo_Union"; -val [major,program,B] = Goalw [leadsTo_def, st_set_def] -"[|(!!A. A:S ==>F:(A Int C) leadsTo B); F:program; st_set(B)|]==>F:(Union(S)Int C)leadsTo B"; +val [major,program,B] = Goalw [leadsTo_def, st_set_def] +"[|(!!A. A:S ==>F:(A Int C) leadsTo B); F:program; st_set(B)|] \ +\ ==>F:(Union(S)Int C)leadsTo B"; by (cut_facts_tac [program, B] 1); -by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); -by (rtac leads.Union 1); +by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1); +by (resolve_tac [leads.Union] 1); by Auto_tac; by (ALLGOALS(dtac major)); by (auto_tac (claset() addDs [leads_left], simpset())); @@ -432,8 +432,7 @@ by (blast_tac (claset() addIs [leadsTo_Trans]) 2); by (rtac leadsTo_Basis 1); by (asm_full_simp_tac (simpset() - addsimps [ensures_def, Diff_Int_distrib RS sym, - Diff_Int_distrib2 RS sym, Int_Un_distrib RS sym]) 1); + addsimps [ensures_def, Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); by (REPEAT(blast_tac (claset() addIs [transient_strengthen,constrains_Int] addDs [constrainsD2]) 1)); @@ -498,9 +497,10 @@ by (ALLGOALS(Asm_simp_tac)); by (subgoal_tac "F : (A Int (f-``(converse(r)``{x}))) leadsTo B" 1); by (stac vimage_eq_UN 2); -by (asm_simp_tac (simpset() addsimps [Int_UN_distrib]) 2); +by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 2); by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); -by (auto_tac (claset() addIs [leadsTo_UN], simpset())); +by (auto_tac (claset() addIs [leadsTo_UN], + simpset() delsimps UN_simps addsimps [Int_UN_distrib])); qed "lemma1"; (** Meta or object quantifier ? **) @@ -703,7 +703,7 @@ by (rtac completion 1); by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4); by (Blast_tac 5); -by (Asm_simp_tac 4); +by (asm_simp_tac (simpset() delsimps INT_simps) 4); by (rtac constrains_INT 4); by (REPEAT(Blast_tac 1)); qed "lemma";