# HG changeset patch
# User paulson
# Date 853495759 -3600
# Node ID d708d8cdc8e8a1de0493a4f5cbd18ec5f60710df
# Parent  0231e4f467f26d8f842f700d0e40bdae90931cf9
New miniscoping rules for the bounded quantifiers and UN/INT operators

diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/IOA/ABP/Correctness.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -172,11 +172,6 @@
 goal Correctness.thy 
       "is_weak_pmap reduce ch_ioa ch_fin_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
-by (rtac conjI 1);
-(* --------------  start states ----------------- *)
-by (Simp_tac 1);
-by (rtac ballI 1);
-by (Asm_full_simp_tac 1);
 (* ---------------- main-part ------------------- *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/IOA/NTP/Correctness.ML
--- a/src/HOL/IOA/NTP/Correctness.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -39,12 +39,12 @@
 \   | C_m_r => False          \
 \   | C_r_s => False          \
 \   | C_r_r(m) => False)";
- by(simp_tac (!simpset addsimps ([externals_def, restrict_def,
+ by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
                             restrict_asig_def, Spec.sig_def]
                             @asig_projections)) 1);
 
-  by(Action.action.induct_tac "a" 1);
-  by(ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
+  by (Action.action.induct_tac "a" 1);
+  by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
  (* 2 *)
   by (simp_tac (!simpset addsimps impl_ioas) 1);
   by (simp_tac (!simpset addsimps impl_asigs) 1);
@@ -67,52 +67,49 @@
 (* Proof of correctness *)
 goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def]
   "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by(simp_tac (!simpset addsimps 
-    [Correctness.hom_def,
-     cancel_restrict,externals_lemma]) 1);
+by (simp_tac (!simpset addsimps 
+    [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
 by (rtac conjI 1);
-by(simp_tac ss' 1);
-by (rtac ballI 1);
-by (dtac CollectD 1);
-by(asm_simp_tac (!simpset addsimps sels) 1);
-by(REPEAT(rtac allI 1));
+by (simp_tac ss' 1);
+by (asm_simp_tac (!simpset addsimps sels) 1);
+by (REPEAT(rtac allI 1));
 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
 
-by(Action.action.induct_tac "a"  1);
-by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
-by(forward_tac [inv4] 1);
+by (Action.action.induct_tac "a"  1);
+by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (forward_tac [inv4] 1);
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
-by(simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
+by (simp_tac ss' 1);
 
-by(asm_simp_tac ss' 1);
-by(forward_tac [inv4] 1);
-by(forward_tac [inv2] 1);
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv4] 1);
+by (forward_tac [inv2] 1);
 by (etac disjE 1);
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
-by(asm_simp_tac ss' 1);
-by(forward_tac [inv2] 1);
+by (asm_simp_tac ss' 1);
+by (forward_tac [inv2] 1);
 by (etac disjE 1);
 
-by(forward_tac [inv3] 1);
-by(case_tac "sq(sen(s))=[]" 1);
+by (forward_tac [inv3] 1);
+by (case_tac "sq(sen(s))=[]" 1);
 
-by(asm_full_simp_tac ss' 1);
-by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (asm_full_simp_tac ss' 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
-by(case_tac "m = hd(sq(sen(s)))" 1);
+by (case_tac "m = hd(sq(sen(s)))" 1);
 
 by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
 
-by(Asm_full_simp_tac 1);
-by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
 qed"ntp_correct";
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/IOA/meta_theory/IOA.ML
--- a/src/HOL/IOA/meta_theory/IOA.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -54,7 +54,7 @@
 
 goalw IOA.thy (reachable_def::exec_rws)
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
-  by (Asm_full_simp_tac 1);
+  by (asm_full_simp_tac (!simpset delsimps bex_simps) 1);
   by (safe_tac (!claset));
   by (res_inst_tac [("x","(%i.if i<n then fst ex i                    \
 \                            else (if i=n then Some a else None),    \
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/IOA/meta_theory/Solve.ML
--- a/src/HOL/IOA/meta_theory/Solve.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -113,7 +113,6 @@
  by (rtac conjI 1);
 (* start_states *)
  by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1);
- by (Fast_tac 1);
 (* transitions *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -6,7 +6,7 @@
 goalw thy [new_tv_def] 
       "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
 \            new_tv n u";
-by ( fast_tac (set_cs addDs [mgu_free]) 1);
+by (fast_tac (set_cs addDs [mgu_free]) 1);
 qed "mgu_new";
 
 (* application of id_subst does not change type expression *)
@@ -124,22 +124,22 @@
 goalw thy [new_tv_def]
   "new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \
 \                (! l. l < n --> new_tv n (s l) ))";
-by ( safe_tac HOL_cs );
+by (safe_tac HOL_cs );
 (* ==> *)
-by ( fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
-by ( subgoal_tac "m:cod s | s l = TVar l" 1);
-by ( safe_tac HOL_cs );
+by (fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1);
+by (subgoal_tac "m:cod s | s l = TVar l" 1);
+by (safe_tac HOL_cs );
 by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1);
 by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1);
 by (Asm_full_simp_tac 1);
 by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1);
 (* <== *)
-by ( rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
-by ( safe_tac set_cs );
-by ( cut_inst_tac [("m","m"),("n","n")] less_linear 1);
-by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
-by ( cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
-by ( fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] );
+by (safe_tac set_cs );
+by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
+by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1);
+by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
 goal thy 
@@ -169,7 +169,7 @@
   "n<=m --> new_tv n (t::typ) --> new_tv m t";
 by (typ.induct_tac "t" 1);
 (* case TVar n *)
-by ( fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
+by (fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1);
 (* case Fun t1 t2 *)
 by (Asm_simp_tac 1);
 qed_spec_mp "new_tv_le";
@@ -177,7 +177,7 @@
 
 goal thy 
   "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by ( list.induct_tac "ts" 1);
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -212,7 +212,7 @@
 
 goal thy
   "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
-by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "ts" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_tel";
@@ -221,7 +221,7 @@
 (* auxilliary lemma *)
 goal thy
   "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
-by ( simp_tac (!simpset addsimps [new_tv_list]) 1);
+by (simp_tac (!simpset addsimps [new_tv_list]) 1);
 by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
@@ -302,51 +302,52 @@
 (* some useful theorems *)
 goalw thy [free_tv_subst] 
       "!!v. v : cod s ==> v : free_tv s";
-by ( fast_tac set_cs 1);
+by (fast_tac set_cs 1);
 qed "codD";
  
 goalw thy [free_tv_subst,dom_def] 
       "!! x. x ~: free_tv s ==> s x = TVar x";
-by ( fast_tac set_cs 1);
+by (fast_tac set_cs 1);
 qed "not_free_impl_id";
 
 goalw thy [new_tv_def] 
       "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
-by ( fast_tac HOL_cs 1 );
+by (fast_tac HOL_cs 1 );
 qed "free_tv_le_new_tv";
 
 goal thy 
      "free_tv (s (v::nat)) <= cod s Un {v}";
-by ( cut_inst_tac [("P","v:dom s")] excluded_middle 1);
-by ( safe_tac (HOL_cs addSIs [subsetI]) );
+by (cut_inst_tac [("P","v:dom s")] excluded_middle 1);
+by (safe_tac (HOL_cs addSIs [subsetI]) );
 by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1);
 by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1);
 qed "free_tv_subst_var";
 
 goal thy 
      "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by ( typ.induct_tac "t" 1);
+by (typ.induct_tac "t" 1);
 (* case TVar n *)
-by ( simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
+by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
-by ( fast_tac (set_cs addss !simpset) 1);
+by (fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_te";     
 
 goal thy 
      "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by ( list.induct_tac "ts" 1);
+by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
-by ( cut_facts_tac [free_tv_app_subst_te] 1);
-by ( fast_tac (set_cs addss !simpset) 1);
+by (cut_facts_tac [free_tv_app_subst_te] 1);
+by (fast_tac (set_cs addss !simpset) 1);
 qed "free_tv_app_subst_tel";
 
 goalw thy [free_tv_subst,dom_def]
      "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=   \
 \     free_tv s1 Un free_tv s2";
-by ( fast_tac (set_cs addSDs [free_tv_app_subst_te RS
-subsetD,free_tv_subst_var RS subsetD] addss (
-!simpset addsimps [cod_def,dom_def])) 1);
+by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD,
+			     free_tv_subst_var RS subsetD] 
+	             addss (!simpset delsimps bex_simps
+				     addsimps [cod_def,dom_def])) 1);
 qed "free_tv_comp_subst";
 
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -176,9 +176,10 @@
 by (eres_inst_tac [("x","t")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
-by (fast_tac (HOL_cs addIs [cod_app_subst]
+by (fast_tac (HOL_cs addSEs [allE]
+	             addIs [cod_app_subst]
                      addss (!simpset addsimps [less_Suc_eq])) 1);
-
+(** LEVEL 12 **)
 (* case App e1 e2 *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (strip_tac 1); 
@@ -190,6 +191,7 @@
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","na")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
+(** LEVEL 22 **)
 (* second case *)
 by (eres_inst_tac [("x","$ s a")] allE 1);
 by (eres_inst_tac [("x","sa")] allE 1);
@@ -201,6 +203,7 @@
 by (dtac W_var_geD 1);
 by (dtac W_var_geD 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
+(** LEVEL 32 **)
 by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
     less_le_trans,less_not_refl2,subsetD]
@@ -211,10 +214,11 @@
 by (dtac (sym RS W_var_geD) 1);
 by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );
 by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,
-    free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
-    less_le_trans,subsetD]
-  addEs [UnE]
-  addss !simpset) 1); 
+			    free_tv_app_subst_te RS subsetD,
+			    free_tv_app_subst_tel RS subsetD,
+			    less_le_trans,subsetD]
+	             addSEs [UnE]
+		     addss !simpset) 1); 
 qed_spec_mp "free_tv_W"; 
 
 
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/equalities.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -564,9 +564,44 @@
                  "(INT x. A x - B)   = ((INT x.A x) - B)",
                  "(INT x. A - B x)   = (A - (UN x.B x))"];
 
-(*Analogous laws for bounded Unions and Intersections are conditional
+val UN_simps = map prover 
+                ["(UN x:C. A x Int B)  = ((UN x:C.A x) Int B)",
+                 "(UN x:C. A Int B x)  = (A Int (UN x:C.B x))",
+                 "(UN x:C. A x - B)    = ((UN x:C.A x) - B)",
+                 "(UN x:C. A - B x)    = (A - (INT x:C.B x))"];
+
+val INT_simps = map prover
+                ["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
+                 "(INT x:C. A x Un B)  = ((INT x:C.A x) Un B)",
+                 "(INT x:C. A Un B x)  = (A Un (INT x:C.B x))"];
+
+(*The missing laws for bounded Unions and Intersections are conditional
   on the index set's being non-empty.  Thus they are probably NOT worth 
   adding as default rewrites.*)
+
+val ball_simps = map prover
+    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
+     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
+     "(ALL x:{}. P x) = True",
+     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
+     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
+     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"];
+
+val ball_conj_distrib = 
+    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
+
+val bex_simps = map prover
+    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
+     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
+     "(EX x:{}. P x) = False",
+     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
+     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
+     "(EX x:Collect Q. P x) = (EX x. Q x & P x)"];
+
+val bex_conj_distrib = 
+    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
+
 end;
 
-Addsimps (UN1_simps @ INT1_simps);
+Addsimps (UN1_simps @ INT1_simps @ UN_simps @ INT_simps @ 
+	  ball_simps @ bex_simps);
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/ex/Mutil.ML
--- a/src/HOL/ex/Mutil.ML	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/ex/Mutil.ML	Fri Jan 17 11:09:19 1997 +0100
@@ -13,12 +13,11 @@
 (** The union of two disjoint tilings is a tiling **)
 
 goal thy "!!t. t: tiling A ==> \
-\              u: tiling A --> t Int u = {} --> t Un u : tiling A";
+\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
 by (fast_tac (!claset addIs tiling.intrs
-                      addss (HOL_ss addsimps [Un_assoc,
-                                              subset_empty_iff RS sym])) 1);
+                      addss (!simpset addsimps [Un_assoc])) 1);
 qed_spec_mp "tiling_UnI";
 
 
diff -r 0231e4f467f2 -r d708d8cdc8e8 src/HOL/ex/Mutil.thy
--- a/src/HOL/ex/Mutil.thy	Fri Jan 17 10:09:46 1997 +0100
+++ b/src/HOL/ex/Mutil.thy	Fri Jan 17 11:09:19 1997 +0100
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
 
 defs
   below_def  "below n    == nat_rec {} insert n"