# HG changeset patch
# User paulson
# Date 1005914923 -3600
# Node ID 9dc4e8fec63dd9740abe21cfdea138ec4941574e
# Parent  ae54aa9f6d08ba0f19ca55215d41b41bfc42f3a1
last-minute tidying

diff -r ae54aa9f6d08 -r 9dc4e8fec63d src/ZF/UNITY/Comp.ML
--- 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);
diff -r ae54aa9f6d08 -r 9dc4e8fec63d src/ZF/UNITY/Constrains.ML
--- 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";
diff -r ae54aa9f6d08 -r 9dc4e8fec63d src/ZF/UNITY/SubstAx.ML
--- 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();
diff -r ae54aa9f6d08 -r 9dc4e8fec63d src/ZF/UNITY/Union.ML
--- 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];
diff -r ae54aa9f6d08 -r 9dc4e8fec63d src/ZF/UNITY/WFair.ML
--- 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";