--- a/src/ZF/UNITY/Comp.ML Thu Nov 15 23:26:58 2001 +0100
+++ b/src/ZF/UNITY/Comp.ML Fri Nov 16 13:48:43 2001 +0100
@@ -66,8 +66,7 @@
by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
qed "Join_absorb2";
-Goal
-"H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)";
+Goal "H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)";
by (case_tac "I=0" 1);
by (Force_tac 1);
by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
--- a/src/ZF/UNITY/Constrains.ML Thu Nov 15 23:26:58 2001 +0100
+++ b/src/ZF/UNITY/Constrains.ML Fri Nov 16 13:48:43 2001 +0100
@@ -165,19 +165,11 @@
"[| (!!i. i:I ==>F: A(i) Co A'(i)); F:program |] \
\ ==> F:(INT i:I. A(i)) Co (INT i:I. A'(i))";
by (cut_facts_tac [minor] 1);
-by (case_tac "I=0" 1);
-by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
-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 (asm_simp_tac (simpset() delsimps INT_simps
+ addsimps [Constrains_def]@INT_extend_simps) 1);
by (rtac constrains_INT 1);
-by (etac not_emptyE 1);
by (dresolve_tac [major] 1);
-by (rewrite_goal_tac [Constrains_def] 1);
-by (ALLGOALS(Asm_full_simp_tac));
+by (auto_tac (claset(), simpset() addsimps [Constrains_def]));
qed "Constrains_INT";
Goalw [Constrains_def] "F : A Co A' ==> reachable(F) Int A <= A'";
@@ -461,8 +453,7 @@
by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
qed "increasing_imp_Increasing";
-Goal
-"F:Increasing(A, r, lam x:state. c) <-> F:program & (EX a. a:A)";
+Goal "F:Increasing(A, r, lam x:state. c) <-> F:program & (EX a. a:A)";
by (auto_tac (claset() addDs [IncreasingD2]
addIs [increasing_imp_Increasing], simpset()));
qed "Increasing_constant";
--- a/src/ZF/UNITY/SubstAx.ML Thu Nov 15 23:26:58 2001 +0100
+++ b/src/ZF/UNITY/SubstAx.ML Fri Nov 16 13:48:43 2001 +0100
@@ -352,17 +352,10 @@
\ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \
\ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)";
by (etac Fin_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Inter_0]));
-by (case_tac "y=0" 1);
-by Auto_tac;
-by (etac not_emptyE 1);
-by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) &\
- \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1);
-by (Blast_tac 2);
-by (Asm_simp_tac 1);
+by (auto_tac (claset(), simpset() delsimps INT_simps
+ addsimps [Inter_0]));
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 (simpset() delsimps INT_simps) 4);
+by (asm_simp_tac (simpset() delsimps INT_simps addsimps INT_extend_simps) 4);
by (rtac Constrains_INT 4);
by (REPEAT(Blast_tac 1));
val lemma = result();
--- a/src/ZF/UNITY/Union.ML Thu Nov 15 23:26:58 2001 +0100
+++ b/src/ZF/UNITY/Union.ML Fri Nov 16 13:48:43 2001 +0100
@@ -85,8 +85,7 @@
qed "Init_Join";
Goal "Acts(F Join G) = Acts(F) Un Acts(G)";
-by (simp_tac (simpset()
- addsimps [Int_Un_distrib2,cons_absorb,Join_def]) 1);
+by (simp_tac (simpset() addsimps [Int_Un_distrib2, cons_absorb, Join_def]) 1);
qed "Acts_Join";
Goal "AllowedActs(F Join G) = \
@@ -104,8 +103,8 @@
qed "Join_commute";
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_distrib2, cons_absorb]) 1);
+by (asm_simp_tac (simpset() addsimps
+ 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)";
@@ -166,13 +165,13 @@
AddSEs [not_emptyE];
Addsimps [Inter_0];
-Goalw [JOIN_def]
- "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
+Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
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)))";
+ "Acts(JOIN(I,F)) = cons(id(state), UN i:I. Acts(F(i)))";
by (auto_tac (claset(), simpset() delsimps (INT_simps@UN_simps)));
by (rtac equalityI 1);
by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
@@ -208,21 +207,12 @@
simpset() addsimps [cons_absorb]));
qed "JN_absorb";
-Goalw [Inter_def] "[| i:I; j:J |] ==> \
-\ (INT i:I Un J. A(i)) = ((INT i:I. A(i)) Int (INT j:J. A(j)))";
-by Auto_tac;
-by (Blast_tac 1);
-qed "INT_Un";
-
Goal "(JN i: I Un J. F(i)) = ((JN i: I. F(i)) Join (JN i:J. F(i)))";
by (rtac program_equalityI 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by Safe_tac;
-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()));
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [UN_Un,INT_Un])));
+by (ALLGOALS(asm_full_simp_tac (simpset() delsimps INT_simps
+ addsimps INT_extend_simps)));
+by (Blast_tac 1);
qed "JN_Un";
Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))";
@@ -230,8 +220,7 @@
by Auto_tac;
qed "JN_constant";
-Goal
-"(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))";
+Goal "(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))";
by (rtac program_equalityI 1);
by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb])));
by Safe_tac;
@@ -240,8 +229,7 @@
by (Force_tac 1);
qed "JN_Join_distrib";
-Goal
-"(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
+Goal "(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))";
by (asm_simp_tac (simpset()
addsimps [JN_Join_distrib, JN_constant]) 1);
qed "JN_Join_miniscope";
@@ -385,8 +373,7 @@
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_distrib2]));
+ simpset() addsimps [transient_def, Join_def, Int_Un_distrib2]));
qed "Join_transient";
AddIffs [Join_transient];
--- a/src/ZF/UNITY/WFair.ML Thu Nov 15 23:26:58 2001 +0100
+++ b/src/ZF/UNITY/WFair.ML Fri Nov 16 13:48:43 2001 +0100
@@ -52,7 +52,6 @@
by (ALLGOALS(Clarify_tac));
by (cut_inst_tac [("F", "x")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1);
-by (subgoal_tac "EX x. x:state" 1);
by Auto_tac;
qed "transient_state";
@@ -61,7 +60,6 @@
by (ALLGOALS(Clarify_tac));
by (cut_inst_tac [("F", "x")] Acts_type 1);
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1);
-by (subgoal_tac "EX x. x:state" 1);
by (subgoal_tac "B=state" 1);
by Auto_tac;
qed "transient_state2";
@@ -101,10 +99,10 @@
qed "ensures_weaken_R";
(*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 (simp_tac (simpset() addsimps [ensures_def,
- Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym]) 1);
+Goalw [ensures_def]
+ "[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)";
+by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
+ Diff_Int_distrib RS sym]) 1);
by (blast_tac (claset()
addIs [transient_strengthen,
stable_constrains_Int, constrains_weaken]) 1);
@@ -166,14 +164,14 @@
(*Useful with cancellation, disjunction*)
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
-by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+by (Asm_full_simp_tac 1);
qed "leadsTo_Un_duplicate";
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "leadsTo_Un_duplicate2";
-(* The Union introduction rule as we should have liked to state it *)
+(*The Union introduction rule as we should have liked to state it*)
val [major, program,B]= Goalw [leadsTo_def, st_set_def]
"[|(!!A. A:S ==> F:A leadsTo B); F:program; st_set(B)|]==>F:Union(S) leadsTo B";
by (cut_facts_tac [program, B] 1);
@@ -432,7 +430,8 @@
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
by (rtac leadsTo_Basis 1);
by (asm_full_simp_tac (simpset()
- addsimps [ensures_def, Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
+ addsimps [ensures_def, Diff_Int_distrib RS sym,
+ Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
by (REPEAT(blast_tac (claset()
addIs [transient_strengthen,constrains_Int]
addDs [constrainsD2]) 1));
@@ -497,7 +496,8 @@
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() delsimps UN_simps 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() delsimps UN_simps addsimps [Int_UN_distrib]));
@@ -691,20 +691,12 @@
\(ALL i:I. F : (A(i)) leadsTo (A'(i) Un C)) --> \
\ (ALL i:I. F : (A'(i)) co (A'(i) Un C)) --> \
\ F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)";
-by (etac Fin_induct 1);
+by (etac Fin_induct 1);
by (auto_tac (claset(), simpset() addsimps [Inter_0]));
-by (case_tac "y=0" 1);
-by Auto_tac;
-by (etac not_emptyE 1);
-by (subgoal_tac "Inter(cons(A(x), RepFun(y, A)))= A(x) Int Inter(RepFun(y,A)) & \
- \ Inter(cons(A'(x), RepFun(y, A')))= A'(x) Int Inter(RepFun(y,A'))" 1);
-by (Blast_tac 2);
-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 (Blast_tac 5);
-by (asm_simp_tac (simpset() delsimps INT_simps) 4);
-by (rtac constrains_INT 4);
+by (auto_tac (claset(),
+ simpset() delsimps INT_simps addsimps INT_extend_simps));
+by (rtac constrains_INT 1);
by (REPEAT(Blast_tac 1));
qed "lemma";