# HG changeset patch
# User oheimb
# Date 941045539 -7200
# Node ID f531589c9fc1df623b5a720713022d5988641b51
# Parent  0196b2302e2109b3d9f74d8787168bcb6e768757
added various little lemmas

diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Finite.ML
--- 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";
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Finite.thy
--- 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
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Fun.ML
--- 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";
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Lex/RegExp2NA.ML
--- 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];
 
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Lex/RegExp2NAe.ML
--- 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];
 
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Map.ML
--- 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";
 
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Map.thy
--- 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)
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/MiniML/MiniML.ML
--- 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);
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Prod.ML
--- 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 *)
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/Real/Hyperreal/Filter.ML
--- 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);
diff -r 0196b2302e21 -r f531589c9fc1 src/HOL/equalities.ML
--- 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";
diff -r 0196b2302e21 -r f531589c9fc1 src/HOLCF/IOA/ABP/Correctness.ML
--- 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);