--- 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);
--- 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";
--- 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), \
--- 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);
--- 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";
--- 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";
--- 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);
--- 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";
--- 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"