--- a/src/HOL/Finite.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Finite.ML Wed Oct 27 19:32:19 1999 +0200
@@ -134,7 +134,7 @@
by (Clarify_tac 1);
by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
by (Clarify_tac 1);
- by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
+ by (full_simp_tac (simpset() addsimps [inj_on_def]delsimps[inj_eq]) 1);
by (Blast_tac 1);
by (thin_tac "ALL A. ?PP(A)" 1);
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
@@ -408,6 +408,15 @@
Delrules [cardR_emptyE];
Delrules cardR.intrs;
+Goal "finite A ==> (card A = 0) = (A = {})";
+by Auto_tac;
+by (dres_inst_tac [("a","x")] mk_disjoint_insert 1);
+by (Clarify_tac 1);
+by (rotate_tac ~1 1);
+by Auto_tac;
+qed "card_0_eq";
+Addsimps[card_0_eq];
+
Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))";
by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
qed "card_insert_if";
@@ -785,8 +794,7 @@
by (subgoal_tac ("x ~: xa") 1);
by Auto_tac;
by (etac rev_mp 1 THEN stac card_Diff_singleton 1);
-by (auto_tac (claset() addIs [finite_subset],
- simpset()));
+by (auto_tac (claset() addIs [finite_subset], simpset()));
qed "choose_deconstruct";
Goal "[| finite(A); finite(B); f : A funcset B; inj_on f A |] \
@@ -814,7 +822,7 @@
by (rtac funcsetI 1);
(* arity *)
by (auto_tac (claset() addSEs [equalityE],
- simpset() addsimps [inj_on_def, restrict_def]));
+ simpset() addsimps [inj_on_def, restrict_def]delsimps[inj_eq]));
by (stac Diff_insert0 1);
by Auto_tac;
qed "constr_bij";
--- a/src/HOL/Finite.thy Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Finite.thy Wed Oct 27 19:32:19 1999 +0200
@@ -18,6 +18,9 @@
syntax finite :: 'a set => bool
translations "finite A" == "A : Finites"
+axclass finite<term
+ finite "finite UNIV"
+
(* This definition, although traditional, is ugly to work with
constdefs
card :: 'a set => nat
--- a/src/HOL/Fun.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Fun.ML Wed Oct 27 19:32:19 1999 +0200
@@ -110,6 +110,7 @@
by (etac injD 1);
by (assume_tac 1);
qed "inj_eq";
+Addsimps[inj_eq];
Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
by (etac injD 1);
@@ -410,7 +411,7 @@
Goal "[| f : A funcset B; g: B funcset C; f `` A = B; inj_on f A; inj_on g B |]\
\ ==> inj_on (compose A g f) A";
by (auto_tac (claset(),
- simpset() addsimps [inj_on_def, compose_eq]));
+ simpset() addsimps [inj_on_def, compose_eq] delsimps[inj_eq]));
qed "inj_on_compose";
@@ -462,7 +463,8 @@
Goal "[| f: A funcset B; inj_on f A; f `` A = B; x: A |] \
\ ==> (lam y: B. (Inv A f) y) (f x) = x";
by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]
+ delsimps[inj_eq]) 1);
by (rtac selectI2 1);
by Auto_tac;
qed "Inv_f_f";
--- a/src/HOL/Lex/RegExp2NA.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Lex/RegExp2NA.ML Wed Oct 27 19:32:19 1999 +0200
@@ -286,7 +286,6 @@
Goalw [epsilon_def,step_def] "step epsilon a = {}";
by (Simp_tac 1);
-by (Blast_tac 1);
qed "step_epsilon";
Addsimps [step_epsilon];
--- a/src/HOL/Lex/RegExp2NAe.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Wed Oct 27 19:32:19 1999 +0200
@@ -21,7 +21,6 @@
Goalw [atom_def,step_def]
"eps(atom a) = {}";
by (Simp_tac 1);
-by (Blast_tac 1);
qed "eps_atom";
Addsimps [eps_atom];
--- a/src/HOL/Map.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Map.ML Wed Oct 27 19:32:19 1999 +0200
@@ -44,7 +44,25 @@
Addsimps[chg_map_new, chg_map_upd];
-section "option_map";
+section "map_of";
+
+Goal "map_of xs k = Some y --> (k,y):set xs";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed_spec_mp "map_of_SomeD";
+
+Goal "[| map_of xs k = Some z; P z |] ==> map_of [(k,z):xs . P z] k = Some z";
+br mp 1;
+ba 2;
+by (etac thin_rl 1);
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_of_filter_in";
+
+
+section "option_map related";
qed_goal "option_map_o_empty" thy
"option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
@@ -54,7 +72,6 @@
(K [rtac ext 1, Simp_tac 1]);
Addsimps[option_map_o_empty, option_map_o_map_upd];
-
section "++";
Goalw [override_def] "m ++ empty = m";
@@ -78,6 +95,12 @@
bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
AddSDs[override_SomeD];
+Goal "!!xx. n k = Some xx ==> (m ++ n) k = Some xx";
+by (stac override_Some_iff 1);
+by (Fast_tac 1);
+qed "override_find_right";
+Addsimps[override_find_right];
+
Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
by (simp_tac (simpset() addsplits [option.split]) 1);
qed "override_None";
@@ -92,13 +115,6 @@
qed "map_of_override";
Addsimps [map_of_override];
-Goal "map_of xs k = Some y --> (k,y):set xs";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
-qed_spec_mp "map_of_SomeD";
-
section "dom";
--- a/src/HOL/Map.thy Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Map.thy Wed Oct 27 19:32:19 1999 +0200
@@ -19,8 +19,6 @@
map_of :: "('a * 'b)list => 'a ~=> 'b"
map_upds:: "('a ~=> 'b) => 'a list => 'b list =>
('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900)
-
-
syntax
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
("_/'(_/|->_')" [900,0,0]900)
--- a/src/HOL/MiniML/MiniML.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/MiniML/MiniML.ML Wed Oct 27 19:32:19 1999 +0200
@@ -223,7 +223,7 @@
by (etac IntE 1);
by (dtac (free_tv_S' RS subsetD) 1);
by (dtac (free_tv_alpha RS subsetD) 1);
- by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() delsimps [full_SetCompr_eq]) 1);
by (etac exE 1);
by (hyp_subst_tac 1);
by (subgoal_tac "new_tv (n + y) ($ S A)" 1);
--- a/src/HOL/Prod.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Prod.ML Wed Oct 27 19:32:19 1999 +0200
@@ -234,6 +234,11 @@
by (Asm_simp_tac 1);
qed "splitI2";
+Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2'";
+
Goal "c a b ==> split c (a,b)";
by (Asm_simp_tac 1);
qed "splitI";
@@ -268,7 +273,7 @@
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "mem_splitE";
-AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
+AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
AddSEs [splitE, mem_splitE];
(* allows simplifications of nested splits in case of independent predicates *)
--- a/src/HOL/Real/Hyperreal/Filter.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.ML Wed Oct 27 19:32:19 1999 +0200
@@ -346,7 +346,7 @@
\ {A:: 'a set. finite (- A)} : Filter UNIV";
by (cut_facts_tac [prem] 1);
by (rtac mem_FiltersetI2 1);
-by (auto_tac (claset(),simpset() addsimps [Compl_Int]));
+by (auto_tac (claset(), simpset() delsimps [Collect_empty_eq]));
by (eres_inst_tac [("c","UNIV")] equalityCE 1);
by (Auto_tac);
by (etac (Compl_anti_mono RS finite_subset) 1);
--- a/src/HOL/equalities.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/equalities.ML Wed Oct 27 19:32:19 1999 +0200
@@ -28,6 +28,11 @@
qed "not_psubset_empty";
AddIffs [not_psubset_empty];
+Goal "(Collect P = {}) = (!x. ~ P x)";
+by Auto_tac;
+qed "Collect_empty_eq";
+Addsimps[Collect_empty_eq];
+
Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
by (Blast_tac 1);
qed "Collect_disj_eq";
@@ -153,6 +158,14 @@
qed "image_cong";
+section "range";
+
+Goal "{u. ? x. u = f x} = range f";
+by Auto_tac;
+qed "full_SetCompr_eq";
+Addsimps[full_SetCompr_eq];
+
+
section "Int";
Goal "A Int A = A";
--- a/src/HOLCF/IOA/ABP/Correctness.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Wed Oct 27 19:32:19 1999 +0200
@@ -10,7 +10,7 @@
by (Fast_tac 1);
qed"exis_elim";
-Delsimps [split_paired_All];
+Delsimps [split_paired_All,Collect_empty_eq];
Addsimps
([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def,
ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def,
@@ -210,9 +210,8 @@
Receiver.receiver_trans_def] @ set_lemmas);
Goal "compatible receiver_ioa (srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,
- asig_of_par,asig_comp_def,actions_def,
- Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);
@@ -221,7 +220,8 @@
(* 5 proofs totally the same as before *)
Goal "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);
@@ -230,7 +230,8 @@
Goal "compatible sender_ioa \
\ (receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);
@@ -239,7 +240,8 @@
Goal "compatible sender_ioa\
\ (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def, compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def, compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);
@@ -248,7 +250,8 @@
Goal "compatible env_ioa\
\ (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);
@@ -257,7 +260,8 @@
Goal "compatible env_ioa\
\ (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)";
-by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
+by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,
+ actions_def,Int_def]) 1);
by (Simp_tac 1);
by (rtac set_ext 1);
by (induct_tac "x" 1);