--- 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";
--- 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();
--- 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 **)
--- 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";
--- 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";