src/ZF/Coind/Map.ML
changeset 1020 76d72126a9e7
parent 915 6dae0daf57b7
child 1075 848bf2e18dff
     1.1 --- a/src/ZF/Coind/Map.ML	Thu Apr 06 12:20:48 1995 +0200
     1.2 +++ b/src/ZF/Coind/Map.ML	Thu Apr 06 12:22:26 1995 +0200
     1.3 @@ -50,7 +50,6 @@
     1.4  by (rtac subsetI 1);
     1.5  by (eresolve_tac prems 1);
     1.6  by (fast_tac ZF_cs 1);
     1.7 -by flexflex_tac;
     1.8  qed "mapQU";
     1.9  
    1.10  (* ############################################################ *)
    1.11 @@ -59,7 +58,6 @@
    1.12  
    1.13  goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
    1.14  by (fast_tac ZF_cs 1);
    1.15 -by (flexflex_tac);
    1.16  qed "map_mono";
    1.17  
    1.18  (* Rename to pmap_mono *)
    1.19 @@ -77,38 +75,23 @@
    1.20  
    1.21  (** map_owr **)
    1.22  
    1.23 +
    1.24  goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
    1.25    "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
    1.26  by (safe_tac ZF_cs);
    1.27 -
    1.28 -by (asm_full_simp_tac if_ss 1);
    1.29 -by (fast_tac ZF_cs 1);
    1.30 -
    1.31 +by (asm_full_simp_tac if_ss 1 THEN fast_tac ZF_cs 1);
    1.32  by (fast_tac ZF_cs 1);
    1.33 -
    1.34 -by (rtac (excluded_middle RS disjE) 1);
    1.35 -by (dtac (if_not_P RS subst) 1);
    1.36 -by (assume_tac 1);
    1.37 +by (asm_full_simp_tac (ZF_ss addsimps [if_iff]) 1);
    1.38  by (fast_tac ZF_cs 1);
    1.39 -by (hyp_subst_tac 1);
    1.40 -by (asm_full_simp_tac if_ss 1);
    1.41 -by (fast_tac ZF_cs 1);
    1.42 -
    1.43  by (rtac (excluded_middle RS disjE) 1);
    1.44  by (etac image_Sigma1 1);
    1.45 -by (rtac (qbeta RS ssubst) 1);
    1.46 -by (assume_tac 1);
    1.47 -by (dtac map_lem1 1);
    1.48 -by (etac qbeta 1);
    1.49 -by (etac UnE'  1);
    1.50 -by (etac singletonE 1);
    1.51 -by (hyp_subst_tac 1);
    1.52 -by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
    1.53 -by (etac notsingletonE 1);
    1.54 -by (dtac map_lem1 1);
    1.55 -by (rtac if_not_P 1);
    1.56 -by (assume_tac 1);
    1.57 -by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
    1.58 +by (safe_tac upair_cs);    (*This claset knows nothing about domain(m).*)
    1.59 +by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.60 +by (asm_simp_tac (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
    1.61 +by (safe_tac FOL_cs);
    1.62 +by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.63 +by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
    1.64 +by (asm_full_simp_tac (ZF_ss addsimps [qbeta]) 1);
    1.65  by (fast_tac ZF_cs 1);
    1.66  qed "pmap_owrI";
    1.67